Decreasing Diagrams and Relative Termination (2009)
Hirokawa, Nao, Middeldorp, Aart
In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and the critical pair steps are relatively...
Naturwissenschaften der Rheinisch-Westfälischen (2009)
René Thiemann, Aachen Erlangung, René Thiemann, Prof Dr, Jürgen Giesl, ...
vorgelegt von
2 SAT Solving for Termination Analysis with (2009)
Carsten Fuhs, Aart Middeldorp, Peter Schneiderkamp, Harald Zankl, Carsten Fuhs, Aart Middeldorp, ...
Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination...
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-kamp, René Thiemann, Harald Zankl
Abstract. We present a new approach for termination proofs that uses polynomial interpretations (with possibly negative coefficients) together with the “maximum ” function. To obtain a powerful...
2 Innermost Termination of Context-Sensitive Rewriting (2009)
Jürgen Giesl, Aart Middeldorp, Jürgen Giesl, Aart Middeldorp
Abstract. Context-sensitive rewriting is a restriction of term rewriting used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under...
Kennaway proved the remarkable result that every (almost) orthogonal term rewriting system admits a computable sequential normalizing reduction strategy. In this paper we present a computable...
Constraint-Based Multi-Completion Procedures for Term Rewriting Systems (2009)
Sato, Haruhiko, Kurihara, Masahito, Winkler, Sarah, Middeldorp, Aart
In equational theorem proving, convergent term rewriting systems play a crucial role. In order to compute convergent term rewriting systems, the standard completion procedure (KB) was proposed by...
On the Complexity of Deciding Call-by-Need (2009)
Durand, Irène, Middeldorp, Aart
In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground...
2 Maximal Termination ⋆ (2008)
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, René Thiemann, Harald Zankl, Carsten Fuhs, ...
Abstract. We present a new approach for termination proofs that uses polynomial interpretations (with possibly negative coefficients) together with the “maximum ” function. To obtain a powerful...
Uncurrying for Termination ⋆ (2008)
Abstract. In this note we present a transformation from untyped applicative term rewrite systems to functional term rewrite systems that preserves termination. Our transformation can handle head...
Abstract Tyrolean Termination Tool: Techniques and Features (2008)
The Tyrolean Termination Tool (T T T for short) is a powerful tool for automatically proving termination of rewrite systems. It incorporates several new refinements of the dependency pair method that...
Abstract Decidable Call-by-Need Computations in Term Rewriting (2008)
The theorem of Huet and Lévy stating that for orthogonal rewrite systems (i) every reducible term contains a needed redex and (ii) repeated contraction of needed redexes results in a normal form if...
Completeness Results for Basic Narrowing 1 (2008)
In this paper we analyze completeness results for basic narrowing. We show that basic narrowing is not complete with respect to normalizable solutions for equational theories defined by confluent...
Uncurrying for Termination ⋆ (2008)
Abstract. In this note we present a transformation from untyped applicative term rewrite systems to functional term rewrite systems that preserves termination. Our transformation can handle head...
Predictive labeling with dependency pairs using SAT (2008)
Adam Koprowski, Aart Middeldorp
Abstract. This paper combines predictive labeling with dependency pairs and reports on its implementation. Our starting point is the method of proving termination of rewrite systems using semantic...
Automating the Dependency Pair Method Abstract (2008)
Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area in the past few...
1 Constraints for Argument Filterings ⋆ (2008)
Harald Zankl, Nao Hirokawa, Aart Middeldorp
Argument filterings are a key ingredient of the dependency pair method. Finding a suitable argument filtering that enables the constraints originating from the dependency pair method to be solved by...
Approximations for Strategies and Termination Abstract (2008)
The theorem of Huet and Lévy stating that for orthogonal rewrite systems (i) every reducible term contains a needed redex and (ii) repeated contraction of needed redexes results in a normal form if...
Decidable Call by Need Computations in Term Rewriting (Extended Abstract) (2008)
Abstract. In this paper we study decidable approximations to call by need computations to normal and root-stable forms in term rewriting. We obtain uniform decidability proofs by making use of...
1 KBO as a Satisfaction Problem ⋆ (2008)
Abstract This note presents an approach to prove termination of term rewrite systems (TRSs) with the Knuth-Bendix order efficiently. The constraints for the weight function as well as for the...
Proving Termination of Rewrite Systems using Bounds (2008)
Abstract. The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. We extend...
Implementing RPO and POLO using SAT ⋆ (2008)
Carsten Fuhs, Peter Schneider-kamp, Rene Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, ...
Abstract. Well-founded orders are the most basic, but also most important ingredient to virtually all termination analyses. Numerous fully automated search algorithms for these classes have therefore...
Predictive labeling with dependency pairs using SAT (2008)
Adam Koprowski, Aart Middeldorp
Abstract. This paper combines predictive labeling with dependency pairs and reports on its implementation. Our starting point is the method of proving termination of rewrite systems using semantic...
On the modularity of deciding call-by-need (2007)
Abstract. In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques...
Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema
Abstract. For two hierarchies of properties of term rewriting systems related to confluence and termination, respectively, we prove relative undecidability: for implications X) Y in the hierarchies...
Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema
Abstract. We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for...
Hitoshi Ohsaki, Aart Middeldorp
Abstract. Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in Zantema [24] is however...
Mohamed Hamada, Aart Middeldorp
In this paper we extend the lazy narrowing calculus of Middeldorp, Okui, and Ida [13] to conditional rewrite systems. We show that our calculus is strongly complete whenever basic conditional...
Mohamed Hamada, Aart Middeldorp
In this paper we extend the lazy narrowing calculus of Middeldorp, Okui, and Ida [13] to conditional rewrite systems. We show that our calculus is strongly complete whenever basic conditional...
Abstract. This paper is concerned with methods that automatically prove termination of term rewrite systems. The aim of dummy elimination, a method to prove termination introduced by Ferreira and...
Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema
Abstract. We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for...
Abstract. In this paper we study decidable approximations to call by need computations to normal and root-stable forms in term rewriting. We obtain uniform decidability proofs by making use of...
Completeness Results for Basic Narrowing 1 (2007)
In this paper we analyze completeness results for basic narrowing. We show that basic narrowing is not complete with respect to normalizable solutions for equational theories defined by confluent...
Hitoshi Ohsaki, Aart Middeldorp
Abstract. Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in Zantema [24] is however...
SAT solving for termination analysis with polynomial interpretations (2007)
Carsten Fuhs, Aart Middeldorp, Peter Schneider-kamp, Harald Zankl
Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination...
Satisfying KBO Constraints (2007)
Abstract. This paper presents two new approaches to prove termination of rewrite systems with the Knuth-Bendix order efficiently. The constraints for the weight function and for the precedence are...
SAT solving for termination analysis with polynomial interpretations (2007)
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-kamp, René Thiemann, Harald Zankl, ...
Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination...
Innermost termination of rewriting systems by labeling (2007)
René Thiemann, Lufg Informatik, Rwth Aachen, Aart Middeldorp
Semantic labeling is a powerful transformation technique for proving termination of term rewrite systems. The semantic part is given by a model or a quasi-model of the rewrite rules. A variant of...
Implementing RPO and POLO using SAT (2007)
Schneider-Kamp, Peter, Fuhs, Carsten, Thiemann, René, Giesl, Jürgen, Annov, Elena, Codish, Michael, ...
Well-founded orderings are the most basic, but also most important ingredient to virtually all termination analyses. The recursive path order with status (RPO) and polynomial interpretations (POLO)...
2 SAT Solving for Termination Analysis with Polynomial Interpretations ⋆ (2007)
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider, René Thiemann, Harald Zankl, ...
Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination...
Satisfying KBO Constraints (2006)
Zankl, Harald, Middeldorp, Aart
This paper presents two new approaches to prove termination of rewrite systems with the Knuth-Bendix order efficiently. The constraints for the weight function and for the precedence are encoded in...
Abstract. Semantic labeling is a transformation technique for proving the termination of rewrite systems. The semantic part is given by a quasi-model of the rewrite rules. In this paper we present a...
Transformation Techniques for Context-Sensitive Rewrite Systems (2004)
Aachener Informatik Berichte, Jiirgen Giesl, Aart Middeldorp, Aart Middeldorp
Abstract. Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and...
WST'04 7th International Workshop on Termination (2004)
Michael Codish, Aart Middeldorp, Aart Middeldorp (eds, Aachener Informatik Berichte, Rwth Aachen
Partial Evaluation for Termination Analysis . . . . . . . . . . . . . . . . . . . . . 47 Lior Tamary, Michael Codish Relative Termination in Term Rewriting . . . . . . . . . . . . . . . . . . . . . ....
Transformation Techniques for Context-Sensitive Rewrite Systems (2004)
Jürgen Giesl, Jürgen Giesl, Aart Middeldorp, Aart Middeldorp
Abstract. Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and...
WST’04 7th International Workshop on Termination (2004)
Michael Codish, Aart Middeldorp (eds, Aart Middeldorp, Claude Marché Orsay, Frederic Mesnard, ...
This workshop delves into all aspects of termination of processes. Though the halting of computer programs is undecidable, methods of establishing termination play a fundamental role in many...
Dependency Pairs Revisited (2004)
Abstract. In this paper we present some new refinements of the dependency pair method for automatically proving the termination of term rewrite systems. These refinements are very easy to implement,...
Polynomial interpretations with negative coefficients (2004)
Abstract. Polynomial interpretations are a useful technique for proving termination of term rewrite systems. We show how polynomial interpretations with negative coefficients, like x − 1 for a...
Tsukuba termination tool (2003)
We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl [1]. It incorporates several new ideas that...
Tsukuba termination tool (2003)
Abstract. We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl. It incorporates several new ideas...
Approximating dependency graphs without using tree automata techniques (2003)
In the dependency pair method of Arts and Giesl [2], one of the most popular methods for automatically proving (innermost) termination of TRSs, a TRS is
Automating the dependency pair method (2003)
Abstract. Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area in the...
Innermost termination of context-sensitive rewriting (2002)
Aart Middeldorp, Aart Middeldorp
Abstract. Context-sensitive rewriting is a restriction of term rewriting used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under...
New Completeness Results for Lazy Conditional Narrowing (2002)
Narrowing was originally invented as a general method for solving unification problems in equational theories that are presented by confluent term rewriting systems (TRSs for short). More recently,...
Innermost termination of context-sensitive rewriting (2002)
Abstract. Context-sensitive rewriting is a restriction of term rewriting used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under...
Relative Undecidability in Term Rewriting (Part 2: The confluence Hierarchy (2002)
Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema
For a hierarchy of properties of term rewriting systems related to confluence we prove relative undecidability, i.e., for implications X Y in the hierarchy the property X is undecidable for term...
Complete selection functions for a lazy conditional narrowing calculus (2002)
Abstract. This paper is concerned with the lazy conditional narrowing calculus lcnc. In an earlier paper we proved that this calculus is complete with respect to normalizable solutions for the class...
New Completeness Results for Lazy Conditional Narrowing (2002)
Narrowing was originally invented as a general method for solving unification problems in equational theories that are presented by confluent term rewriting systems (TRSs for short). More recently,...
Innermost termination of context-sensitive rewriting (2002)
Aart Middeldorp, Aart Middeldorp
Context-sensitive rewriting is a restriction of term rewriting used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under certain...
Innermost termination of context-sensitive rewriting (2002)
Abstract. Context-sensitive rewriting is a restriction of term rewriting used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under...
Relative Undecidability in Term Rewriting (Part 2: The confluence Hierarchy (2002)
Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema
For a hierarchy of properties of term rewriting systems related to confluence we prove relative undecidability, i.e., for implications X ⇒ Y in the hierarchy the property X is undecidable for term...
Approximating dependency graphs using tree automata techniques (2001)
Abstract. The dependency pair method of Arts and Giesl is the most powerful technique for proving termination of term rewrite systems automatically. We show that the method can be improved by using...
Eliminating dummy elimination (2000)
Abstract. This paper is concerned with methods that automatically prove termination of term rewrite systems. The aim of dummy elimination, a method to prove termination introduced by Ferreira and...
Logicality of conditional rewrite systems (2000)
Toshiyuki Yamada, Jurgen Avenhaus, Aart Middeldorp
A conditional term rewriting system is called logical if it has the same logical strength as the underlying conditional equational system. In this paper we summarize known logicality results and we...
Equational Termination by Semantic Labelling (2000)
Hitoshi Ohsaki, Aart Middeldorp, Jürgen Giesl
. Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in Zantema [24] is however rather...
Eliminating Dummy Elimination (2000)
This paper is concerned with methods that automatically prove termination of term rewrite systems. The aim of dummy elimination, a method to prove termination introduced by Ferreira and Zantema, is...
Logicality of Conditional Rewrite Systems (2000)
Toshiyuki Yamada Doctoral, Toshiyuki Yamada, Jurgen Avenhaus, Aart Middeldorp
A conditional term rewriting system is called logical if it has the same logical strength as the underlying conditional equational system. In this paper we summarize known logicality results and we...
Eliminating dummy elimination (2000)
Abstract. This paper is concerned with methods that automatically prove termination of term rewrite systems. The aim of dummy elimination, a method to prove termination introduced by Ferreira and...
Eliminating dummy elimination (2000)
Abstract. This paper is concerned with methods that automatically prove termination of term rewrite systems. The aim of dummy elimination, a method to prove termination introduced by Ferreira and...
Transforming context-sensitive rewrite systems (1999)
Abstract. We present two new transformation techniques for proving termination of context-sensitive rewriting. Our first method is simple, sound, and more powerful than previously suggested...
Transforming Context-Sensitive Rewrite Systems (1999)
. We present two new transformation techniques for proving termination of context-sensitive rewriting. Our first method is simple, sound, and more powerful than previously suggested transformations....
LNCA: A Lazy Narrowing Calculus for Applicative Term Rewriting Systems (1999)
Mircea Marin, Tetsuo Ida, Aart Middeldorp, Takura Yanagi
The integration of higher-order functions into functional logic programming is widely seen as a powerful and desirable feature. The natural way to deal with higher-order functions in the well-studied...
Context-Freeness and Infinitary Normalization (1999)
In [2] it is shown that context-free root-normalizing reduction strategies are infinitary fair-normalizing for confluent TRSs. Lucas [1, Theorem 6.6] shows that every NV-strategy is infinitary...
On the Complexity of Deciding Call-by-Need (1998)
Durand, Irène, Middeldorp, Aart
In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground...
On the Complexity of Deciding Call-by-Need (1998)
Durand, Irène, Middeldorp, Aart
In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground...
A Deterministic Lazy Narrowing Calculus (1998)
In this paper we study the non-determinism between the inference rules of the lazy narrowing calculus lnc (Middeldorp et al., 1996). We show that all non-determinism can be removed without losing the...
A Deterministic Lazy Narrowing Calculus (1998)
In this paper we study the non-determinism between the inference rules of the lazy narrowing calculus lnc [16]. We show that all non-determinism can be removed without losing the important...
Strongly sequential and inductively sequential term rewriting systems (1998)
Michael Hanus, Salvador Lucas, Aart Middeldorp
The concept of definitional tree by Antoy serves to introduce control information into the bare set of rules of a constructor-based term rewriting system (TRS). TRSs whose rules can be arranged into...
A Deterministic Lazy Narrowing Calculus (1998)
In this paper we study the non-determinism between the inference rules of the lazy narrowing calculus lnc (Middeldorp et al., 1996). We show that all non-determinism can be removed without losing the...
Logicality of Conditional Rewrite Systems Abstract (1998)
Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría-sáenz, Aart Middeldorp
A conditional term rewriting system is called logical if it has the same logical strength as the underlying conditional equational system. In this paper we summarize known logicality results and we...
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Femke van Raamsdonk Roel de Vrijer (Eds.)
Decidable Call by Need Computations in Term Rewriting (Extended Abstract (1997)
In this paper we study decidable approximations to call by need computations to normal and root-stable forms in term rewriting. We obtain uniform decidability proofs by making use of elementary tree...
Call by Need Computations to Root-Stable Form (1997)
The following theorem of Huet and L'evy forms the basis of all results on optimal reduction strategies for orthogonal term rewriting systems: every term not in normal form contains a needed...
Simple termination of rewrite systems (1997)
In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simplification order. The basic...
Simple termination of rewrite systems (1997)
In this paper we investigate the concept of simple termination. A term rewriting system (TRS for short) is called simply terminating if its termination can be proved by means of a simplification...
Relative undecidability in term rewriting (1997)
Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema
Abstract. For two hierarchies of properties of term rewriting systems related to con uence and termination, respectively, we prove relative undecidability: for implications X) Y in the hierarchies...
Simple termination of rewrite systems (1997)
In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simplification order. The basic...
Lazy Narrowing: Strong Completeness and Eager Variable Elimination (1996)
Aart Middeldorp, Satoshi Okui, Tetsuo Ida
Narrowing is an important method for solving unification problems in equational theories that are presented by confluent term rewriting systems. Because narrowing is a rather complicated operation,...
Lazy Narrowing: Strong Completeness and Eager Variable Elimination (1996)
Aart Middeldorp, Satoshi Okui, Tetsuo Ida
Narrowing is an important method for solving unification problems in equational theories that are presented by confluent term rewriting systems. Because narrowing is a rather complicated operation,...
Relative Undecidability in Term Rewriting (1996)
Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema
. For two hierarchies of properties of term rewriting systems related to confluence and termination, respectively, we prove relative undecidability: for implications X ) Y in the hierarchies the...
Transforming Termination by Self-Labelling (1996)
Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema
. We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for establishing...
Transforming Termination by Self-Labelling (1996)
Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema
. We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for establishing...
A Sequential Reduction Strategy (1996)
Kennaway proved the remarkable result that every (almost) orthogonal term rewriting system admits a computable sequential normalizing reduction strategy. In this paper we present a computable...
Transforming termination by selflabelling (1996)
Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema
Abstract. We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for...
A complete narrowing calculus for higher-order functional logic programming (1995)
Koichi Nakahara, Aart Middeldorp, Tetsuo Ida, Canon Inc
Abstract. Using higher-order functions is standard practice in functional programming, but most functional logic programming languages that have been described in the literature lack this feature....
A complete narrowing calculus for higher-order functional logic programming (1995)
Koichi Nakahara, Aart Middeldorp, Tetsuo Ida
Abstract. Using higher-order functions is standard practice in functional programming, but most functional logic programming languages that have been described in the literature lack this feature....
Level-confluence of conditional rewrite systems with extra variables in right-hand sides (1995)
Taro Suzuki, Aart Middeldorp, Tetsuo Ida
Level-confluence is an important property of conditional term rewriting systems that allow extra variables in the rewrite rules because it guarantees the completeness of narrowing for such systems....
Level-confluence of conditional rewrite systems with extra variables in right-hand sides (1995)
Taro Suzuki, Aart Middeldorp, Tetsuo Ida
Level-confluence is an important property of conditional term rewriting systems that allow extra variables in the rewrite rules because it guarantees the completeness of narrowing for such systems....
A complete narrowing calculus for higher-order functional logic programming (1995)
Koichi Nakahara, Aart Middeldorp, Tetsuo Ida, Canon Inc
Abstract. Using higher-order functions is standard practice in functional programming, but most functional logic programming languages that have been described in the literature lack this feature....
Level-confluence of conditional rewrite systems with extra variables in right-hand sides (1995)
Taro Suzuki, Aart Middeldorp, Tetsuo Ida
Level-confluence is an important property of conditional term rewriting systems that allow extra variables in the rewrite rules because it guarantees the completeness of narrowing for such systems....
Simple Termination Revisited (1994)
In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simplification order. The basic...
A sequential reduction strategy (1994)
Kennaway proved the remarkable result that every (almost) orthogonal term rewriting system admits a computable sequential normalizing reduction strategy. In this paper we present a computable...
Simple Termination Revisited (1994)
In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simplification order. The basic...
A sequential reduction strategy (1994)
Kennaway proved the remarkable result that every (almost) orthogonal term rewriting system admits a computable sequential normalizing reduction strategy. In this paper we present a computable...
Completeness of combinations of conditional constructor systems (1994)
In this paper we extend the divide and conquer technique of Middeldorp and Toyama for establishing (semi-)completeness of constructor systems to conditional constructor systems. We show that both...
Modularity of confluence: A simplified proof (1994)
Jan Willem Klop, Aart Middeldorp, Yoshihito Toyama, Roel De Vrijer
In this note we present a simple proof of a result of Toyama which states that the disjoint union of confluent term rewriting systems is confluent.
Simple termination is difficult (1993)
Aart Middeldorp, Bernhard Gramlich
A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than...
Simple Termination is Difficult (1993)
Aart Middeldorp, Bernhard Gramlich
A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than...
Simple Termination is Difficult (1993)
Aart Middeldorp, Bernhard Gramlich
A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than...
Simple termination is difficult (1993)
Aart Middeldorp, Bernhard Gramlich
A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than...
Completeness of combinations of constructor systems (1991)
A term rewriting system is called complete if it is both confluent and strongly normalising. Barendregt and Klop showed that the disjoint union of complete term rewriting systems does not need to be...
A rewrite approach to polynomial ideal theory (1991)
Aart Middeldorp, Mirjana Starčević
A self-contained introduction is given to the theory of Gröbner bases which provide algorithmic solutions to many problems in polynomial ideal theory. After explaining the basic theory of Gröbner...
Completeness of combinations of constructor systems (1991)
Aart Middeldorp, Yoshihito Toyama
A term rewriting system is called complete if it is both confluent and strongly normalising. Barendregt and Klop showed that the disjoint union of complete term rewriting systems does not need to be...