Gutiérrez Gil, Raúl; Lucas Alba, Salvador(Springer Nature, 2020-07-06)
[EN] We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems. We follow a ...
Lucas Alba, Salvador; Meseguer, Jose(Elsevier, 2016-01)
We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the ...
Lucas Alba, Salvador; Vítores-Vicente, Miguel; Gutiérrez Gil, Raúl(Elsevier, 2022-04)
[EN] Context-sensitive rewriting is a restriction of term rewriting where reductions are allowed on specific arguments of function symbols only, and then in particular positions of terms. Confluence is an abstract property ...
Lucas Alba, Salvador; Meseguer, José(ACM, 2014-09)
A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) ...
[EN] The semantics of computational systems (e.g., relational and knowledge data bases, query-answering systems, programming languages, etc.) can often be expressed as (the specification of) a logical theory Th. Queries, ...
[EN] Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. Proving termination of CSR is an interesting problem with several applications in the fields ...
[EN] MU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted ...
Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g.; termination proving, program invariant generation and hybrid system verification, to name a ...
Navarro Marset, Rafael Andrés(Universitat Politècnica de València, 2011-11-28)
A termination problem can be transformed into a set of polynomial constraints. Up to now, several approaches have been studied to deal with these constraints as constraint solving problems. In this thesis, we study in depth ...
Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
[EN] Recent developments in termination analysis for declarative programs emphasize the use of appropriate models for the logical theory representing the program at stake as a generic approach to prove termination of ...
Arnal Julián, Salvador(Universitat Politècnica de València, 2014-11-18)
[EN] This thesis presents the implementation of a framework to work with term rewriting
systems. Term rewriting systems provide a complete computational model which is very
close to functional programming. Its formulation ...
[EN] Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization ...
Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl(Elsevier, 2018-09)
[EN] Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite ...
Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl(Springer-Verlag, 2020-10)
[EN] Proving termination of programs in `real-life¿ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully cap- turing the impact in the termination ...
[EN] The halting problem is a prominent example of undecidable problem and its formulation and undecidability proof is usually attributed to Turing's 1936 landmark paper. Copeland noticed in 2004, though, that it was so ...
Alarcón Jiménez, Beatriz(Universitat Politècnica de València, 2011-06-10)
Maude es un lenguaje de programación declarativo basado en la lógica de reescritura
que incorpora muchas características que lo hacen muy potente. Sin
embargo, a la hora de probar ciertas propiedades computacionales esto ...
Gutiérrez Gil, Raúl; Lucas Alba, Salvador(Sistedes, 2014-09-16)
Modularity is essential in software development, where a piece of software is often designed and implemented as a composition of simpler modules. So, if we want to prove that a program satisfies a given property, a modular ...
Darás de la Fuente, Claudia(Universitat Politècnica de València, 2022-10-18)
[ES] El sector de la programación está en una continua actualización e innovación, ya sea por nuevas
tendencias que surgen o por nuevas tecnologías emergentes. Pero para que la programación
funcione se necesitan lenguajes ...