[EN] Context-sensitive rewriting is a restriction of term rewriting which is obtained by imposing replacement restrictions on the arguments of function symbols. It has proven useful to analyze computational properties of ...

[EN] Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the ...

[EN] The appropriate selection of the arguments of functions that can be evaluated in function calls is often useful to improve efficiency, speed, termination behavior, and so on. This is essential, e.g., in the conditional ...

[EN] Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments mu(f) subset of {1, ..., k} of k-ary function symbols f only. Terms which cannot be further rewritten ...

[EN] The dependency pairs method is one of the most powerful technique for proving termination of rewriting and it is currently central in most automatic termination provers. Recently, it has been adapted to be used in ...

Innermost context-sensitive 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 ...

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce ...

[EN] Essentially, in a reversible programming language, for each forward computation from state S to state S', there exists a constructive method to go backwards from state S' to state S. Besides its theoretical interest, ...

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 ...