Freezing - Termination Proofs for Classical, Context-Sensitive and Innermost Rewriting (2007)
. Freezing is a powerful technique for orienting equations. Here we give a new presentation of it which is suitable for an efficient automatic use. Further, it is shown how slight modifications of it...
Erasure for Termination Proofs (2007)
. Weintroduce a technique to facilitate termination proofs for term rewriting systems. We especially focus on innermost termination. The main features of this technique lie in its simplicity and...
Erasure for Termination Proofs (2007)
. We introduce a technique to facilitate termination proofs for term rewriting systems. We especially focus on innermost termination. The main features of this technique lie in its simplicity and...
Towards the Generation of Polynomial Orderings (2007)
Orderings on polynomial interpretations of operators represent a powerful technique for proving the termination of rewriting systems. One of the main problems of polynomial orderings concerns the...
Notes on Transformation Orderings (2000)
An important property and also a crucial point ofa term rewriting system is its termination. Transformation or-derings, developed by Bellegarde & Lescanne strongly based on awork of Bachmair &...
On the Complexity of Simplification Orderings (2000)
Various methods for proving the termination of term rewriting systems havebeen suggested. Most of them are based on the notion of simplification ordering.In this paper, the theoretical time...
Termination Proofs of Rewriting Systems (2000)
Orderings on polynomial interpretations of operators represent a powerful technique for proving thetermination of rewriting systems. One of the main problems of polynomial orderings concerns...
Termination of Rewriting (2000)
More and more, term rewriting systems are applied in computer science aswell as in mathematics. They are based on directed equations which may be used as non-deterministic functional programs....
Model Elimination with Basic Ordered Paramodulation (1995)
Max Moser, Christopher Lynch, Joachim Steinbach
this paper, we introduce a novel approach for goal-directed theorem proving with equality which integrates Basic Ordered Paramodulation into a Model Elimination framework. The underlying idea is to...
A Reduction Ordering for Higher-Order Terms (1995)
Jürgen Avenhaus, Carlos Loría-Sáenz, Joachim Steinbach
. We investigate one of the classical problems of the theory of term rewriting, namely termination. We present an ordering for comparing higher-order terms that can be utilized for testing...
Kaiserslautern, Universiẗat, Diss., 1994.
On the Complexity of Simplification Orderings (1993)
Various methods for proving the termination of term rewriting systems have been suggested. Most of them are based on the notion of simplification ordering. In this paper, the theoretical time...
Notes on Transformation Orderings (1992)
. An important property and also a crucial point of a term rewriting system is its termination. Transformation orderings, developed by Bellegarde & Lescanne strongly based on a work of Bachmair...