
Gutiérrez Gil, Raúl; Lucas Alba, Salvador
Contextsensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions of subterms that can be rewritten; or frozen, i.e., positions that cannot. Frozen positions can be used to denote subexpressions whose evaluation is delayed or just forbidden. A typical example is the ifthenelse operator whose second and third arguments are not evaluated until the evaluation of the first argument yields either true or false. Imposing replacement restrictions can improve the termination behavior of rewritingbased computational systems. Termination of...

María Alpuente; Santiago Escobar; Javier Espert; José Meseguer
Computing generalizers is relevant in a wide spectrum of automated
reasoning areas where analogical reasoning and inductive inference
are needed. The ACUOS system computes a complete and minimal
set of semantic generalizers (also called \antiuni ers") of two structures
in a typed language modulo a set of equational axioms. By supporting
types and any combination of associativity (A), commutativity (C), and
unity (U) algebraic axioms for function symbols, ACUOS allows reasoning
about typed data structures, e.g. lists, trees, and (multi)sets, and
typical hierarchical/structural relations such as is a and part of. This
paper discusses the modular ACU generalization tool ACUOS and illustrates
its use in a classical arti ficial intelligence...

COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
Automatic techniques for program verification usually suffer the wellknown state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which rep resents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and some times the needed fragment is quite huge.
In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpreta tion techniques)...

COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
In this paper, we present a new compositional bottomup semantics for the Timed Concurrent Constraint Language (tccp in short) which is defined for the full language. In particular, is able to deal with the non monotonic characteristic of tccp, which constitutes a substantial addi tional technical difficulty w.r.t. other compositional denotational seman tics present in literature (which do not tackle the full language).
The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems and they may not terminate with...

COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
In this paper, we present a new compositional bottomup semantics for the Timed Concurrent Constraint Language (tccp in short). Such semantics is defined for the full language. In particular, is able to deal with the nonmonotonic characteristic of the language, which constitutes a substantial additional technical difficulty w.r.t. other compositional denotational semantics present in literature (which do not tackle the full language).
The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems.
The overall of these features makes our proposal...

Alarcón Jiménez, Beatriz; Gutierrez Gil, Raúl; Lucas, Salvador; Meseguer, José
The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logicbased programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. One of the most important techniques for proving termination over a wide range of variants of rewriting (strategies) is the dependency pair approach. Several works have tried to adapt it to rewriting modulo associative and commutative (AC) equational theories, and even to more general theories. However, as we discuss in this paper, no appropriate notion of minimality (and minimal chain of dependency pairs) which is wellsuited to develop a...

Alarcón Jiménez, Beatriz; Lucas, Salvador
Innermost contextsensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude, OBJ, etc, which incorporate an innermost strategy which is used to break down the nondeterminism which is inherent to reduction relations. Furthermore, innermost termination of rewriting is often easier to prove than termination. Thus, under appropriate conditions, a useful strategy for proving termination of rewriting is trying to prove termination of innermost rewriting. This phenomenon has also been investigated for contextsensitive rewriting. Up to now, only few transformationbased methods have been proposed and used to (specifically) prove termination of innermost...

Alpuente Frasnedo, María; Ballis, Demis; Espert, Javier; Romero, Daniel
Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textuallylarge system computations...

Alpuente Frasnedo, María; Ballis, D.; Espert, J.; Romero, D.
Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result.
Our methodology is particularly suitable for analyzing complex, textuallylarge system computations...

Alpuente Frasnedo, María; Baggi, Michele; Ballis, Demis; Falaschi, Moreno
Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowingbased unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of...