JAIST Repository
https://dspace.jaist.ac.jp/

Title

Equational Reasoning and Completion

Author(s)Klein, Dominik

CitationIssue Date

2012‑06

Type

Thesis or Dissertation

Text version

author

URL

http://hdl.handle.net/10119/10560

RightsDescription

Supervisor: Mizuhito Ogawa, 情報科学研究科, 博士

Japan Advanced Institute of Science and Technology

Equational Reasoning and Completion

byDominik Klein

submitted toJapan Advanced Institute of Science and Technology
in partial fulfillment of the requirements
for the degree ofDoctor of Philosophy

Supervisor: Professor Mizuhito Ogawa

School of Information Science
Japan Advanced Institute of Science and Technology

June 2012Abstract
Equations are a versatile and natural tool for various reasoning tasks. This
thesis investigates how to fully automate equational reasoning. Central to automation is Knuth and Bendix’ ground-breaking completion procedure. It was
originally formulated as an algorithm, and requires a user-provided reduction
order. We show that completion can be characterized as an optimization problem. Using this formulation, called Maximal Completion, algorithmic aspects canbe abstracted away by encoding the optimization problem to constraints. Full automation can be achieved by constructing a suitable order from the solution of
the constraint problem.
The success of Knuth and Bendix’ procedure has led to several adaptations torelated reasoning tasks, such as Inductionless Induction or Rewriting Induction.
We propose a new uniform framework based on constrained equalities. It allows
to easily formulate several completion procedures by simple parameter changes.
But more importantly it also makes it possible to adopt a similar approach as
above, namely reformulating these adaptations as optimization problems. A convenient side effect of this framework is that soundness proofs are simplified, sincenecessary conditions are encoded in the constraint part.
Lastly we investigate confluence of Term Rewriting Systems (TRSs). Testing
confluence automatically is a central property not only for completion, but inother applications as well, such as narrowing or type theory. We present a newconfluence criterion for non-left-linear and non-terminating TRSs. Since it requires joinability of uncomputable extended critical pairs, we provide a new result on unification, which enables full automation of our criterion.
All results presented in this thesis have been implemented and experimentally
evaluated to show their practical effectiveness.

iii

Acknowledgments
I am much indebted to both Associate Professor Nao Hirokawa and Professor
Mizuhito Ogawa for supporting me throughout my studies, for their constantencouragement, and for providing valuable advice. Nao Hirokawa introduced
me into the world of term rewriting, and supervised large parts of my research.
His attitude towards teaching and research has been a great inspiration, andI would like to thank him for his guidance and, an education. I would also
like to thank Associate Professor Xavier Défago, who supervised my “minor
research project” in the PhD Program, and François Bonnet for his cooperation.
I feel very honoured and grateful that all referees, Associate Professor Takahito
Aoto, Professor Aart Middeldorp, Associate Professor Kazuhiro Ogata, Professor
Michio Oyamaguchi, and Assistant Professor Haruhiko Sato accepted to review
this thesis. Professor Aart Middeldorp and Sarah Winkler also provided valuablecomments on Maximal Completion, which helped to significantly improve thepresentation. Last but not least I would like to thank Hiroko and my family andfriends for their moral support.

v

Contents
1

Introduction
1.1 Equational Reasoning and its Challenges . . . . . . . . . . . . . . .
1.2 Overview and Contributions . . . . . . . . . . . . . . . . . . . . . .

9
9
16

2

Preliminaries
2.1 Abstract Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Terms and Substitutions . . . . . . . . . . . . . . . . . . . . . . . . .
2.4 Term Rewriting Systems . . . . . . . . . . . . . . . . . . . . . . . . .
2.5 Equational Problems . . . . . . . . . . . . . . . . . . . . . . . . . . .

21
21
23
25
27
31

3

Completion Procedures
3.1 Knuth-Bendix Completion . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Completion with Termination Tools . . . . . . . . . . . . . . . . . .
3.3 Multi-Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4 Multi-Completion with Termination Tools . . . . . . . . . . . . . . .
3.5 Inductive Proofs by Completion . . . . . . . . . . . . . . . . . . . .

35
35
39
40
43
46

4

Maximal Completion
4.1 Maximality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Automation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

49
50
52
55
58

5

Constrained Equalities
5.1 Constrained Equalities . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2 Constraints for Joinability Problems . . . . . . . . . . . . . . . . . .
5.3 Automation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.5 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

61
62
64
68
70
73

6

Confluence and Relative Termination
6.1 Confluence Criterion . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.2 Correctness of the Criterion . . . . . . . . . . . . . . . . . . . . . . .
6.3 Joinability of Extended Critical Pairs . . . . . . . . . . . . . . . . . .

75
76
79
85

vii

Contents
6.4
6.5
7

Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9092Conclusion and Future Work95

A Experimental Data for Chapter 4

97

B Experimental Data for Chapter 5

101

C Experimental Data for Chapter 6

105

D Maxcomp: Installation and Usage

107

References

110

Index

119

Publications

123

viii

Chapter 1
Introduction

This introduction consists of two parts. The first part provides an informal introduction into equational reasoning based on term rewriting, and associated challenges and open problems. The second part gives an overview of the approaches
taken to tackle these challenges, and lists the contributions of this thesis.

1.1 Equational Reasoning and its Challenges
To express and reason about various facts, several formalisms exist. Very often,
such facts and relationships between them can be very naturally expressed as
equations. For example, addition on natural numbers can be axiomatized by theequational system (ES):1:2:

0+x ≈ xs( x ) + y ≈ s( x + y )We could now ask whether 1 + 0 equals 0 + 1, i.e. whether s(0) + 0 ≈ 0 + s(0)follows from the given axioms. A proof can be constructed by equational reasoning:

9Chapter 1: Introduction

lhs

rhs

s(0) + 0

0 + s(0)↔2 s(0 + 0)
↔1 s(0)↔1 s(0)where ↔i stands for an application of equation i in either direction. There are two
major observations in the above proof: First, the equations of the axiomatization
were applied only from left to right, just directed steps →1 and →2 would havebeen sufficient. We call a directed equation s ≈ t a rule (written s → t), sets ofrules a Term Rewriting System (TRS), and applications of rules to terms rewriting.
In the context of TRSs, we will write i to denote orientation from left to right, andi0 for right to left.
The second major observation is that no semantic insight was needed: Insteadof deriving a proof, we can compute it. Thus, given a set of equations E , insteadof employing equational steps ↔E , the goal is to orient the equations to a TRS R
and employ only →R . In the above example, the TRS {1, 2} suffices to efficiently
construct a proof for any valid equation. This is because it has three important
properties:
1. It is terminating: There exists no term s with infinite sequence s → s1 → . . .
2. It is confluent: For all terms t, s, u such that t ∗ ← s →∗ u, there exists a termv with t →∗ v ∗ ← u. Thus, the result of a computation does not depend on
the order of applications of rewrite rules.
3. The TRS is equivalent to the equational system, i.e. ↔∗E = ↔∗R . Thus two
terms are reachable by equational steps if and only if they are convertible
by rewriting.
Termination implies that for a given term, after finitely many steps, we reach aterm where no rule is applicable — the given term’s normal form. Confluence
implies that this normal form is unique. Equivalence ensures that reachability
by equational steps and reachability by directional steps coincide. We call a TRS
complete for an equational system, if it is terminating, confluent and equivalent to
the ES.
Unfortunately, not always can equational systems be turned into complete
TRSs by just merely orienting its equations to rules. Consider an axiomatization of group-theory EG , consisting of3:

1∗x ≈ xneutral element

4:−1

inverse element

5:

10

∗x ≈1
( x ∗ y) ∗ z ≈ x ∗ (y ∗ z)x

associativity

1.1 Equational Reasoning and its Challenges
and the proof of ( x ∗ 1) ∗ x −1 ≈ 1. We have( x ∗ 1 ) ∗ x −1 ↔ 5 x ∗ (1 ∗ x −1 )↔ 3 x ∗ x −1
↔ 3 1 ∗ ( x ∗ x −1 )
↔4 (( x −1 )−1 ∗ x −1 ) ∗ ( x ∗ x −1 )
↔ 5 ( x −1 ) −1 ∗ ( x −1 ∗ ( x ∗ x −1 )
↔ 5 ( x −1 ) −1 ∗ ( x −1 ∗ x ) ∗ x −1 )
↔ 4 ( x −1 ) −1 ∗ (1 ∗ x −1 )
↔ 3 ( x −1 ) −1 ∗ x −1

↔4 1

Using the TRS {3, 4, 5} misses the proof, since then both ( x ∗ 1) ∗ x −1 and 1 arein normal form. The reason is that {3, 4, 5} is terminating, but neither confluent,
nor equivalent to the ES. The difficulty in finding a complete TRS is, that naively
trying to fix one of the three properties easily leads to violation of another. For
example {3, 4} is both terminating and confluent, but not equivalent to the ES.
{3, 30 , 4, 40 , 5, 50 } is confluent and equivalent to the ES, but clearly not terminating.
Completion
Given an ES, Knuth and Bendix’ [49] ground-breaking completion procedure systematically searches for an equivalent and complete TRS by orienting equations
to rules, while maintaining confluence by resolving local peaks. For example,
their procedure can construct the following complete TRS RG for group-theory:1:1∗x → x6:

1−1 → 12:

x −1 ∗ x → 1

7:( x −1 ) −1 → x( x ∗ y) ∗ z → x ∗ (y ∗ z) 8 :x ∗ x −1 → 1

3:

4 : x −1 ∗ ( x ∗ y ) → y

9:x∗1 → x10 :5:x ∗ ( x −1 ∗ y ) → y( x ∗ y ) −1 → y −1 ∗ x −1

The proof of ( x ∗ 1) ∗ x −1 ≈ x is trivial with the complete TRS, since( x ∗ 1) ∗ x −1 →5 x ∗ x −1 →8 1 = 1.
So far we have only considered computing proofs for valid conjectures. To disprove a conjecture s ≈ t for a given ES E , one has to verify the absence of equational steps to connect s and t, i.e. to show that s ↔∗E t is impossible. Since foreach side of a conjecture potentially infinitely many derivations exist, it is usually
not possible to exhaustively enumerate them.

11Chapter 1: Introduction
One way to disprove a conjecture is to exploit the tight connection of equational
steps and logical entailment. A conjecture is a logical consequence of an ES E , if
and only if all algebraic models of E are also a model of the conjecture. Due toBirkhoff’s theorem [14], both notions of logical entailment and connectedness byequational steps are equivalent: A conjecture s ≈ t is a logical consequence of agiven ES E , if and only if s ↔∗E t holds. Thus one way to disprove a conjecture is
to find a (counter-)model, and apply Birkhoff’s theorem:
Consider again the equations of the ES EG , and take the model M with carrier
set GL2 (R) of invertible 2 × 2-matrices over the field of real numbers



a b
GL2 (R) =a, . . . , d ∈ R and ad − bc 6= 0c dwith the standard matrix operations as interpretations of the function symbols,
namely:






a b
ae + bg a f + bh
e f
∗
=
,
c d M g hce + dg c f + dh

 −1M


1
a b
d −b
=
∗
, and
c d
ad − bc M −c a


1 0
1M =
.
0 1
Then M is a valid model of EG , since for all A, B, C ∈ GL2 (R) the three equations
A ∗M 1M = A, A−1M ∗M A = 1M , and ( A ∗M B) ∗M C = A ∗M ( B ∗M C ) hold.
The conjecture x ∗ y ≈ y ∗ x is not true, since not every group is abelian. In
particular, M is a counter-model, because



 



0 1
0 0
0 0
0 1
∗
6=
∗
.
0 0 M 1 0
1 0 M 0 0
While simpler counter-models for group-theory exist, the construction of acounter-model is in general difficult to automate, as it requires semantic insight
into the ES — most Lie-groups are non-commutative.
On the other hand one can also make use of the following lemma, combining
Birkhoff’s theorem with completion: Given a complete TRS R for an ES E , a
conjecture s ≈ t is a logical consequence of E , if and only if the normal forms ofs and t w.r.t. R are syntactically equal. This very much simplifies the disproof ofx ∗ y ≈ y ∗ x: Both x ∗ y and y ∗ x are in normal form w.r.t. RG , and not syntactically equal. Therefore we can immediately reject the conjecture — without theneed to explicitly construct a counter-model.
Note how all three properties of RG are essential: Confluence implies the
Church-Rosser property ↔∗RG = →∗RG · RG∗ ←, by equivalence ↔∗EG = ↔∗RG holds,

12

1.1 Equational Reasoning and its Challenges
and termination ensures the existence of normal forms and together with confluence their uniqueness. Finally ↔∗EG connects to logical entailment by Birkhoff’s
theorem.
Challenges in Completion
Deciding validity of equations is undecidable in general. Thus it is not surprisingthat we cannot always find a complete TRS for a given ES. But even if a complete
TRS exists, it is no trivial task to find it. Knuth and Bendix’ completion procedureposes several challenges:
1. The procedure is formulated as an iterative algorithm, but its formulation
includes several indeterminism, which have to be resolved in an effective way
to achieve full automation.
2. The procedure assumes a reduction order as an input parameter to ensuretermination. It is in general a highly non-trivial task to find a suitablereduction ordering a priori.
3. Its algorithmic formulation makes it very difficult to distinguish essential
properties from implementational details. This is especially a hindrance,
when trying to extend the procedure to resolve the above two issues.
Inductive Reasoning
Depending on the area of application, the notion of logical entailment and connectedness via equational steps does not capture the properties one is interested
in. Consider the following axiomatization E@ of list-append, that almost verbatim
corresponds to code in functional programming languages:
1:
2:[ ] @ xs ≈ xs
( x :: xs) @ ys ≈ x :: (xs @ ys)

The ES E@ does not logically entail the conjecture3:

xs @ [ ] ≈ xs.

Take the model M with carrier set {0, 1}, and interpretations [ ]M = 0, x ::M
xs = xs, and xs @M ys = ys. One can verify, that M is indeed a model of E@ . But
M is a counter-model of the conjecture, since 1 @M 0 = 0 6= 1.
When executing a program however, one can be sure that the data structures
operated on are lists, and thus any instance of the variables is constructed byusing the operator :: and the empty list [ ]. Taking this into account, one canprove the conjecture xs @ [ ] ≈ xs by induction on these constructor symbols.

13Chapter 1: Introduction
For the proof, we distinguish two cases: If xs is instantiated as [ ], then trivially[ ] @ [ ] = [ ]. On the other hand, if xs has the form x :: xs0 where x and xs0 are
free, we have

↔2
↔3

lhs

rhs

( x :: xs0 ) @ [ ]x :: (xs0 @ [ ])x :: xs0

x :: xs0

Thus the conjecture does not hold in general, but it does hold on all ground instances. Observations on the computation of this proof are similar to the introductory example of addition: Again, we used both equations from E@ and the
hypothesis only from left to right, we could have conducted the proof using
the TRS R@ = {1, 2, 3} instead. The main difference and difficulty compared
to completion is, that extra care is needed to ensure that the application of the
hypothesis is sound. For example, both rule 2 and rule 3 are applicable on theleft-hand side of ( x :: xs0 ) @ [ ] ≈ x :: xs0 . Using rule 3 however leads to unsoundreasoning, since it means self-application of the hypothesis. Another differenceis, that due to its application, we are rarely interested in disproving but rather
in proving conjectures. To compute a proof, one needs to ensure that all groundinstances of both sides of the conjecture are joinable by rewrite steps of the TRS,
and by sound application of rewrite steps using the hypothesis. Confluence of
the TRS together with the hypothesis can be a sufficient criterion to ensure that,
but it is not a necessary one, and in practice usually too strong.
Challenges in Inductive Reasoning
Inductive reasoning is considered to be even more challenging to automate thanstandard equational reasoning. For a more in-depth treatment, we refer to [36],but mention the following issues:
1. The proof strategy. Proofs usually have a recursive structure, yet it is notclear when and how to soundly apply the hypothesis. Since confluence,and even termination can be too strong properties to assume, it is also not
clear which rewrite strategy should be applied.
2. The need of lemmata. Very often, direct proof attempts fail, and must be
split up into several sub-goals, for which additional lemmata are needed.
Since this usually requires semantic insight, it is very challenging to identify
such sub-goals and generate appropriate lemmata automatically.
3. The lack of an expressive framework. Different inductive proof techniques
exist. But identifying their essential properties is difficult, as soundness is14

1.1 Equational Reasoning and its Challenges
left-linear

terminating

non-left-linear

Knuth & Bendix [49]

our criterion (Chapter 6)
Jouannoud & Kirchner [44]non-terminating

Rosen [64]Huet [39]Toyama [77]van Oostrom [80]Hirokawa & Middeldorp [38]Decomposition Criteria[5, 58, 76]

Gomi et al [33]Sakai & Ogawa [65]Figure 1.1: A non-exhaustive overview of confluence criteria.
established by ensuring abstract joinability requirements on ground terms,
which are hard to express and reason about.
Confluence
Confluence is an important property in various domains. For TRSs, confluence is equivalent to the Church-Rosser property ↔∗ ⊆ →∗ · ∗ ←. Church andRosser [16] investigated this property to ensure consistency of combinatory logic
and the λ-calculus. Both form the foundation for the development of functional
programming languages such as SML [55], OCaml1 or Haskell [61]. Other areasof application include narrowing [24, 42] and type safety [73].
From the perspective of equational reasoning, confluence together with termination ensures completeness. Both conditions impose severe restrictions on
the TRS, and naturally one wants to relax both of them. Relaxing the confluence condition is however almost impossible, since it is tied so closely to theconcept of orienting equations to rules. On the other hand confluence implies↔∗R ⊆ →∗R · R∗ ←. Even if termination does not hold, this still suggests a simple
1 http://caml.inria.fr

15

Chapter 1: Introductionm ← with increasing n and m.
semi-decision procedure by enumerating →nR · R
Suitable strategies to apply rewrite rules can help to reduce the size of the searchtree significantly. Thus it is more promising to relax the termination condition,and identify criteria for confluence that do not rely on it.

Challenges to Develop Confluence Criteria
Knuth and Bendix [49] showed that confluence of terminating TRSs is decidable
by testing joinability of so-called critical pairs. For non-terminating TRSs, very
often syntactical criteria are employed, in particular left-linearity, i.e. each variable in a left-hand side of a rule may occur only once. A famous result due toRosen [64] is that a left-linear TRS without critical pairs is confluent. However
the fact that the complete TRS RG for group-theory includes non-left-linear rules
already gives a hint that this is a too strong property to presuppose in practice.
We list as challenges:
1. Proving confluence of both non-left-linear and non-terminating TRSs remains
extremely difficult, and only few results exist. One reason is that noneof the notions and techniques, for example critical pairs, that are used inshowing confluence of terminating or left-linear TRSs are suitable in the
non-left-linear and non-terminating case.
2. Extending these notions can lead to new criteria, but often such extensions
face the problem of computability. For example, extending the notion of critical pairs quickly leads to infinite sets of equations that are uncomputablein general. Thus, despite developing criteria, automation is hard to obtain.

1.2 Overview and Contributions
This thesis is structured as follows: Chapter 2 is an introduction to term rewriting
systems. First, abstract reduction systems are introduced. Properties such asconfluence and termination can already be defined on this abstract level, andwill be used when later specializing the notion of abstract reduction systems toterm rewriting systems. Also formally introduced are several kinds of equational
problems that will be treated in the later chapters, namely equational reasoning
and inductive reasoning.
Chapter 3 recalls existing completion procedures. The original Knuth-Bendix
completion procedure and Huet’s algorithm [40] are introduced, as well as its
reformulation by means of inference rules [12]. We also recollect approaches that
increase the power of the original algorithm by automatically finding a suitablereduction ordering, such as Multi-Completion [51], Completion with Termination
Tools [83], and Multi-Completion with Termination Tools [68, 85].

16

1.2 Overview and Contributions
During the early 2000’s, significant progress has been made in automated constraint solving. In a lot of areas, encoding problems as boolean constraints andsolving them with SAT solvers has turned out to be more effective than the development of dedicated algorithms, and have largely replaced traditional approaches. Here we mention bounded model checking [13] and termination analysis of TRSs [17, 26, 70, 88]. To obtain efficient encodings to SAT, the search
space of the underlying problem has to be known, and representable by a finite
number of constraints. Unfortunately, in the case of completion, the search spacethat includes all complete TRSs is usually unknown in advance. Therefore it is
non-trivial to directly encode the completion problem as a satisfiability problem.
Inspired by the progress in satisfiability solving, also several tools for MaxSAT
solving appeared. Compared to SAT solving however, few of these systems haveseen application outside their very domain. In Chapter 4, we present maximal
completion. We characterize completion as an optimization problem, where thegoal is to find an optimal TRS among a set of (exponentially) many. This task
can be encoded as a maximal satisfiability problem and automatically solved by
a MaxSAT (or MaxSMT) solver. We relate maximal completion with existing
completion procedures, and compare our implementation Maxcomp with stateof-the-art completion tools.
Maximality is the key ingredient in maximal completion. To apply maximality
in adaptations of completion for equational reasoning, we propose a framework
for equational reasoning based on constrained equalities in Chapter 5. This framework is universal enough to formulate various joinability requirements for equational reasoning tasks, including the more complex requirements of methods for
inductive reasoning, such as inductionless induction and rewriting induction.
Most importantly it enables us to reformulate the various joinability conditions
as optimization problems and thus exploit maximality. Experiments for inductive
proof methods such as rewriting induction show practical effectiveness. Additionally the framework also allows to recover inter-reduction for completion thatwas lost in the abstraction of maximal completion. Experimental evaluation however shows that for completion the approach used in maximal completion is more
efficient.
For non-terminating TRSs, several criteria exist to establish confluence. Figure 1.1 gives an non-exhaustive overview of confluence criteria on four classesof TRSs related to our setting. Note here that criteria for non-terminating TRSs
can of course also be applied to terminating ones. Likewise those for non-leftlinear TRSs apply to left-linear ones as well. As mentioned, for terminating TRSs
confluence is decidable by testing joinability of critical pairs, which are inducedby overlaps. Criteria for the case of non-terminating and left-linear TRSs usuallybuild up on the orthogonality result by Rosen [64], either by a more precise analysis of overlaps [35, 38, 39, 77, 80] or by employing relative termination. Approaches

17Chapter 1: Introduction
for the case of non-termination and non-confluence can be roughly classified into
three categories:
1. By generalizing the notion of overlaps, one can formulate direct criteria [31,65] that ensure confluence. Usually, strong syntactic restrictions are imposed to handle the very complex overlap analysis.
2. By decomposing the TRS [5, 25, 58, 59, 76] into smaller ones, one can employ
existing criteria to show confluence for each of them. Modularity of thedecomposition then ensures that the union remains confluent.
3. Criteria that relax termination requirements to relative termination. To apply equational reasoning for theories where no complete TRSs exists, Jouannaud and Kirchner gave a confluence criterion for the Church-Rosser modulo property [44] based on so called extended critical pairs. Later Geser [27]analyzed their proof and gave a criterion based on purely syntactic criticalpairs.
In Chapter 6 we first recall some definitions and techniques, such as extended
critical pairs, to build our tool-set for later proofs. Then we introduce our confluence criterion for non-left-linear and non-terminating TRSs, which also relies on
relative termination. Similar to Jouannaud and Kirchner’s criterion, it requires tocheck joinability of (uncomputable) extended critical pairs, but we show that for
certain classes of TRSs, joinability of (computable) syntactic critical pairs suffices.
We then compare our criterion with existing results, and provide experimental
data.
Contributions
As main contributions of this thesis we list:
1. Maximal completion. We show that completion can be characterized as an optimization problem. In contrast to existing procedures, our reformulation
does not contain any algorithmic aspect. It abstracts away from implementational details by encoding the completion requirements to constraints. It isless reliant on heuristics to resolve indeterminism than existing procedures,and suitable reduction orderings are constructed automatically based on
solutions of the constraint problem.
2. Constrained Equalities. This framework allows not only to uniformly express the joinability requirements of completion and several proceduresfor inductive reasoning, but more importantly also makes it possible toreformulate these procedures as optimization problems, similar to maximal completion. While for completion itself practically not as efficient as18

1.2 Overview and Contributions
maximal completion, it provides a powerful technique to implement fully
automated inductive theorem provers. As a theoretical interest, it recovers
inter-reduction in completion, an optimization technique that is lost in the
abstraction used in maximal completion.
3. A new confluence criterion for non-left-linear and non-terminating TRSs. Ourcriterion is based on moderate syntactic restrictions and relative termination, and requires joinability of extended critical pairs. In order to overcome
the uncomputability of extended critical pairs, we provide a new result on
equational unification, and with it, our confluence criterion can be fully automated.
4. All of the above approaches have been implemented and experimentally
evaluated to show their effectiveness. Moreover, we provide the free completion tool Maxcomp, which is based on maximal completion.
All results are included in the papers [4, 46, 47].

19

Chapter 2
Preliminaries

In this chapter we formally introduce term-rewriting, and the equational problems that we will tackle. We restrict us to the essential definitions and properties
needed for the later chapters. For full proofs and a more gentle, comprehensive introduction to term-rewriting we refer to [10, 60, 75], and [9] (the latter inGerman).

2.1 Abstract Rewriting
A (binary) relation → on a set A is a subset of A × A. Given two relations →1
and →2 on A, the composition →1 · →2 is defined as{( x, z) ∈ A | there exists y ∈ A such that x →1 y and y →2 z}.
Definition 2.1.1. An Abstract Rewrite System (ARS) A = ( A, h→α iα∈ I ) is a tuple
consisting of a set A and a set of relations →α on A, where I is a set of labels. We say→α is a reduction relation labeled with α. The reduction relation →A of A is defined as

→A =

[

→α .

α∈ I

We sometimes write → instead of →A , if A is clear from the context. In the following definitions, we assume I to be a singleton and simply write A = ( A, →).

21

Chapter 2: Preliminaries
One motivation to introduce labels is that it is sometimes useful to consider( A, h→α iα∈ I ) as a representation of ( A, →). In particular the decreasing diagram
technique [79] used in Chapter 6 will make use of this.
Definition 2.1.2. Let A = ( A, →) be an ARS. We define the following notions:→0 = {( a, a) | a ∈ A}

identity→ i +1 = → i · →(i + 1)-fold composition→+ =transitive closure

→

=

→∗
←
↔
↔+
↔∗
↓

[

→i

i >0
0

= → ∪→======→0 ∪ → +{(b, a) | ( a, b) ∈ →}
→∪←
(↔)+
(↔)∗
→∗ · ∗ ←reflexive closuretransitive reflexive closure
inverse relation
symmetric closuretransitive symmetric closurereflexive transitive symmetric closurejoin relation

We will make use of the following terminology:• We will write a → b if ( a, b) ∈ →, and say that a rewrites to b and b is areduct of a.
• We say that a and b are joinable, if a ↓ b.
We now define the central notions of confluence and termination for ARSs andinvestigate their relation with normal forms.
Definition 2.1.3. Let A = ( A, →) be an ARS.
1. a ∈ A is in normal form (w.r.t. →), if there exists no b such that a → b.
2. b is a normal form of a, if a →∗ b, and b is in normal form. If a has a uniquenormal form b, we write a↓A for b. In some contexts, we will ambiguously writea↓A to denote a specific normal form. The set of normal forms of A is written
NF( A) or NF(→), if A is clear from the context.
3. A is normalizing, if for every a ∈ A there exists a b ∈ A such that b is a normal
from of a.
4. A is uniquely normalizing, if for every a ∈ A there exists exactly one b ∈ Asuch that b is a normal form of a.
5. A is terminating, if there exists no infinite sequence a0 → a1 → a2 → a3 → . . .

22

2.2 Orders
Definition 2.1.4. Let A = ( A, →) be an ARS.
1. A is Church-Rosser if ↔∗ ⊆ ↓ .
2. A is confluent if ∗ ← · →∗ ⊆ ↓ .
3. A is locally confluent (or weakly Church-Rosser) if ← · → ⊆ ↓ .
Lemma 2.1.5. A relation → is confluent if and only if it is Church-Rosser.
Termination localizes the confluence condition.
Lemma 2.1.6 (Newman [56]). A terminating ARS A is confluent if and only if it islocally confluent.
Definition 2.1.7. An ARS A is complete, if it is confluent and terminating.
Confluence and unique normal forms are connected:
Lemma 2.1.8. Let A be an ARS.
• Suppose A is confluent. Then each a ∈ A has at most one normal form.
• Suppose A is complete. Then A is uniquely normalizing.

Completeness of an ARS A provides a way to test a ↔∗A b.
Theorem 2.1.9. Let A be a complete ARS. Then a ↔∗A b if and only if a↓A = b↓A .

2.2 Orders
A binary relation → on A is well-founded, if there exists no infinite sequence
a0 → a1 → a2 → · · · of elements. One might wonder, why we call it wellfounded and not, like ARSs ( A, →) without infinite sequence a0 → a1 → a2 →. . ., terminating. It is convenient to use a separate terminology here, since welater specialize ARSs to term rewriting systems (TRSs), and employ certain kindsof well-founded orders to automatically show termination of TRSs.
Definition 2.2.1. A binary relation on A is
1. a strict order, if it is irreflexive and transitive
2. a preorder, if it is reflexive and transitive and3. a partial order, if it is reflexive, transitive and anti-symmetric.

23

Chapter 2: Preliminaries
Definition 2.2.2. A > strict order on A is
1. a total order, if for all a, b ∈ A we have a > b, b > a or a = b.
2. a well-founded order, if > is well-founded and3. a well-order, if it is both total and well-founded.
We introduce two extensions of strict orders. The first is the lexicographic
extension.
Definition 2.2.3. Let > be a strict order on A. The lexicographic extension >lex on
An is defined as: (s1 , . . . , sn ) >lex (t1 , . . . , tn ) if and only if there exists some i with0 ≤ i < n such that s j = t j for all 1 ≤ j ≤ i and si+1 > ti+1 .
The lexicographic extension preserves well-foundedness.
Theorem 2.2.4 ([10]). Let > be a strict ordering. The lexicographic extension >lex iswell-founded if > is well-founded.
The second extension is based on multisets.
Definition 2.2.5. Let A be a set. A multiset M over A is a function M : A → N.
A multiset M is finite, if there are only finitely many x such that M( x ) > 0. The setof all finite multisets over A is denoted by M( A). Let a1 , . . . , an be elements of A. We
write {{ a1 , . . . , an }} for the multiset M defined as follows: M( a) denotes the size of theset {i | 1 ≤ i ≤ n, ai = a}. Let M and N be multisets. The following operations aredefined:• x ∈ M, if M ( x ) > 0• M ⊆ N, if M ( x ) ≤ N ( x ) for all x ∈ A.
• M ∪ N stands for x 7→ M ( x ) + N ( x ), and• M \ N stands for x 7→ max{0, M( x ) − N ( x )}.
Definition 2.2.6. Let > be an order on A. The multiset extension >mul of > is definedon M( A) as:
M >mul N if and only if there exists X, Y ∈ M( A) such thata) {{ }} 6= X ⊆ M,b) N = ( M \ X ) ∪ Y, andc) for every y ∈ Y there exists an x ∈ X with x > y
Theorem 2.2.7 ([10]). Let > be a strict ordering. The multiset extension >mul is wellfounded if and only if > is well-founded.

24

2.3 Terms and Substitutions

2.3 Terms and Substitutions
Definition 2.3.1. A signature F is a countable set of function symbols, where eachf ∈ F is associated with a natural number denoting its arity (the number of arguments).
We write f (n) when we want to explicitly express that the arity of f is n. A function
symbol of arity zero is called a constant.
Definition 2.3.2. Let F be a signature and V be a countable set of variables withF ∩ V = ∅. The set of terms T (F , V ) over F and V is the smallest set such that• V ⊆ T (F , V ), and• if f (n) ∈ F and t1 , . . . , tn ∈ T (F , V ), then f (t1 , . . . , tn ) ∈ T (F , V ).
When denoting specific function symbols f, g, . . . we will use a gothic (sansserif) font, and for variables x, y, . . . we will use italics.
Definition 2.3.3. Let t ∈ T (F , V ) be a term. V ar(t) denotes the set of variables
occurring in t:
if t is a variable
{t}nV ar(t) = [ V ar(ti ) if t = f (t1 , . . . , tn )i =1Similarly, F un(t) denotes the set of function symbols (including constants) of t:
if t is a variable∅n[
F un(t) ={ f } ∪ F un(ti ) if t = f (t1 , . . . , tn )i =1

Definition 2.3.4. For t ∈ T (F , V ) the set of positions P os(t) is defined as({ε}
if t is a variable
P os(t) ={ε} ∪ {i.q | 1 ≤ i ≤ n, q ∈ P os(ti )} if t = f (t1 , . . . , tn )Here ε denotes the empty string. A position is thus a sequence of integers separated by
the . symbol. The position ε is the root position. The root symbol of t is defined as:(
t if t is a variableroot(t) =f if t = f (t1 , . . . , tn )A position describes the path from the root to a specific subterm.
Definition 2.3.5. Let t be a term and p ∈ P os(t). The subterm t| p of t at position p isdefined as:(t
if p = εt| p =
ti |q if p = i.q and t = f (t1 , . . . , ti , . . . , tn )25

Chapter 2: Preliminaries
We define P osF (t) as the set { p ∈ P os(t) | root(t| p ) ∈ F }. With t[u] p we denote theoperation of replacing the subterm t| p of t at p with the term u:(u
if p = εt[u] p =f (t1 , . . . , ti [u]q , . . . , tn ) if p = i.q and t = f (t1 , . . . , tn )A term u is called a subterm of a term t, if there exists a position p ∈ P os(t), such thatu = t| p . Given positions p, q, and o, we write p\q for o if p = q.o. Let x be a variable.
We will write |t| x for { p | p ∈ P os(t) and t| p = x } , i.e. the number of occurrences of
x in t.
Definition 2.3.6. A term t is
• a ground term if V ar(t) = ∅. Instead of T (F , ∅) we sometimes write T (F ) todenote the set of all ground terms over the signature F , and• linear if each variable appears only once, i.e. if for all x ∈ V ar(t), we have |t| x = 1.
The size |t| of a term is defined as |P os(t)|, that is the number of functions
symbols and variables occurring in it.
Definition 2.3.7. Let F be a signature, and let  denote a special constant symbol,
called the hole. A context over the union of the signature and the hole F ∪ {} is aterm C, such that C contains exactly one hole, i.e. { p ∈ P os(t) | t| p = } = 1. The
application C [t] of a context C on a term t is defined as:(t
if C = C [t] =0f (t1 , . . . , C [t], . . . , tn ) if C = f (t1 , . . . , C 0 , . . . , tn )Here C 0 denotes a context.
Definition 2.3.8. Let F be a signature, and V be a countable set of variables, such thatF ∩ V = ∅. A substitution σ over T (F , V ) is a function V → T (F , V ), such thatthe domain Dom(σ)
Dom(σ) = { x ∈ V | σ( x ) 6= x }is finite. When referring to a specific substitution σ, we sometimes write it as{ x1 7 → t1 , x2 7 → t2 , . . . , x n 7 → t n }using the finiteness of the domain. The application σ (t) of a substitution σ on a term t isdefined as follows:(σ(t)
if t ∈ V
σ(t) =f (σ(t1 ), . . . , σ (tn )) if t = f (t1 , . . . , tn )26

2.4 Term Rewriting Systems
We say σ(t) is an instance of t. The composition στ of two substitutions σ and τ
is defined as (στ )( x ) = σ (τ ( x )). A substitution σ : V → V is called a variable
substitution, and a bijective variable substitution is called a variable renaming. A
substitution σ with σ( x ) ∈ T (F , ∅) for all x ∈ V ar(t) is called a ground substitution
on t. A substitution σ is a ground substitution on an equation s ≈ t, if it is both aground substitution on s and on t. Finally, we will often write tσ instead of σ(t).
Definition 2.3.9. Let s and t be terms. We define the following notions:• s and t are syntactically unifiable if there exists a substitution σ with σ(s) = σ (t).
• If σ(s) = σ (t) holds for a substitution σ, then we call σ a unifier of s and t.
• A unifier σ of s and t is a most general unifier (mgu) if for every unifier τ of sand t there exists some substitution ρ such that ρσ = τ.
Syntactical unifiability is decidable ([10, 63]), and unifiable terms admit anmgu, which is unique up to variable renamings. We will extend the notion ofunifiability to equational unifiability in Chapter 6, where these extensions andseveral of their properties will be used. When speaking of unifiability and unifiers, we usually mean syntactic unifiability and syntactic unifiers, unless noted
otherwise.

2.4 Term Rewriting Systems
Definition 2.4.1. Let → be a relation on terms. It is• monotonic (or closed under contexts) if C [s] → C [t] holds for all s and t withs → t and all contexts C,• stable (or closed under substitutions) if sσ → tσ holds for all s and t withs → t and all substitutions σ,• a rewrite relation if it is monotonic and stable,• a rewrite order if it is a strict order, monotonic and stable, and• a reduction order if it is a well-founded rewrite order.
Definition 2.4.2. A Term Rewriting System (TRS) is a tuple (F , R) consisting of asignature F and a set R ⊆ T (F , V ) × T (F , V ) of rewrite rules. A rewrite rule (`, r )must satisfy• ` 6∈ V , and• V ar(`) ⊇ V ar(r ).

27

Chapter 2: Preliminaries
We write ` → r instead of (`, r ). The rewrite relation →R of a TRS (F , R) is definedas: s →R t if there exists a position p ∈ P os(s), a substitution σ, and a rule ` → r ∈ Rsuch that s = s[`σ ] p and t = s[rσ] p . We say s →R t is a rewrite step. A rule `0 → r 0
is a variant of a rule ` → r, if there exists a variable renaming σ, such that `σ = `0 andrσ = r 0 .
By definition, s →R t implies the existence of a position p ∈ P os(s), a rule
` → r ∈ R such that s = s[`σ] p and t = s[rσ] p . When we want to make theppposition and/or rule explicit, we will write s −→`→r t, s −→R t or s →`→r t.
We often omit F when referring to a TRS, simply write R and assume, unlessotherwise noted, the signature of R to consist of all function symbols occurringin R.
Definition 2.4.3. Let ` → r be a rule of the TRS R. It is called• left-linear if ` is linear,• right-linear if r is linear,• linear if both ` and r are linear,• collapsing, if r ∈ V , and• erasing if not each variable that occurs in the left-hand side also occurs at least
once in the right-hand side.
Note that all properties of ARSs, in particular confluence and termination tradeover to TRS when treating a TRS R with signature F as an ARS over the set ofterms and relation →R , i.e. as the ARS (T (F , V ), →R ). In general, confluenceand termination or TRSs are undecidable [41, 10]. But several sufficient criteria
to detect confluence of a TRS exist, which are based on overlaps:
Definition 2.4.4. Let R1 and R2 be TRSs. Then an overlap of R1 on R2 is a tuple(`1 → r1 , p, `2 → r2 )σ consisting of a position p ∈ P osF (`2 ), a substitution σ, andvariants of rules `1 → r1 ∈ R1 and `2 → r2 ∈ R2 , such that following conditions hold:• V ar(`1 , r1 ) ∩ V ar(`2 , r2 ) = ∅,• `2 | p 6 ∈ V ,• if `1 → r1 is a renaming of `2 → r2 , then p 6= ε, and• `2 | p and `1 unify with mgu σ.
This overlap induces the critical pair `2 σ[r1 σ ] p ← o → r2 σ. A critical pair is trivial,if `2 σ[r1 σ ] p = r2 σ. Given a TRSs R1 and R2 , the set of critical pairs generated by
all overlaps of R1 on R2 and all overlaps on R2 on R1 is written as CP(R1 , R2 ).
We write CP(R) for CP(R, R). A TRS R is non-overlapping if CP(R) = ∅. A
non-overlapping and left-linear TRS is called orthogonal.

28

2.4 Term Rewriting Systems
We remark that a more general notion of overlap and critical pair exists that
subsumes the above definition. We will make use of this more general notion
when introducing our confluence criterion in Chapter 6. Since we do consider
these notions non-standard, we will not treat them here but define and discussthem when needed in Chapter 6.
The following result by Knuth and Bendix shows decidability of confluence forterminating TRSs.
Theorem 2.4.5 (Knuth and Bendix, [49]). Let R be a terminating TRS. Then R is
confluent if and only if all critical pairs are joinable, that is CP(R) ⊆ ↓R .
For non-terminating TRSs, the most famous result is due to Rosen:
Theorem 2.4.6 (Rosen, [64]). Every orthogonal TRS is confluent.
Similarly, criteria exist to detect termination of a TRS. Several are based on
reduction orders.
Theorem 2.4.7. A TRS R is terminating if and only if there exists a reduction order >with ` > r for all ` → r ∈ R.
We will introduce three orders to show termination. They are all instances ofsimplification orders.
Definition 2.4.8. The strict subterm relation B ⊆ T (F , V ) × T (F , V ) is defined as:s B t if there exists a position p 6= ε such that s| p = t.
Definition 2.4.9. A rewrite order > is a simplification order if B ⊆ >.
Simplification orders ensure termination:
Theorem 2.4.10 ([20, 21]). Let F be a finite signature and V a countable set of variables.
Every simplification order on T (F , V ) is a reduction order.
In the following, a precedence on F is a strict ordering on F .
Definition 2.4.11. A status τ is a function that maps every f ∈ F to either mul orlexπ . Here π is a permutation on {1, . . . , n}, where n is the arity of f .
Let > be a partial order on T (F , V ), and f ∈ F be of arity n. The partial order >τ ( f )is defined on sequences of length n of terms as follows.

(s1 , . . . , sn ) >τ ( f ) (t1 , . . . , tn ) is defined as({{s1 , . . . , sn }} >mul {{t1 , . . . , tn }}if τ ( f ) = mul(s1 , . . . , sn ) >lex (tπ (1) , . . . , tπ (n) ) if τ ( f ) = lexπ .

29

Chapter 2: Preliminaries
Definition 2.4.12. Let F be a signature, V a countable set of variables,  be a wellfounded precedence, and τ be a status. The recursive path order >rpo ⊆ T (F , V ) ×
T (F , V ) is defined as as s >rpo t if s has the form f (s1 , . . . , sn ) and1. si = t or si >rpo t for some 1 ≤ i ≤ n, or
2. t = g(t1 , . . . , tm ), s >rpo ti for all 1 ≤ i ≤ m, and eithera) f  g orτ( f )b) f = g and (s1 , . . . , sn ) >rpo (t1 , . . . , tm ).
When requiring τ ( f ) = mul for all function symbols, the order is called themultiset path order (MPO). It was originally introduced by Dershowitz [21]. The
lexicographic path order (LPO), introduced by Kamin and Lévy [45], is obtainedby requiring τ ( f ) = lexπ for all function symbols. The recursive path order
combines these two ideas of showing termination of TRSs.
Theorem 2.4.13 ([75]). Let F be a signature, V be a countable set of variables,  be awell-founded precedence, and τ be a status on F . Then >rpo is a simplification order on
T (F , V ).
The next order is due to Knuth and Bendix [49]. Below N denotes the natural
numbers.
Definition 2.4.14. A weight function for a signature F is a tuple (w, w0 ), where w isa function w : F → N and w0 ∈ N is a constant such that w0 > 0 and w(c) ≥ w0 for
all constants c ∈ F . Given a signature F and a weight-function (w, w0 ), the weight ofa term t ∈ T (F , V ) is defined as:
if t ∈ V w0
nw(t) =w( f ) + ∑ w(ti ) if t = f (t1 , . . . , tn )i =1

A weight function (w, w0 ) is admissible for a precedence  if f  g for all function
symbols g whenever f is a unary function symbol with w( f ) = 0.
In the next definition we write F n for the set of all n-ary function symbols.
Definition 2.4.15. Let  be a well-founded precedence and (w, w0 ) an admissible weightfunction. The Knuth-Bendix order (KBO) is defined as s >kbo t if |s| x ≥ |t| x for allx ∈ V and either
1. w(s) > w(t), or
2. w(s) = w(t) and one of the following conditions hold:30

2.5 Equational Problemsa) there is a function symbol f ∈ F 1 , a variable x and an integer n such thats = f n ( x ) and t = x, orb) s = f (s1 , . . . , sn ), t = f (t1 , . . . , tn ), and there exists an i with 1 ≤ i ≤ nsuch that s1 = t1 , . . . , si−1 = ti−1 and si >kbo ti , orc) s = f (s1 , . . . , sn ), t = g(t1 , . . . , tn ) and f  g.
Theorem 2.4.16 ([49]). Let  be a well-founded precedence on F , and (w, w0 ) an admissible weight-function. Then >kbo generated by  and (w, w0 ) is a simplification
order.
Sorted Term Rewriting Systems
Definition 2.4.17. Let S be a non-empty set of sorts. An S -sorted signature is acountable set of function symbols F , where each f ∈ F of arity n is associated with thefunction signature sig( f ) ∈ S n+1 , where sig is a function sig : F → S ∗ .
Here components from 1 to n of sig provide the sort of each argument, andthe n + 1-th component is the sort of the result of the function. We will write
f : s1 × · · · × sn → sn+1 when f has the signature (s1 , . . . , sn+1 ).
Definition 2.4.18. An S -sorted set A is a family of sets { As }s∈S . For an S -sorted set
V of variables with Vs ∩ Vt = ∅ for all s 6= t, let T (F , V )s denote the set of terms withsort s over F and V , defined inductively byx ∈ Vsx ∈ T (F , V )s

f ∈F

f : s1 × · · · × sn → s ti ∈ T (F , V )sif (t1 , . . . , tn ) ∈ T (F , V )sThis yields the S -sorted set T (F , V ) = s∈S T (F , V )s . We associate with each term
its sort, i.e. the sort of a term t is s, if t ∈ T (F , V )s . An S -sorted TRS R is a TRS
where for each rule ` → r ∈ R, the terms ` and r are of the same sort.
S

All notions for unsorted TRSs are lifted to sorted TRSs by limiting terms towell-sorted ones. Sorts are distinguished frequently in inductive theorem proving. In examples however we often consider TRSs with only one sort, and identify
them with TRSs.

2.5 Equational Problems
Definition 2.5.1. Let s and t be terms over T (F , V ). An equation is a pair of terms(s, t). We usually write s ≈ t. A set of equations is called an equational system (ES).
Definition 2.5.2. Let F be a signature. A tuple A = ( A, { f A } f ∈F ) is called an F algebra. Here

31

Chapter 2: Preliminaries• A 6= ∅ is a set, called the carrier or universe• { f A } f ∈F is a family of functions, called interpretations of the function symbols. Each f is assigned a function f A : An → A, where n is the arity of f .
Let α : V → A be a variable assignment. An F -algebra together with a variableassignment induces an evaluation [α]A (t) of a term t as follows(α(t)
if t ∈ V[α]A (t) =f A ([α]A (t1 ), . . . , [α]A (tn )) if t = f (t1 , . . . , tn )Definition 2.5.3. Let s ≈ t be an equation over a signature F .
• An F -algebra A = ( A, { f A } f ∈F ) models s ≈ t, written A |= s ≈ t, if[α]A (s) = [α]A (t) for all variable assignments α.
• An F -algebra A is a model of an ES E , written A |= E , if A |= s ≈ t for alls ≈ t ∈ E.
• The equation s ≈ t follows from an ES E (is valid, is true in an ES E ), written
E |= s ≈ t, if A |= s ≈ t for all algebras A with A |= E .
• The relation ≈E ⊆ T (F , V ) × T (F , V ) is defined as s ≈E t if E |= s ≈ t.
• Given an ES E , and an equation s ≈ t, the question whether s ≈ t follows from E
is called the word problem.
Definition 2.5.4. The equational step relation →E ⊆ T (F , V ) × T (F , V ) is defined
as s →E t if there exist a position p ∈ P os(s), a substitution σ, and an equationu ≈ v ∈ E such that s = s[uσ] p and t = s[vσ] p . Here E is an ES. We say s ≈ t can be
deduced from E , if s ↔∗E t.
Theorem 2.5.5 (Birkhoff [14]). Let E be an ES, and s ≈ t an equation. E |= s ≈ t if
and only if s ↔∗E t.
Using Birkhoff’s theorem, one can already construct a semi-decision procedure for s ↔∗E t, since ↔∗E is recursively enumerable. In practice however, thisapproach does not work due to the sheer size of possible derivations. For example if two terms s and t are connected by ten equational steps, and if in each step
four equations are applicable, the search tree has already 410 = 1048576 nodes.
Here, equivalent complete TRSs come in handy.
Definition 2.5.6. Let E be an ES and R be a TRS over a signature F and set of variables
V . The TRS R is equivalent to E if ↔∗R = ↔∗E .
To test equivalence of ↔∗R and ↔∗E , it suffices to check equivalence only w.r.t.
to equations and rules:32

2.5 Equational Problems
Lemma 2.5.7. Let E be an ES and R a TRS over a signature F and set of variables V .
Then R is equivalent to E if and only if ` ↔∗E r holds for every ` → r ∈ R, and s ↔∗R t
holds for every s ≈ t ∈ E .
We will use the following notion throughout the rest of this thesis.
Definition 2.5.8. A TRS R is complete for an ES E , if R is complete and equivalent
to E .
We now arrive at a central theorem, that builds the foundation for equational
theorem proving.
Theorem 2.5.9. Let R be a complete TRS for E . Then E |= s ≈ t iff s↓R = t↓R .
Proof.

iff
iff
iff

E |= s ≈ t
s ↔∗E ts ↔∗R ts↓R = t↓R

by Theorem 2.5.5 (Birkhoff)by equivalence of R and E
by Theorem 2.1.9

Definition 2.5.10. Let E be an ES over a signature F and set of variables V , ands ≈ t an equation. Then s ≈ t is an inductive theorem of E , written E `i s ≈ t, if
E |= sσg ≈ tσg for all ground substitutions σg on s ≈ t.
Using Birkhoff’s theorem, one can reduce the question E `i s ≈ t of inductive
validity to the question whether sσg ↔∗E tσg holds for all substitutions σg thatare ground both on s and t. However unlike for completion as in Theorem 2.5.9,
there exists no definitive single characterization of a suitable TRS R for inductive
theorem proving. The question on how to express the requirements of a suitable
TRS R that ensures joinability on ground terms of a conjecture s ≈ t will be thesubject of Chapter 5.

33

Chapter 3
Completion Procedures

Given an equational set E , completion procedures try to construct a complete(confluent and terminating) TRS R that is equivalent for E . By Theorem 2.4.5,
confluence is decidable for terminating TRSs. Completion procedures thus try to
first compute a terminating candidate TRS, and then test its confluence. Therefore ensuring termination is of central importance. All extensions of the original
procedure have in common that they focus on and try to increase the capabilityof showing termination. In this chapter we briefly recall these extensions andillustrate their workings with small examples.

3.1 Knuth-Bendix Completion
Knuth and Bendix’ completion procedure was the first to employ critical pairs tofind a complete TRS. It was originally formulated in procedural form, which islisted as Algorithm 1.
The procedure takes as input not only an equational system E but also a reduction order >, and operates on a set of equations Ei , initially E , and a set ofrules Ri , initially empty. In each iteration, an equation from Ei is selected by aselection heuristic. Then both sides of the equation are rewritten to some normal
form with respect to the current Ri . If the normal forms are syntactically equal,
the equation is removed from Ei , and the iteration continues. Otherwise, if the35

Chapter 3: Completion Procedureschosen normal forms for each side are incomparable, the algorithm stops with
failure. If they are comparable in the ordering however, the original equationis removed from Ei , the normalized equation is oriented, and critical pairs w.r.t.
the new rule and Ri are added to Ei . The new rule is added to Ri and the next
iteration starts.
Algorithm 1 Knuth-Bendix Completion
Input: an equational system E and a reduction order >Output: a TRS R or FAIL
1: procedure KB-Complete
2:
R0 : = ∅3:
E0 : = E
4:i := 05:while Ei 6= ∅ do6:
select s ≈ t ∈ Ei
7:s 0 ≈ t 0 : = s ↓ Ri ≈ t ↓ Ri
8:
if s0 = t0 then9:
R i +1 : = R i
10:
E i +1 : = E i \ { s ≈ t }
11:
else
12:
if s0 > t0 then13:
` → r := s0 → t0
14:
else
15:
if t0 > s0 then16:
` → r := t0 → s0
17:
else
18:

FAIL

end if20:
end if21:
Ri+1 := Ri ∪ {` → r }22:
Ei+1 := Ei ∪ CP(Ri ∪ {` → r }, {` → r })23:
end if24:
i := i + 1
25:
end while
26:
return R
27: end procedure19:

One should remark here, that when normalizing the selected equation (line 7),
several possible normal forms can exist, since Ri is terminating, but needs not tobe confluent. Also, according to the original description of the algorithm in [49],after constructing the new rule ` → r, all left and right hands sides of rules from
Ri are rewritten to a normal form to remove redundant rules. This is called36

3.1 Knuth-Bendix Completioninter-reduction. However, one needs extra care in this case, since applying interreduction before normalizing the selected equation (i.e. in-between line 6 andline 7) leads to an incorrect algorithm. Huet [40] was the first to give a full proofof soundness of the algorithm including inter-reduction.
Theorem 3.1.1. Let E be an ES, and > a reduction order. If KB-Complete(E , >)terminates with output R, then R is a complete TRS for E .
We give a brief example to illustrate the mechanisms of the algorithm, and also
one of its weaknesses. To keep track of rules and equations, when referring to arule originating from an indexed equation j : s ≈ t, we write j to denote s → t,
and j0 to denote t → s. However we omit the counter i of the Knuth-Bendix
algorithm for brevity.
Example 3.1.2. Consider the ES E consisting of the equalities:1:s(p( x )) ≈ x2:p(s( x )) ≈ x

3:s( x ) + y ≈ s( x + y )and the lexicographic path order > with precedence +  s  p. Suppose we selectthe first rule. Since there are no critical pairs of rule 1 on itself, we have E = {2, 3}
and R = {1}. We continue by selecting the second rule, which leads to E = {3} andR = {1, 2}. Since the critical pairs s( x ) ≈ s( x ) and p( x ) ≈ p( x ) between 1 and 2 aretrivial, we can ignore them, continue and select rule 3. There is one critical pair between
rule 1 and rule 3
4:

x + y ≈ s(p( x ) + y )which is in normal form w.r.t. R. Thus E = {4} and R = {1, 2, 3}. We select equation
4, and obtain three new critical pairs:5:p( x + y ) ≈ p( x ) + y

7:s( x + y ) ≈ s( x ) + y

6:( x + y) + z ≈ s((p( x ) + y) + z)

Suppose rule 5 is selected. Then R = {1, 2, 3, 40 , 50 } is complete. After two iterations
where equations 6 and 7 are selected, rewritten to identical normal forms and removed
from E , we arrive at E = ∅ and the algorithm succeeds. It should be noted, that rule 40
is redundant, since both sides of it rewrite to identical normal form by R = {1, 2, 3, 50 }.
It can be observed in Example 3.1.2 that the algorithm has some inefficiency,
since it does not apply inter-reduction to remove redundant rules from the current TRS in every iteration. As mentioned, one has to be careful when rewriting
rules of a TRS by itself, as it might affect soundness, cf. [75]. Bachmair et al. [12]made this condition explicit, by reformulating the procedure into a set of inference rules KB, which operate on a tuple (E , R) of an equational set and a TRS. To
formulate the condition of soundness, the encompassment order is used.

37

Chapter 3: Completion Procedures

DeduceE, R
E ∪ { s ≈ t }, R

if s R ← · →R t

OrientE ∪ { s ≈ t }, R
E , R ∪ {s → t}

if s > t

DeleteSimplifyE ∪ { s ≈ s }, R
E, R
E ∪ { s ≈ t }, RE ∪ { u ≈ t }, R

if s →R u

ComposeE , R ∪ {s → t}
E , R ∪ {s → u}

if t →R u

Collapse

E , R ∪ {s → t}
E ∪ { u ≈ t }, R

if s −→R u

A

Figure 3.1: Inference rules KB of Knuth-Bendix completion
Definition 3.1.3. The encompassment quasi order w is defined as s w t if there exist a
position p ∈ P os(s) and a substitution σ, such that s| p = tσ. Its strict part A is definedA

as s A t if s w t and t 6w s. We will write s −→R t if s →`→r t for some ` → r ∈ R ands A `.
Note that the strict part of the encompassment order is well-founded.
Definition 3.1.4. Let KB be the set of inference rules depicted in Figure 3.1. A completion procedure takes as input an ES E and a reduction order >, and generates a run
with E0 = E and R0 = ∅. Here, a run is a sequence(E0 , R0 ) `KB (E1 , R1 ) `KB (E2 , R2 ) `KB (E3 , R3 ) `KB . . .
where for all i ≥ 0 the first component Ei is an equational system, the second component
Ri is a TRS and (Ei+1 , Ri+1 ) is reachable from (Ei , Ri ) by one of the inferences.
The output of the procedure is formulated as persistent sets.
Definition 3.1.5. The sets of persistent equations Eω and persistent rules Rω aredefined as

Eω =

[\
i ≥0 j ≥ i

38

Ej

and

Rω =

[\
i ≥0 j ≥ i

Rj.

3.2 Completion with Termination Tools
Definition 3.1.6. The run generated by a completion procedure on E fails if Eω 6= ∅.
A run is fair if[
CP(Rω ) ⊆
Ei .
i ≥0

Theorem 3.1.7. Suppose a completion procedure generates a non-failing and fair run on
E . Then Rω is complete for E .
Thus Theorem 3.1.7 applies not just to one particular algorithm, but to every
procedure that applies the inferences sequentially in a fair manner. Actual implementations of course need to turn the procedure into some algorithmic form, andusually implementations are similar to the original Knuth-Bendix completion or
Huet’s procedure [40].

3.2 Completion with Termination Tools
Knuth-Bendix completion requires to fix the ordering a priori. However the orders we presented in Chapter 2 are sometimes simply too weak to prove termination of a TRS. Consider for example the ES with just one equationf ( x ) ∗ g(y) ≈ g(y) ∗ f ( x )This equation appears for example in theories of commuting group endomorphisms [74]. Orienting the equation in either direction results in a complete TRS.
But one can verify that there exists no LPO, MPO or KBO that allows to orient
this rule. However much progress has been made in showing the terminationof term rewriting systems automatically. Here we especially mention the dependency pair method [8, 30, 37] and matrix interpretations [23]. Both methods areable to show termination in the example.
Wehrman et al. [83] suggested to not fix a reduction order in advance, but instead to test termination of the TRS component R during completion and use →+R
as the ordering. In practice, the test for termination can be done by a dedicatedtermination tool. Note that →+R is a reduction order whenever R is terminating. Based on this idea, they formulated a framework for completion based on
inference rules, depicted in Figure 3.2.
The notion of run, fairness and failure can be extended in a straight-forwardmanner for the inference rules KBT. Initially the component C is empty.
Theorem 3.2.1 ([83]). Suppose a completion procedure generates a non-failing and fairrun with KBT on input E . Then Rω is complete and equivalent for E .
One might wonder why ensuring termination of Ri is not sufficient and why
adding a dedicated component C is necessary. The role of C is to incrementally

39

Chapter 3: Completion Procedures

DeduceE , R, CE ∪ { s ≈ t }, R, C

OrientE ∪ { s ≈ t }, C
if C ∪ {s → t} is terminating
E , R ∪ { s → t }, C ∪ { s → t }E ∪ { s ≈ s }, R, C
E , R, CE ∪ { s ≈ t }, R, C
SimplifyE ∪ { u ≈ t }, R, C

if s R ← · →R t

Deleteif s →R u

ComposeE , R ∪ { s → t }, C
E , R ∪ { s → u }, C

if t →R u

Collapse

E , R ∪ { s → t }, CE ∪ { u ≈ t }, R, C

if s −→R u

A

Figure 3.2: Inference rules KBT of Completion with Termination Tools
construct an order. Whenever a step (Ei , Ri , Ci ) `KBT (Ei+1 , Ri+1 , Ci+1 ) is applied,
the inclusion Ci ⊆ Ci+1 holds by definition, and thus we have →C+ ⊆ →C+ .
i
i +1
However due to the rule Collapse, Ri ⊆ Ri+1 does not necessarily hold and thus+→+
Ri ⊆ →Ri+1 also does not hold in general. The question whether changing
the order in a non-incremental manner still yields a correct procedure was formulated as problem #35 in the RTA list of open problems1 , and finally answered
negatively in [69].
To practically apply the inferences, Wehrman et al. proposed an algorithm very
similar to Huet’s [40].

3.3 Multi-Completion
As seen, in Knuth-Bendix completion, a fixed order is expected as an input parameter, and in completion with termination tools the order is constructed onthe-fly by orienting equations into a terminating TRS. If an equation can be oriented in both directions, a choice between the corresponding orders has to be
made. Therefore in both procedures failure or success heavily depends on the
choice of the reduction order.
1 http://rtaloop.mancoosi.univ-paris-diderot.fr

40

3.3 Multi-Completion
Example 3.3.1. Consider the following ES E from [72], consisting of1:( x + y) + z ≈ x + (y + z)

2:f ( x + y) ≈ f ( x ) + f (y)Let >1 be the lexicographic path order with precedence f  +, and >2 the lexicographic
path order with precedence +  f. A run with >1 succeeds with the complete andequivalent TRS {1, 2}. However a run with >2 fails, since then Eω is not empty.
In general it is not trivial to make a suitable choice for an order in advance.
To practically apply completion with termination tools, Wehrman et al. [83] developed a heuristical best-first search strategy to select one orientation if bothare possible. In the case of unorientable equations, backtracking is employed torecover failed attempts. One drawback of such an approach is that a complete
TRSs is easily missed if infinitely many orientable equations are generated as in
Example 3.3.1, or if the best-first heuristic dos not apply for the ES in question.

OrientN ∪ {hs : t, L1 , L2 , L3 ∪ Li}
N ∪ {hs : t, L1 ∪ L, L2 , L3 i}
if L 6= ∅, L3 ∩ L = ∅ and s >i t for all i ∈ L
N ∪ {hs : s, ∅, ∅, Li}N

DeleteRewrite-1

Rewrite-2

Deduceif L 6= ∅N ∪ {hs : t, L1 , L2 , L3 i}hs : t, L1 \ L, L2 , L3 \ Li,N∪
hs : u, L1 ∩ L, ∅, L3 ∩ Li
if h` : r, L, ·, ·i ∈ N, ( L1 ∪ L3 ) ∩ L 6= ∅, t →`→r u, and t and` are variantsN ∪ {hs : t, L1 , L2 , L3 i}hs : t, L1 \ L, L2 \ L, L3 \ Li,N∪
hs : u, L1 ∩ L, ∅, ( L2 ∪ L3 ) ∩ Li
if h` : r, L, ·, ·i ∈ N, ( L1 ∪ L2 ∪ L3 ) ∩ L 6= ∅, and t →`→r u,
and t A `N
N ∪ {hs : t, ∅, ∅, L ∩ L0 i}
if h` : r, L, ·, ·i ∈ N, h`0 : r 0 , L0 , ·, ·i ∈ N, L ∩ L0 6= ∅, ands `→r ← · →`0 →r0 t

Figure 3.3: Inference rules MKB of Multi-Completion

41

Chapter 3: Completion Procedures
A natural idea to handle Example 3.3.1 is to run Knuth-Bendix completion withseveral orders in parallel. Due to the sheer number of possible orders, this is
usually not efficient. For example a signature with n function symbols induces n!
total precedences and thus at least n! possible lexicographic path orderings, andeven more if we count non-total precedences. Much performance can be gained,
if operations involving equations and rules that are shared among runs withdifferent orders have to be performed only once. Kurihara and Kondo [51] first
introduced this idea, and central to its practical applicability is the introductionof a specialized data structure, a node.
Definition 3.3.2. Let I be a set of indices, and >1 , . . . , >n be n reduction orders. A node
is a tuple hs : t, L1 , L2 , L3 i, where s : t is an ordered pair of terms, L1 , L2 and L3 aremutually disjoint subsets of I that satisfy the following two conditions. For 1 ≤ i ≤ n:
1. s >i t whenever i ∈ L1 , and2. t >i s whenever i ∈ L2 .
A node hs : t, L1 , L2 , L3 i is identified with ht : s, L2 , L1 , L3 i.
In practice, one could for example choose for the orders >1 , . . . >n the lexicographic path orders generated by all possible precedences.
Definition 3.3.3. Let n = hs : t, L1 , L2 , L3 i be a node and i ∈ I an index. The Eprojection and R-projection E[n, i ] and R[n, i ] of node n onto i are defined as(
{s → t} if i ∈ L1
{s ≈ t} if i ∈ L3
E[n, i ] =R[n, i ] = {t → s} if i ∈ L2∅otherwise∅otherwise
They are extended to a set of nodes N by
E[ N, i ] =[n∈ NE[n, i ]R[ N, i ] =[R[n, i ]n∈ NInferences similar to Knuth-Bendix completion can be formulated. Here theinferences MKB, depicted in Figure 3.3, operate on nodes.
Definition 3.3.4. A run of multi-completion is a sequence of sets of nodes S =N0 `MKB N1 `MKB . . . with N0 = {hs : t, ∅, ∅, I i | s ≈ t ∈ E } such that Ni+1
is reachable from Ni by on of the inferences of MKB.
One can project a run of multi-completion to a run of Knuth-Bendix completion as follows. Given a run S of multi-completion and index i ∈ I of the run,the projection KB[S, i ] is generated as follows: First, every set of nodes Nj is projected to the tuple ( E[ Nj , i ], R[ Nj , i ]). Then we yield a sequence of configurations,42

3.4 Multi-Completion with Termination Tools
where each ( E[ Nj+1 , i ], R[ Nj+1 , i ]) is reachable from ( E[ Nj , i ], R[ Nj , i ]) either bya step of Knuth-Bendix completion or by an equivalent step, i.e. both configurations are identical. Now all such equivalent steps with ( E[ Nj , i ], R[ Nj , i ]) =( E[ Nj+1 , i ], R[ Nj+1 , i ]) are removed to obtain the projection KB[S, i ].
Lemma 3.3.5. Let S be a run of multi-completion, and i ∈ I. Then KB[S, i ] is a run ofcompletion with KB.
Definition 3.3.6. An MKB-completion procedure is a program that takes as input an ES
E and an indexed set of orders I, and generates a run of multi-completion S. The set of
persisting nodes Nω is defined as
Nω =

[ \

Nk .

j ≥0 k ≥ j

A run of MKB fails, if KB[S, i ] fails for all i ∈ I. An MKB-completion is fair, if it isfinite and KB[S, i ] is non-failing for some some i ∈ I or if it is infinite and KB[S, i ] iseither fair or failing for all for all i ∈ I.
The above definition follows [86] and differs from [51] to ensure soundness andcompleteness properties similar to Knuth-Bendix completion. We refer to [86] fora more in-depth discussion.
Theorem 3.3.7. Let E be an ES, and I an indexed set of reduction orders. Let S =N0 `MKB N1 `MKB . . . be a non-failing, fair run of MKB-completion. Then there exists
an i ∈ I such that R[ Nω , i ] is complete and equivalent for E .

3.4 Multi-Completion with Termination Tools
Implementations of Multi-completion do not suffer from the indeterminism of
the inference Orient of Knuth-Bendix completion and completion with termination tools. On the other hand, the latter significantly enhances the powerof completion by making a larger class of reduction orders available. It was
shown in [68] how these two approaches can be combined with the inference
rules MKBTT, depicted in Figure 3.4.
While multi-completion considers indices of runs with different reduction orders, here runs of parallel completion procedures are directly identified by bitstrings. Whenever an equation can be oriented both ways, the run is split bycreating two copies of all nodes and attaching a 0 resp. 1 to each of them. Intuitively a node hs : t, R1 , R2 , E, C1 , C2 i is a tuple containing the equation itself,
the set R1 which collects all bitstrings where the equation is oriented s → t, andthe set R2 which collects those where t → s. Similar to KBT, the sets C1 and C2collect constraints for R1 and R2 to ensure the implied orders are constructed in

43Chapter 3: Completion Procedures

OrientN ∪ {hs : t, R1 , R2 , E, C1 , C2 i}
split( N ) ∪ {hs : t, R1 ∪ Rlr , R2 ∪ Rrl , E0 , C1 ∪ Rlr , C2 ∪ Rrl i}with Elr , Erl ⊆ E such that
• Elr ∪ Erl 6= ∅,• P = Elr ∩ Erl ,• E0 = E\( Elr ∪ Erl )• C [ N, p] ∪ {s → t} terminates for all p ∈ Elr ,• C [ N, p] ∪ {t → s} terminates for all p ∈ Erl ,• Rlr = ( Elr \ Erl ∪ { p0 | p ∈ P}, and• Rrl = ( Er \ Elr ) ∪ { p1 | p ∈ P},
and split p ( N ) replaces every p ∈ P in any label in N by p0 and p1.

DeleteN ∪ {hs : s, ∅, ∅, E, ∅, ∅i}
NGc

N ∪ {hs : t, ∅, ∅, ∅, ∅i}N

Rewrite-1

N ∪ {hs : t, R1 , R2 , E, C1 , C2 i}hs : t, R1 \ R, R2 , E\ R, C1 , C2 i,
N∪
hs : t, R1 ∩ R, ∅, E ∩ R, C1 , C2 i
if h` : r, R, · · · i ∈ N, t →`→r u, t and ` are variants, R ∩ ( R1 ∪ E) 6= ∅Rewrite-2

N ∪ {hs : t, R1 , R2 , E, C1 , C2 i}hs : t, R1 \ R, R2 \ R, E\ R, C1 , C2 i,
N∪
hs : t, R1 ∩ R, ∅, ( R2 ∪ E) ∩ R, ∅, ∅i

if h` : r, R, · · · i ∈ N, t →`→r u, t A ` and R ∩ ( R1 ∪ R2 ∪ E) 6= ∅DeduceSubsumeNN ∪ {hs : t, ∅, ∅, R ∩ R0 , ∅, ∅i}if there exist nodes h` : r, R, · · · i, h`0 : r 0 , R0 , · · · i ∈ N such thats `→r ← · →`0 →r0 t and R ∩ R0 6= ∅N ∪ hs : t, R1 , R2 , E, C1 , C2 i, hs0 : t0 , R10 , R20 , E0 , C10 , C20 i
N ∪ {hs : t, R1 ∪ R10 , R2 ∪ R20 , E00 , C1 ∪ C10 , C2 ∪ C20 i}
if E00 = ( E\( R10 ∪ R20 ∪ C10 ∪ C20 )) ∪ ( E0 \( R1 ∪ R2 ∪ C1 ∪ C2 )) and s
and s0 , and t and t0 are variants

Figure 3.4: Inference rules MKBTT of Multi-Completion w/ Termination-Tools
44

3.4 Multi-Completion with Termination Tools
an incremental manner. The set E contains the indices of those runs, where theequation s ≈ t has been deduced, but not been oriented or rewritten to identity
yet.
Soundness can be established in a similar way as done for multi-completion.
For precise definitions and proofs, we refer to [67], and instead we illustrate how
the inferences of MKBTT operate on the ES of Example 3.1.2.
Example 3.4.1 (continued from Example 3.1.2). Initially, three nodes are created:
1:
2:
3:

hs(p( x )) : x, ∅, ∅, {ε}, ∅, ∅i
hp(s( x )) : x, ∅, ∅, {ε}, ∅, ∅ihs( x ) + y : s( x + y), ∅, ∅, {ε}, ∅, ∅i

After three applications of Orient, we yield the following set of nodes. Note that orienting node 3 causes a split.

hs(p( x )) : x, {0, 1}, ∅, ∅, {0, 1}, ∅ihp(s( x )) : x, {0, 1}, ∅, ∅, {0, 1}, ∅ihs( x ) + y : s( x + y), {0}, {1}, ∅, {0}, {1}i

1:
2:
3:

Applying Deduce to nodes 1 and 3 and to nodes 2 and 3 yields two new nodes:
4:5:

h x + y : s(p( x ) + y), ∅, ∅, {0}, ∅, ∅i
hp(s( x ) + y) : x + y, ∅, ∅, {1}, ∅, ∅i

Applying Orient on 4 and 5, modifies these nodes to4:5:

h x + y : s(p( x ) + y), ∅, {0}, ∅, ∅, {0}i
hp(s( x ) + y) : x + y, {1}, ∅, ∅, {1}, ∅i

The inference Deduce on nodes 4 and 2, and on node 5 and 1 yield one new node:6:

hp( x ) + y : p( x + y), ∅, ∅, {0, 1}, ∅, ∅i

Then Orient modifies this equation to6:

hp( x ) + y : p( x + y), ∅, {0}, {1}, ∅, ∅i

Now Rewrite-2 can be applied twice on node 4, first using node 6 and then node 1, andfinally Delete removes node 4 entirely. We can now consider the run indexed by 0. The
E-projection of index 0 consists of the equations of those nodes, where 0 appears in the
E-component (fourth component) of a node — it is empty.
The R-projection of a node n with respect to index 0 is defined as {s → t} if p ∈ R1 , as{t → s} if p ∈ R2 and ∅ otherwise. Thus the union of R-projections of all nodes yields
the TRS R = {1, 2, 3, 6}. Moreover one can verify that the run indexed by 0 is fair, since
since all non-trivial critical pairs of R have been considered. Thus R is complete.

45Chapter 3: Completion Procedures
Note how in completion with MKBTT of Example 3.4.1, several equations(equations 1, 2, 3 and 6) are shared among the runs. When the completion ofan equational system is more complex than in the considered example, this effects a significant performance gain. Moreover MKBTT allows to fully use theprogress made in research about automated termination analysis, and yields avery powerful procedure.
In the example, the sequence of selection of nodes and inferences on them leads
quickly to a complete TRS. Two issues remain in this framework. The first one
is that when practically applying this framework, the indeterminism of nodeselection has to be resolved. Similar to the choice of the reduction order, thequestion which node to select when, can have an influence both on the outcomeof the algorithm itself and on its performance. Secondly, the incorporation of
implementational details, the data structure node, makes the formulation of theinferences more complex, and the extraction of the essential soundness propertiesof completion non-trivial.

3.5 Inductive Proofs by Completion
Methods to prove inductive theorem can roughly be classified into three categories. Explicit methods [15] construct an explicit induction scheme that is adjusted specifically for the equational system and the conjecture in question. Proofs
by consistency [18] do not rely on an induction scheme at all. Instead they starta proof attempt directly and try to find a suitable induction scheme during theproof. Lastly, implicit induction techniques are somewhat between the two above.
They are direct adaptations of completion to the setting of inductive theorem
proving. While no explicit induction scheme is generated a priori, an induction
scheme is implicitly provided by a syntactic order. Since the order changes theinduction scheme, the choice of it affects the outcome of a proof attempt, quite
similar to completion.
Due to the deep connection with completion we solely focus on the latter. For
an overview of methods based on proofs by consistency, and a more in-depth
discussion about the differences to implicit methods we refer to [18]. We remarkthat [18] refers to methods using proofs by consistency as inductionless induction.
The terminology inductionless induction has been used by multiple authors inseveral different manners.
We will use the terminology inductionless induction in a different fashion
than [18]. With it we refer to one specific implicit proof method due to Gramlich [34]. It greatly illustrates the connection between Knuth-Bendix completion
and inductive proof methods. The second result we recall here is rewriting induction. Although there is no direct historical connection, it can be seen as a refinement of Gramlich’s method. Several extensions to rewriting induction have been46

3.5 Inductive Proofs by CompletionE ∪ { s ≈ s }, H
E, H
E ∪ { s ≈ t }, H
SimplifyE ∪ { u ≈ t }, H
DeleteExpandif s →R∪H u

E ∪ { s ≈ t }, H
if {s → t} is R-expandable
E ∪ Expd(R, {s → t}), H ∪ {s → t}

Figure 3.5: Inference rules of Rewriting Induction
proposed [1, 2], which allow to construct powerful inductive theorem provers.
Multi-completion also has been adapted to be used with rewriting induction [66].
Such extensions however are beyond the scope of this thesis.
Before continuing, we first recall some definitions related to inductive theorems.
Definition 3.5.1. A term t is R0 -inductively-reducible, if for all ground substitutions
σg on t, the term tσg is R0 -reducible. A TRS R is left-R0 -inductively-reducible, if for
all rules ` → r ∈ R, the term ` is R0 -inductively-reducible.
Below when writing R0 `i H for TRS R and H the latter is regarded as an ES.
The next theorem is the basis of inductionless induction.
Theorem 3.5.2 ([34]). Let R = R0 ∪ H be a terminating, and left-R0 -inductivelyreducible TRS. If CP(R0 , H) ⊆ ↓R , then R0 `i H.
It is not difficult to design inference rules for inductive proofs based on Theorem 3.5.2 that delete identities, rewrite equations or add critical pairs, see [34].
We skip such a calculus however and proceed to rewriting induction [62]. It relaxes the joinability conditions of inductionless induction. Instead of requiring
all critical pairs to be joinable, joinability of only a specific subset suffices.
We recall some additional definitions. Given a TRS R, the set D = {root(`) |` → r ∈ R} is the set of defined function symbols (of R). The set C = F \ D
is the set of constructor symbols. A term t = f (c1 , . . . , cn ) is basic, if f ∈ D andci ∈ T (C , V ) for all 1 ≤ i ≤ n. We write B(t) for the set of all basic positions{ p ∈ P os(t) | t| p is basic}. A TRS is quasi-reducible if no ground basic term is innormal form. Let R0 be a quasi-reducible TRS with defined function symbols D
and constructor symbols C , and let E be an ES. We say that R is R0 -expandable
if for every ` → r ∈ R there exists a basic (w.r.t. D and C ) position in `. We
write Expd(R0 , R) for the set of all critical pairs originating from overlaps (`1 →47

Chapter 3: Completion Procedures
r1 , p, `2 → r2 )µ of R0 on R, where p is a fixed (depending on `1 → r1 ) basic
position in `2 .
Before continuing, we remark the following. Quasi-reducibility ensures that all
instantiations of variables can be considered to be solely built upon constructor
symbols. However quasi-reducibility rarely holds for unsorted TRSs. Thus one
often assumes TRSs to be sorted when reasoning with inductive theorems. We
will follow this approach throughout this thesis.
Theorem 3.5.3 ([62]). Let R and H be TRSs such that R is quasi-reducible and R ∪ H
is terminating. If Expd(R, H) ⊆ ↓R∪H then R `i H.
Inference rules for Rewriting Induction are depicted in Figure 3.5. We write(E , H)(E 0 , H0 ) when applying an inference rule of Figure 3.5. The reflexive
transitive closure of application of such rules is depicted by ∗ . Using Theorem 3.5.3 one can show correctness of deriving proofs by this inference system.
Theorem 3.5.4 ([62]). Let R be a quasi-reducible TRS, E a set of equations and > a
reduction order with R ⊆ >. If there exists a sequence of inferences and a TRS H suchthat (E , ∅) ∗ (∅, H), then R `i H.
To conclude this section, we give an example to show how a proof of a valid
conjecture is obtained using the inference rules in Figure 3.5.
Example 3.5.5. Consider the TRS R consisting of
1:0+y → y2:s( x ) + y → s( x + y )with sorts 0 : nat, s : nat → nat and + : nat × nat → nat. Let the set of conjectures E
consist of the next equation.
3:( x + y) + z ≈ ( x + y) + z

The proof starts by ({3}, ∅). After expansion at the leftmost, innermost basic position
we reach ({4, 5}, {3}) where 4 and 5 are the equations:4:y1 + z ≈ 0 + ( y1 + z )5:s( x2 + y2 ) + z ≈ s( x2 ) + ( y2 + z )Both sides of equation 4 and 5 rewrite to identical normal form by the TRS {1, 2, 3}.
Therefore by several steps of the rules Simplify and Delete we have ({4, 5}, {3}) ∗(∅, {3}). Thus R `i E .

48

Chapter 4
Maximal Completion

In Chapter 3 we presented the original Knuth-Bendix completion procedure andseveral extensions. Searching for a complete TRS, these procedures face a kind of
dilemma: With simplicity of the framework comes a decrease in power, and withmore power comes an increase in the complexity of the framework due to incorporation of algorithmic and implementational details. The underlying reason isthat all extensions essentially rely on the original algorithmic design of KnuthBendix’ procedure to ensure soundness. This design imposes a certain way how
to construct the search space, and a dedicated search algorithm to resolve allindeterminism.
During the early 2000’s, much progress has been made in the area of constraint solving. Problems such as SAT, which are NP-hard and were thought tobe intractable, turned out to be effectively solvable in many instances. Highly
optimized algorithms, usually extensions of the DPLL-procedure [19], enabledapplications in other domains, where encoding the problem to constraints andusing a constraint solver has surpassed the development of dedicated algorithms.
Such an approach is usually more efficient, and moreover allows to abstract implementational details from a framework as constraints. For example many techniques to automatically show termination of a TRS can be encoded as an instanceof SAT.
To encode a problem as an instance of SAT, the search space has to be made49

Chapter 4: Maximal Completion
explicit in order to be representable by a finite number of constraints. Unfortunately, due to the complexity of the completion problem, it is non-trivial to
explicitly give the search space that includes all desirable complete TRSs. But we
present a new framework for completion by giving an encoding to a maximality
problem over constraints. This allows to separate the soundness properties ofcompletion from the search problem. Since the search space is represented indirectly by maximality constraints, no dedicated algorithm is needed any more,
and implementational details are no longer part of the framework. Therefore it
can be formulated in a much simpler way than existing powerful completion procedures, even though all existing completion procedures can be expressed in ourframework by choosing suitable parameters. Experimental evaluation of a prototype implementation shows that the procedure can cope with and often surpasses
existing state-of-the-art tools. Moreover due to its modularity, the framework canbenefit from any future progress in MaxSAT or MaxSMT.
To formulate our framework we first look again at the completion procedure
itself, and reformulate it as a maximality problem in Section 4.1. We show how
to automate this formulation by giving an encoding to maximality constraints in
Section 4.2, and we relate our framework to existing procedures in Section 4.3.
Finally we evaluate our approach experimentally in Section 4.4.

4.1 Maximality
The task of completion is to find a complete TRS with respect to some given
system of equalities. This notion of completeness is captured in the next lemma.
Lemma 4.1.1. A TRS R is complete for an ES E if and only if R is terminating,R ⊆ ↔∗E , and E ∪ CP(R) ⊆ ↓R .
Proof. For the “if”-direction, by Knuth and Bendix’ confluence criterion [49] (Theorem 2.4.5), confluence of R follows from CP(R) ⊆ ↓R and termination of R.
Moreover, E ⊆ ↓R and R ⊆ ↔∗E yield ↔∗R = ↔∗E . The “only if”-direction isimmediate from ↔∗E = ↔∗R ⊆ ↓R .
Lemma 4.1.1 yields a simple completion procedure. Let E be an ES. We assume
that two parameter functions R and S are given and the next two conditions holdfor every ES C : S(C) is a set of equalities in ↔∗E , and R(C) is a set of terminating
TRSs R with R ⊆ ↔∗E .
Definition 4.1.2. Given ESs E and C , the procedure ϕ is defined as(R
if E ∪ CP(R) ⊆ ↓R for some R ∈ R(C)
ϕ(C) =
ϕ(C ∪ S(C)) otherwise
Note that ϕ(C) is neither unique nor defined in general.

50

4.1 Maximality
Theorem 4.1.3. ϕ(E ) is a complete TRS for an ES E , if it is defined.
The procedure ϕ repeatedly expands C (initially E ) by S(C) until R(C) contains
a complete TRS for E . For its success the choice of R(C) and S(C) is crucial. Lett↓R denote a fixed normal form of t with respect to R. We say that a TRS R isover an ES C if R ⊆ C ∪ C −1 . The set of all terminating TRSs over C is denoted by
T(C). We propose to use
R(C) = Max T(C)S(C) =[{s↓R ≈ t↓R | s ≈ t ∈ E ∪ CP(R) and s↓R 6= t↓R }R∈ R(C)

Here Max computes all maximal sets of rewrite rules (called maximal TRSs) in
its given family of TRSs, and this is the reason that we call our method maximal
completion. Part (b) in the next lemma explains why non-maximal TRSs in T(R)can be ignored safely.
Lemma 4.1.4. Let E be an ES. The following claims hold:(a) Let R and R0 be TRSs such that R ⊆ R0 ⊆ ↔∗E with R0 terminating. Then R0 is
complete for E if R is complete for E .
(b) E ∪ CP(R) ⊆ ↓R for some R ∈ T(C) iff E ∪ CP(R) ⊆ ↓R for some R ∈ R(C).
Proof. (a) Due to completeness of R, we have E ∪ CP(R0 ) ⊆ ↓R . The claim follows together with →R ⊆ →R0 . (b) The ‘only if’-direction is straightforwardfrom the first claim, and the converse is trivial.
We illustrate maximal completion with an example.
Example 4.1.5. Consider the ES E consisting of the equalities:1:s(p( x )) ≈ x2:p(s( x )) ≈ x

3:s( x ) + y ≈ s( x + y )We compute ϕ(E ) with the above S(C) and R(C).
(i) R(E ) consists of two TRSs {1, 2, 3} and {1, 2, 30 }. Since the join-condition of ϕdoes not hold, we have ϕ(E ) = ϕ(E ∪ S(E )). Here S(E ) consists of two equalities:
4:

x + y ≈ s(p( x ) + y )5:p(s( x ) + y ) ≈ x + y(ii) R({1, . . . , 5}) consists of the two TRSs {1, 2, 3, 40 , 5} and {1, 2, 30 , 40 , 5}. Again
the join-condition does not hold. Thus, ϕ({1, . . . , 5}) = ϕ({1, . . . , 9}), where
6 : ( x + y) + z ≈ s((p( x ) + y) + z)
8:p( x ) + y ≈ p( x + y )7 : p((s( x ) + y) + z) ≈ ( x + y) + z
9:p(( x + y) + z) ≈ (p( x ) + y) + z

51

Chapter 4: Maximal Completion(iii) R({1, . . . , 9}) consists of four TRSs including the TRS R of

{1, 2, 3, 40 , 5, 60 , 7, 8, 90 }which satisfies the join-condition. Thus, ϕ({1, . . . , 9}) = R.
Hence, ϕ(E ) = R and it is a complete TRS for E .
Very often a complete TRS resulting from maximal completion contains manysuperfluous rules. It is known that this problem is resolved by computing reduced TRSs (cf. [40]). A TRS R is reduced if ` ∈ NF(R \ {` → r }) and r ∈ NF(R)b for the reduced TRS
for all rules ` → r ∈ R. We write R
e | ` ∈ NF(Re \ {` → r })}{` → r ∈ R
e = {` → r ↓R | ` → r ∈ R}. The TRS R
b fulfills the desired property:
where Rb is complete for E .
Lemma 4.1.6. If a TRS R is complete for E , then R
b is complete and ↔∗ = ↔∗ (see [54]).
Proof. Using the fact that RRbRe = {1, . . . 9}. The leftExample 4.1.7 (continued from Example 4.1.5). We have R
hand sides of rules 5 and 7 are reducible by rule 3, and the left-hand sides of rules 40 , 60
and 90 are reducible by rule 8. Rules i = 1, 2, 3, 8 are in normal form with respect toe \ {i }. Thus the reduced version R
b is {1, 2, 3, 8}.
R
As Example 4.1.5 illustrates, maximality dismisses undesirable complete TRSs
like empty or singletons in T(C). This is one major source of efficiency in maximal completion. We refer to the subsequent two sections for further discussion
on R(C) and S(C).

4.2 Automation
We describe how to automate the approach of Section 4.1.

4.2.1 Computing Maximal Terminating TRSs
Since termination is undecidable, for automation we compute maximal elementsin the set of TRSs over a given C , for which we can show termination with reduction orders automatically. However, since there are exponentially many TRSs
over C in general, it is impractical to check termination of each of them to compute maximal elements. We present a solution using MaxSAT solving.
In the last years, SAT/SMT-encodings of termination conditions based on existing subclasses of reduction orders have been extensively investigated, and today52

4.2 Automation
they are well-established. Here we mention recursive path orders [52, 17], KnuthBendix orders [88] and orders based on matrix interpretations [23]. Importantly,
all of them can test the existence of a reduction order > that satisfies arbitrary
Boolean combinations of order constraints:
C ::= s > t | > | ⊥ | ¬ C | C ∨ C | C ∧ C
We exploit this fact to encode a maximal termination problem into a maximal
satisfiability problem. Even though NP-hard in general, nowadays solving canbe efficiently done by SMT solvers.
Computing maximal terminating TRSs is done iteratively: Given a set of equalities C , assume we already found k maximal terminating TRSs R1 , . . . , Rk over C .
In the following we write
Maximize S subject to ϕ
for the problem of finding an assignment (here an order) that maximizes thenumber of satisfied elements in the set S while satisfying ϕ. We construct thefollowing optimization problem ψ:Maximize {(s > t) ∨ (t > s)}s≈t∈C subject to

k
^

_

i =1

`→r ∈(C∪C −1 )\R`>ri

Since each ` > r can be encoded w.r.t. a particular class of reduction orders to
Boolean constraints, ψ can be treated as an instance of MaxSAT/MaxSMT. A
solution yields a maximal subset of oriented equalities from C , that forms a terminating TRS Rk+1 and is different from all R1 , . . . , Rk . If ψ is unsatisfiable, we
found all maximal terminating TRSs over C (w.r.t. the considered reduction order) and return {R1 , . . . , Rk }. Otherwise, we re-encode ψ w.r.t. Rk+1 for another
MaxSAT/MaxSMT-instance.
One might wonder, why one has to maximize all possible rules subject to
k
^

^

i =1

`→r ∈(C∪C −1 )\R` > r.
i

Intuitively one might think thatk^_¬(` > r )i =1 `→r ∈Ri

is sufficient. However, note that ¬(` > r ) holds, if ` > r does not hold in theconsidered order, and this does not mean that r > `. While such an encoding issound, it does generate TRSs that are not always maximal terminating. In the following example, we assume that our constraint encodings are further translated
to test the existence of a lexicographic path order.

53

Chapter 4: Maximal Completion
Example 4.2.1 (continued from Example 4.1.5). Recall the ES E consisting of:1:s(p( x )) ≈ x2:p(s( x )) ≈ xs( x ) + y ≈ s( x + y )3:

We have found no maximal TRS yet, thus k = 0. The corresponding constraint is:
Maximize{(1 ∨ 10 ), (2 ∨ 20 ), (3 ∨ 30 )} subject to >This constraint can be further translated into a problem over boolean constraints, thattests the existence of a suitable lexicographic path order such that all the termination constraints are satisfied. The LPO with precedence +  s maximizes the above constraints,
as it yields the TRS R1 = {1, 2, 3}. To find another maximal TRS R2 , we encode thefollowing constraint problem:
Maximize{(1 ∨ 10 ), (2 ∨ 20 ), (3 ∨ 30 )} subject to (10 ∨ 20 ∨ 30 )A valid solution to this maximality constraint is the TRS R2 = {1, 2, 30 }, induced fromthe LPO with precedence s  +. For the next constraint problem
Maximize{(1 ∨ 10 ), (2 ∨ 20 ), (3 ∨ 30 )} subject to (10 ∨ 20 ∨ 30 ) ∧ (10 ∨ 20 ∨ 3)

the “subject to”-part is not satisfiable, so no terminating TRS can satisfy this constraint.
In particular, there exists no LPO that satisfies it. Thus all maximal terminating TRSs
have been computed. Now suppose we would have instead used the other encoding:Maximize {(s > t) ∨ (t > s)}s≈t∈C subject tok^_¬(` > r )i =1 `→r ∈RiThen, after computing R1 and R2 similar as above, we have the following constraint.
Maximize{(1 ∨ 10 ), (2 ∨ 20 ), (3 ∨ 30 )}subject to (¬10 ∨ ¬20 ∨ ¬30 ) ∧ (¬10 ∨ ¬20 ∨ ¬3)

If one takes the LPO with empty precedence, both sides of equation 3 are incomparable.
Thus the constraint is satisfiable, and we obtain the TRS R = {1, 2}. This TRS is indeed
terminating, but it is not maximal terminating.
Finally, in our implementation we do not compute all maximal terminating
TRSs. This is because there still may be exponentially many maximal terminating
TRSs. Instead, we fix a number K to stop the enumeration of maximal terminating TRSs whenever the number reaches K. This is motivated by the following
observation: Assume that there exists a complete TRS R ∈ R(C), but we fail toselect it. Since R is a terminating TRS over C ∪ S(C), by Lemma 4.1.4 (a) there
exists a maximal terminating, complete TRS R0 ∈ R(C ∪ S(C)) with R ⊆ R0 .
Thus when missing the complete TRS R in one iteration, there is still a chance toselect R0 in the next one.

54

4.3 Related Work4.2.2 Filtering Equalities
Our implementation of the parameter function S(C) follows closely the proposed
one of Section 4.1, but adds a few small operations as described below.
When orienting equalities to rules, some equalities tend to generate a lot of
critical pairs. This is why Knuth-Bendix completion employs selection heuristics(cf. [10, 83, 85]) that select only certain kinds of equalities. We also heuristicallyselect equalities, since otherwise the number of critical pairs grows too fast andour implementation fails to handle it. In order to address it, we first normalize
the equalities to filter out all those whose size exceeds a bound d. Then, we selectthe n smallest equalities. If they are not uniquely defined, i.e. there are several
equalities of the same size, we simply select equalities in the order in which they
were generated. We formulate this filtering. For a set of equalities C , we write
C <d to denote all equalities s ≈ t of C with |s| + |t| < d. Moreover we write C n
for the set of the n smallest equalities in C . With these notations, S(C) can be
described as follows:[
S(C) ={s↓R ≈ t↓R | s ≈ t ∈ E ∪ CP(R) and s↓R 6= t↓R }<d nR∈ R(C)

4.3 Related WorkWe relate our procedure ϕ to existing completion methods described in Chapter 3. Due to their algorithmic nature precise simulations are difficult, but we
capture their main features. We say that S is an inter-reduced version of a terminating TRS R, if S is a terminating reduced TRS whose rules are obtained byrewriting rules in R by R itself.
• Knuth-Bendix Completion. Let > be a reduction order for the KnuthBendix completion procedure and for the orientable part {` → r ∈ C ∪C −1 | ` > r } we write C > . The Knuth-Bendix completion procedure (cf.
Section 3.1) can be simulated by ϕ if one uses
R(C) = {C > }and

S(C) = {s↓R0 ≈ t↓R0 }where R0 is an inter-reduced version of C > and s ≈ t ∈ C ∪ CP(R0 ).
• Multi-completion. As mentioned in Section 3.3, Multi-completion uses aclass of reduction orders >1 , . . . , >n to run Knuth-Bendix completion in parallel, and typically the class is the set of all possible recursive path orders.
Its run can be simulated in our method as follows:
R(C) = {C >1 , . . . , C >n }andS(C) = {s↓R0 ≈ t↓R0 }55

Chapter 4: Maximal Completion
where, R0 is an inter-reduced version of C >i and s ≈ t ∈ C ∪ CP(R0 ). A
naive implementation of this approach fails due to the large number ofcompatibility checks as well as computations of normal forms. As illustrated in Chapter 3, the specialized data structure node allows to share thesecomputations among the orders.
• Completion with termination tools. As introduced in Section 3.2, this procedure does not require a reduction order as an input parameter, because
during its process a necessary reduction order is constructed on the fly:R(C) = {R}S(C) = {s↓R0 ≈ t↓R0 }andwhere, R is a TRS over C whose termination is shown by a termination tool,
R0 is an inter-reduced version of R, and s ≈ t ∈ C ∪ CP(R0 ). Unlike afixed single reduction order, a termination tool can find a number of terminating TRSs over C , which avoids failure of Knuth-Bendix completion.
The main drawback of this procedure is similar as with multi-completion,and in n [83] a heuristic for the best-first search strategy is suggested to select one of the terminating TRSs. Nevertheless, this approach significantly
extends the power of Knuth-Bendix completion, and has been adopted intheir completion tool Slothrop.
• Multi-completion with termination tools (cf. Chapter 3.4). The method
replaces reduction orders in multi-completion by a termination tool:
R(C) = {R1 , . . . , Rn }andS(C) = {s↓R0 ≈ t↓R0 }where, R1 , . . . , Rn are all TRS over C whose termination is shown by atermination tool, R0 is an inter-reduced version of some R ∈ R(C), ands ≈ t ∈ C ∪ CP(R0 ). A variant of the node data structure that is used in
multi-completion provides a compact representation of R(C) as well as anefficient algorithm to compute it. This approach has been implemented in
the very effective completion tool mkbTT.
As stated before, maximal completion only computes maximal terminating
TRSs, which are often much fewer than all terminating TRSs, but it does notmiss a complete TRS. This is the main idea of our approach. One drawback isthe current limited power of maximal termination provers. Theoretically, brute
force search allows using a termination tool to compute maximal terminating
TRSs. However, it is practically infeasible due to exponentially many calls of thetermination tool.
Another difference is the definition of S(C). Except for maximal completion, allprocedures use a single equality in S(C) and its selection is critical for successful
runs. The next example illustrates this.

56

4.3 Related Work

Table 4.1: Summary for all 115 equational systems
LPO

KBO

termination tool

mkbTT Maxcomp

mkbTT Maxcomp

mkbTT

Slothrop

completed

70

86

67

69

81

71

failure

6

6

3

3

3

4

timeout

39

23

45

43

31

40

Example 4.3.1. Recall the ES E in Example 4.1.5:
1:s(p( x )) ≈ x2:p(s( x )) ≈ x

3:s( x ) + y ≈ s( x + y )We perform ϕ(E ) as the simulated run of multi-completion, where the class of reduction
orders is all LPOs with total precedence. Assume that our selection strategy for S(C)prefers an equality derived from the critical pair of rule 3 and the rule of the biggest
possible index for some TRS in R(C).
(i) R({1, 2, 3}) = {{1, 2, 3}, {1, 2, 30 }}, which both do not satisfy the join-conditionof ϕ. Thus, ϕ({1, 2, 3}) = ϕ({1, . . . , 4}), where 4 is the single equality inS({1, 2, 3}):4 : x + y ≈ s(p( x ) + y )(ii) R({1, . . . , 4}) = {{1, 2, 3, 40 }, {1, 2, 30 , 40 }} and the join-condition does not holdagain. We continue the run with ϕ({1, . . . , 4}) = ϕ({1, . . . , 5}), where 5 inS({1, . . . , 4}) is
5 : ( x + y) + z ≈ s((p( x ) + y) + z)(iii) Generally, we have R({1, . . . , n}) = {{1, 2, 3, 40 , . . . , n0 }, {1, 2, 30 , 40 , . . . , n0 }}and S({1, . . . , n}) is the singleton ofn +1 :(( x1 + x2 ) + · · · ) + xn−1 ≈ s(((p( x1 ) + x2 ) + · · · ) + xn−1 )for n ≥ 3. Thus, the join-condition never holds and the procedure does not terminate.
Admittedly, for the above example it is easy to choose an appropriate selection
strategy that succeeds. In general however, it is difficult to know a suitable selection strategy a priori. This is why mkbTT provides several selection strategies

57

Chapter 4: Maximal Completion
90

mkbTT/LPO
Maxcomp/LPO
mkbTT/KBO
Maxcomp/KBO
mkbTT/TTT2
Slothrop/AProVE

completed systems

80
70
60
50
40
30

1

5

10
60
time (sec)

180

360

Figure 4.1: Comparison of execution times.
as a user parameter. Maximal completion does not use a singleton but a set of
equalities for S(C), which reduces the risk to get stuck.
To conclude, we like to stress the simplicity of maximal completion, due to
avoiding a dedicated search algorithm like the one in Slothrop, and a sophisticated but complex data structure like that of multi-completion. The only major
drawback is that maximal completion is practically limited to methods of showing termination that can be encoded to constraints. This can prevent to find acomplete TRS even if one exists for a given ES. For example to complete thetheory CGEn of n commuting group endomorphisms [83], advanced termination techniques are required which can not be encoded as a constraint problem.
Consequently, maximal completion cannot (practically) complete CGEn .

4.4 Experiments
We implemented maximal completion in the tool Maxcomp. The tool employs
the SMT solver Yices [22] to support LPO and KBO. Concerning parameter K for
R(C) in Section 4.2, at the beginning we use K = 2 to compute two maximal
terminating TRSs. During the recursion of ϕ, we increase K whenever S(C) ⊆ C .
If, at some point, no new equalities are generated and all maximal terminating
TRSs are computed (i.e. the parameter K cannot be increased any more), the toolstops with failure. Moreover, we fix n = 7 and d = 20 for S(C). These values
were chosen heuristically, see below for a brief discussion on their effect.

58

4.4 Experimentscompleted systems

90

80

70

60
Maxcomp/LPO
Maxcomp/KBO

50

0

2

4

6
8
parameter K

10

12

14

Figure 4.2: Computation of maximal terminating TRSs ("K").
We compare Maxcomp with the two existing completion tools Slothrop andmkbTT. Since the latter two require termination provers, we used AProVE [28]for Slothrop, and for mkbTT its internally supplied prover TTT2 [50]. The test-bed
consists of 115 equational systems from the distribution of mkbTT.1 The tests were
single-threaded run on a system equipped with an Intel Core Duo L7500 with 1.6
GHz and 2 GB of RAM using a timeout of 300 seconds.
Table 4.1 gives a summary of the overall results. Here we also included results,
where mkbTT’s termination proving power was limited to LPO and KBO2 (this is
not possible for Slothrop). Aside from this, all parameters of all tools were left attheir default values. A full list of all results can be found in Appendix A.
It should be noted that the complete systems found by using a termination tool
are mostly different from those found with LPO or KBO, since the reduction order constructed using a termination tool is usually different from them. Table 4.1
suggests that Maxcomp succeeds whenever mkbTT or Slothrop succeed, but thisis not the case. In fact for each tool there exist equational systems for which thetool succeeds to find a complete TRS, but both of the other tools fail to do so.
For almost all equational systems in the test-set complete TRSs are known. The
reason why the tools fail or time out however is different with respect to each tool.
Maxcomp mostly fails or times out when it is not possible to show terminationof the known complete TRS for the ES in question by LPO or KBO. For Slothrop,
the reason for a timeout is usually that its best-first search algorithm picks the1 http://cl-informatik.uibk.ac.at/software/mkbtt/
2 mkbtt -s lpo for LPO, and mkbtt -s kbo for KBO.

59

Chapter 4: Maximal Completion
wrong branch in the search tree and is unable to recover from that, and mkbTT
faces a similar problem. It should be noted however that by choosing specific,
suitable selection strategies for each equational system individually, mkbTT cancomplete more systems than with its default selection strategy. To name one
example, mkbTT completes SK90.3.22 with LPO and selection strategy old [85]within roughly 40 seconds, however times out after 300 seconds with all otherpredefined strategies (max, slothrop, sum). While the chosen selection strategy
vastly affects the outcome of mkbTT, it is in general non-trivial to decide which
selection strategy to choose in advance.
Concerning the timeout, with very few exceptions, a higher timeout seems
not to affect the results. A notable exception are the group axioms with two
commuting endomorphisms CGE2 [83], for which Slothrop was the first tool toautomatically construct a complete TRS. Here however Slothrop fails to complete
CGE2 within 300 seconds.
All in all, as can be seen in Figure 4.1, Maxcomp is the fastest tool. The reason
is that significant time during completion is spent on termination analysis, andthe constraint-based approach of Maxcomp outperforms the use of termination
tools. For overall performance, whenever all tools succeeded, they usually (withfour exceptions) did so in less than 35 seconds. For the rest of systems, timing
values do not show a clear trend. As seen in Figure 4.2, the parameter K mostly
remains unchanged at 2, and for the vast majority of successful runs does notexceed 5, the maximum being 14. It seems that the computation of few maximal
terminating TRSs suffices to guide the search process in the right direction.
One might think that other parameters (n and k) of Maxcomp should heavily
affect the outcome of the experiments, but in practice their overall influence israther small. For example with settings n = 7 and d = 21, and n = 7 and d = 19
using LPO, the completed systems did not change at all. For n = 8 and d = 20 the
ES LS94.P1.trs could be completed, but completion of SK90.3.28.trs did notterminate. Lastly for n = 6 and d = 20 the ESs LS94.P1.trs and SK90.3.26.trs
were completed, but again, the run on the ES SK90.3.28.trs did not terminate.
An explanation for this behavior is that with no bound n and k at all we haveexponential growth of the set C due to the exponential number of critical pairs.
However, fixing n and k with any values ensures that the growth of C becomes
constant, which suffices to get practically good results.

60

Chapter 5
Constrained Equalities

Most calculi for (inductive) theorem proving are based on the idea of finding
a terminating TRS that satisfies certain joinability requirements of equalities (cf.
Chapter 3). Thereby an equational proof is transformed into a search problem.
To find such a TRS the inference rules of completion are adapted. However theyusually require a fixed reduction ordering as an input parameter.
Chapter 4 illustrated how completion can be fully automated by reformulating
it as an optimization problem over constraints. As seen, this also yields a practically highly efficient procedure. The key ingredient in the reformulation is theuse of maximality (Lemma 4.1.4). It states that given a set of candidate equalities,
it can never be harmful to choose a terminating superset of the required rules.
Thus one can maximize the choice of rules with respect to orientability.
In inductive theorem proving, such a choice does not fit, even if only (inductively) valid equations are considered. For example, in rewriting induction an
analogous formulation would be that if R and H are TRSs with R quasi-reducible
and R ∪ H terminating and Expd(R, H) ⊆ ↓R∪H , then for all H0 with H ⊆ H0
and R ∪ H0 terminating and R `i H0 we have Expd(R, H0 ) ⊆ ↓R∪H0 , cf. Theorem 3.5.3. Unfortunately this is not the case.
Example 5.0.1. Recall the TRS R of Example 3.5.5:
1:0+y → y2:s( x ) + y → s( x + y )61Chapter 5: Constrained Equalities
Suppose we have additionally the following two equations
3:( x + y) + z ≈ x + (y + z)

4:x + s( x ) ≈ s( x + x )and we want to prove that R `i {3}. One can verify that indeed all the conditionsof the above (false) conjecture are met. Suppose we orient rules 3 and 4 from left toright and expand at leftmost, innermost basic positions. If we take H = {3} thenExpd(R, H) ⊆ ↓R∪H which implies R `i {3} by Theorem 3.5.3. However whenchoosing the superset H = {3, 4} we have Expd(R, H) 6⊆ ↓R∪H even though both 3
and 4 are valid inductive theorems.
To summarize, choosing an appropriate set of equations H among candidates
to solve the associated joinability problem Expd(R, H) ⊆ ↓R∪H is a highly nontrivial task. Clearly, maximality with respect to the number of orientations is nota suitable criterion.
To address this problem we attach constraints to each equation. From such
constrained equalities one can infer information on how selecting this equation
will affect the joinability problem, namely how many unjoinable equations it
will induce. Such additional information allow to again formulate these more
complicated joinability requirements as optimization problems, and automate
them in a similar fashion to maximal completion.
The framework turns out to be very flexible. Due to the abstract nature of theconstraints it allows easy adaptations to various settings. In Section 5.1 we introduce the framework of constrained equalities, and in Section 5.2 we show how
inductionless induction and rewriting induction (cf. Chapter 3) can be formulated
in it. In maximal completion there is no possibility to apply inter-reduction. In
contrast to maximal completion, constrained equalities allow to formulate completion with inter-reduction as well, which is also done in Section 5.2, and in
Section 5.3 it is shown how such an approach can be automated. In the practical experiments of Section 5.4 however it turns out that exploiting maximality
in completion and maximizing as in maximal completion is more effective thanusing an approach based on constrained equalities. In contrast, for our main
objective, namely inductive methods, we obtain a fully automatic and practicallyefficient procedure. Finally we compare our approach with related work in Section 5.5.

5.1 Constrained Equalities
We introduce termination constraints. The syntax is given by the next BNF C
C ::= ` → r | > | ⊥ | ¬C | C ∨ C | C ∧ C

62

5.1 Constrained Equalities
A TRS R satisfies a constraint C if R |= C holds. Here R |= C is inductively
defined on C as the standard interpretation of Boolean connectives together withthe following base case: R |= ` → r if and only if ` → r ∈ R.
A constrained equality is a pair of an equality on terms and a constraint. A
constrained equational system, in short CES, C is a set of constrained equalities. Let
R be a terminating TRS. The R-projection of C is the ES given by{s ≈ t | (s ≈ t, C ) ∈ C and R |= C }and is denoted by C JRK. Below we write
define the following notations:

V

R for

V

`→r ∈R ` → r. For brevity, we

E > = {(s ≈ t, >) | s ≈ t ∈ E }no^ 
C R = s ≈ t, C ∧ ¬ R | (s ≈ t, C ) ∈ Cno^ C↓R = s↓R ≈ t↓R , C ∧ R | (s ≈ t, C ) ∈ C and s↓R 6= t↓R
The intuition behind these notations is as follows. E > denotes constrained equalities obtained from sets of equalities, and C↓R rewrites the equational part in
C to some normal form. However an added constraint ensures that the newly
obtained normal forms will be only triggered by the TRS R with which they
were normalized with. Lastly C R removes R from the constrained part, andthus we have R 6|= C R. The next lemmata state important properties of thesenotations. Their proofs are straightforward by unfolding the above definitions.
Lemma 5.1.1. If E > ↓R = ∅ then E ⊆ ↓R .
Lemma 5.1.2. (CR)JRK = ∅.

Our main concern is a joinability problem of C , namely, C JRK ⊆ ↓R . But for
inductive theorem proving, one has only to consider ground joinability: We saythat an ES E is ground joinable for R if sσ ↓R tσ whenever s ≈ t ∈ E and sσ, tσ ∈T (F ). A function S is a (ground) joinability reflection for (ground) joinability
problems if for every constrained ES C and every TRS R (ground) joinabilityof S(C)JRK for R implies that of C JRK. We give a simple criterion for testingwhether S is a (ground) joinability reflection. Below we say A ⊆ B on (ground)terms, if for all s ≈ t ∈ A and all (ground) substitutions σ on s and t we havesσ ≈ tσ ∈ B.
Lemma 5.1.3. S is a (ground) joinability reflection if C JHK ⊆ →∗H · ↔=· ∗←S(C)JHK H
on (ground) terms for all C and H.
Proof. We show that S is a (ground) joinability reflection if the inclusion of thelemma holds for (ground) terms. Let C be a CES and H be a TRS. Assume

63

Chapter 5: Constrained Equalities
S(C)JHK is (ground) joinable for H. Then for any s ≈ t ∈ S(C)JHK and any
substitution σ we have sσ ↓H tσ. Together with∗C JHK ⊆ →∗H · ↔=S(C)JHK · H ←we have C JHK ⊆ ↓H . Thus (ground) joinability of C JHK for H holds. Hence S isa reflection.

5.2 Constraints for Joinability Problems
In this section we show how completion and variants can be recast as joinability
problems using joinability reflections.
Definition 5.2.1. Let R be a function from CESs to a set of terminating TRSs, and F bea function from TRSs to ESs. In the following we use the notation
SR (C) = (CS(C) =R) ∪ C↓R ∪ F (R)> ↓R , and[SR (C).

R∈R(C)

Lemma 5.2.2. S is a (ground) joinability reflection.
Proof. Let s ≈ t ∈ C JHK and R ∈ R(C). According to Lemma 5.1.3 it is sufficient
to show sσ →∗H · ↔=· H∗ ← tσ for all (ground) substitutions σ. By the
S(C)JHK
assumption there is a C with (s ≈ t, C ) ∈ C and H |= C. We distinguish threecases.
• If R ⊆ H and s↓R = t↓R then sσ ↓R tσ for all (ground) substitutions σ, andthus sσ ↓H tσ.
• If R ⊆ H and s↓R 6= t↓R then H |= C ∧ R. Thus s↓R ≈ t↓R ∈ SR (C)JHK.
Therefore sσ →∗H s↓R ↔SR (C)JHK t↓R H∗ ← tσ for all (ground) substitutionsσ.
V• If R * H then H |= C ∧ ¬ R. Thus, we have s ≈ t ∈ SR (C)JHK, which
implies sσ ↔SR (C)JHK tσ for all (ground) substitutions σ.
VLemma 5.2.3. If S(C)JRK = ∅ and R ∈ R(C), then F (R) ⊆ ↓R .
Proof. Let R ∈ R(C) and s ≈ t ∈ F (R). Because R |=must have s↓R = t↓R , and thus s ↓R t.

64

V

R and S(C)JRK = ∅, we5.2 Constraints for Joinability Problems

5.2.1 Completion
In this section, we specify parameters to derive our completion criterion withinter-reduction. Let E be an ES. Below we assume that SKB (C) is an instance of theabove reflection S so that R(C) is a set of terminating TRSs with R ⊆ ↔∗E for all
R ∈ R(C), and F (R) = CP(R).
n (E > ). If C JRK = ∅ for some R ∈ R(C), then R is
Theorem 5.2.4. Let C = SKB
complete for E .

Proof. Let R ∈ R(C) and C JRK = ∅. Easy induction on n shows that the n-foldn being a reflection iscomposition of a reflection forms a reflection. Thus, SKB
implied by Lemma 5.2.2 and we obtain E ⊆ ↓R . Together with R ⊆ ↔∗E , whichholds by assumption, we obtain ↔∗R = ↔∗R . We now distinguish two cases: If
n = 0 then E must be empty. Since termination of R and the inclusion R ⊆ ←→∗Eentail emptiness of R, the claim trivially holds. If n > 0, it is not difficult to
see that C JRK = ∅ implies SKB (C)JRK = ∅. Thus by Lemma 5.2.3 we have
CP(R) ⊆ ↓R which implies confluence of R. Together with termination of Rand ↔∗R = ↔∗R completeness of R for E follows.
In the following examples we assume that R(C) is a singleton.
Example 5.2.5. Consider the ES E consisting of the following equations:
1 : s(p( x )) ≈ x

2 : p(s( x )) ≈ x

3 : s( x ) + y ≈ s( x + y )We thus obtain three initial constraints C0 = E > = {(1, >), (2, >), (3, >)}. Assuming
R0 = {1, 2, 3} ∈ R(C0 ) and abbreviating R0 = 1 ∧ 2 ∧ 3 results in the constraints
C1 = {(1, ¬ R0 ), (2, ¬ R0 ), (3, ¬ R0 ), (4, >)} where 4 is derived from the critical overlap
h1, 1, 3i:
4:x + y ≈ s(p( x ) + y )Now we can for instance take R1 = {1, 2, 30 , 40 } ∈ R(C1 ). We write R1 as a shorthandfor 1 ∧ 2 ∧ 30 ∧ 40 , and obtain

C2 = {(1, ¬ R0 ∧ ¬ R1 ), (2, ¬ R0 ∧ ¬ R1 ), (3, ¬ R0 ∧ ¬ R1 ), (4, ¬ R1 ), (5, >), (6, >)}where 5 and 6 are new equalities obtained from the critical overlaps h30 , 1, 2i and h40 , 1, 2i,
respectively:5:p(s( x ) + y) ≈ x + y,

6:p( x + y ) ≈ p( x ) + y

For R2 = R0 ∪ {40 , 5, 60 } ∈ R(C2 ) we now have SKB (C2 )JR2 K = ∅, so R2 is complete
for E . Note that this would also hold for the smaller (inter-reduced) system R20 ={1, 2, 3, 60 }, which is actually complete.

65

Chapter 5: Constrained Equalities
We remark that in Example 5.2.5 SKB (C2 )JR20 K = ∅, and thus completenessof R20 can be inferred directly from the attached constraints in C2 . In maximal
completion this information is not available, and a non-inter-reduced TRS suchas R2 is always selected (cf. Example 4.1.5). Of course one question is how toautomatically construct R20 from C2 . This is the subject of Section 5.3.

5.2.2 Inductionless Induction
Furthermore, Gramlich’s criterion 3.5.2 for inductionless induction can be instantiated. Note that when talking about inductive theorem proving, throughout thisand the next section we consider TRSs to be sorted (cf. Chapter 3).
We recall Theorem 3.5.2:
Lemma 5.2.6 ([34]). Let R = R0 ∪ H be a terminating, and left-R0 -inductivelyreducible TRS. If CP(R0 , H) ⊆ ↓R , then R0 `i H.
Lemma 5.2.7. Let R = R0 ∪ H be a TRS, such that R0 `i H, and E be a set of
equalities. If E ⊆ ↓R on ground terms, then R0 `i E .
Let R0 be a TRS and E an ES. We assume that SG (C) is an instance of S so that
F (R) = CP(R0 , R \ R0 ) and R(C) is a set of terminating and left-R0 -inductivelyreducible TRSs.
n (E > ). If C JRK = ∅ for some R ∈ R(C), then R ` E .
Theorem 5.2.8. Let C = SG
0 i

Proof. Let R ∈ R(C) and C JRK = ∅. Analogous to Theorem 5.2.4, we obtainE ⊆ ↓R on ground terms. Again, we distinguish two cases: If n = 0 then E
must be empty, and the claim trivially holds. If n > 0 then by C JRK = ∅ we
obtain SG (C)JRK = ∅, and by Lemma 5.2.3, we have CP(R0 , R \ R0 ) ⊆ ↓R .
Since R is terminating and left-R0 -inductively-reducible, by Lemma 5.2.6 wehave R0 `i (R \ R0 ). Together with E ⊆ ↓R , by Lemma 5.2.7 we have R0 `i E .
Example 5.2.9. Consider the TRS R0 consisting of the following rules:
1:0−x → 02:s( x ) − 0 → s( x )4:p(0) → 05:p(s( x )) → x

3:s( x ) − s( y ) → x − yand E the single equality6:p( x − y ) ≈ p( x ) − y

Here we assume the signature to be sorted with 0 : nat, p, s : nat → nat and +, − : nat ×
nat → nat. We obtain the initial constraints C0 = {(6, >)}. Choosing R1 = {1, . . . , 6}from R(C0 ) results in the following constraint equations

C1 = SG (C0 ) = {(6, ¬R1 ), (7, >), (8, >)}66

5.2 Constraints for Joinability Problems
where 7, 8 are
7:x−0 ≈ x

8:p( x ) − y ≈ x − s( y )Let R2 = {1, . . . , 8} be in R(C1 ), resulting in

C2 = {(6, ¬R1 ∧ ¬R2 ), (7, ¬R2 ), (8, ¬R2 )}Suppose R2 is again included in R(C2 ) and chosen as R3 . Then SG (C2 )JR3 K = ∅. One
can verify that indeed R1 , . . . , R3 are left-R0 -inductively reducible and terminating.
Thus R0 `i E .

5.2.3 Rewriting Induction
As mentioned in Chapter 3, Rewriting Induction [62] relaxes the joinability conditions of inductionless induction. Instead of requiring all critical pairs to bejoinable, joinability of only a specific subset suffices.
In the following, we assume R(C) to be a set of R0 -expandable, terminating
TRSs such that for every R ∈ R(C), we have R0 ⊆ R and `σg ↔∗R0 ∪E rσg for all` → r ∈ R and ground substitutions σg . We assume SRI (C) to be an instance of
S with F (R) = Expd(R0 , R).
Lemma 5.2.10 ([62]). Let R and H be TRSs such that R is quasi-reducible TRS, andR ∪ H is terminating. If Expd(R, H) ⊆ ↓R∪H , then R `i H.
n JRK = ∅ for some R ∈ R(C), then R ` E .
Theorem 5.2.11. If SRI
0 i

Proof. Similar to Theorem 5.2.8, using Lemma 5.2.10.
Example 5.2.12. Consider the following TRS R0 :1:

x+0 → 02:

x + s( y ) → s( x + y )and E the single equality
3:( x + y) + z ≈ x + (y + z)

As previously, we assume the signature to be sorted, here with 0 : nat, s : nat → nat and+ : nat × nat → nat. We obtain the initial constraints C0 = {(3, >)}. Suppose R(C0 )is the singleton R0 = {1, 2, 3}. Then expanding 3 results in

C1 = SRI (C0 ) = {(3, ¬R0 ), (4, >)}where 4 is
4:x + z ≈ x + (0 + z )5:s( x + y ) + z = x + (s( y ) + z )67Chapter 5: Constrained Equalities
In fact it is not difficult to see that orienting 5 and 3 will lead to an infinite run. However,suppose now that R(C1 ) is the singleton R1 = {1, 2, 30 }. Expansion leads to

C1 = SRI (C0 ) = {(3, ¬R0 ∨ ¬R1 ), (4, ¬R0 ), (5, R0 )}With R1 , we have SRI (C)JR1 K = ∅. One can verify that R0 is quasi-reducible, and theposition 1 of the rhs of equation 3 is basic. Thus R0 `i E .
Example 5.2.12 illustrates two important facts: First, similar as in Knuth-Bendix
completion, the orientation of an equation to a rule is crucial, and a bad choice
can easily lead to divergence. Secondly, in practice it is not necessary to exhaustively compute all TRSs at once. A bad choice can be always recovered at laterstage.

5.3 Automation
The challenge when automating our framework is the question how to find a setof terminating TRSs R(C) given a set of constrained equalities C . We first show
how to find a TRS R that satisfies a termination constraint by solving a boolean
constraint. We then illustrate how this can be used to formulate an optimization
problem over boolean constraints to automate the search for a set terminating
TRSs R(C) among candidates C that fulfill the desired joinability requirements.
SAT/SMT-encodings of termination conditions based on existing subclasses of
reduction orders are well established nowadays, cf. [52, 17, 88, 23]. All of them
can test the existence of a tuple of an assignment of boolean variables and areduction order ( M, ) that satisfies arbitrary Boolean combinations of boolean
variables and order constraints:
C ::= s > t | x | > | ⊥ | ¬ C | C ∨ C | C ∧ C
Here, for the base cases, we define ( M, ) |= ` > r if `  r and ( M, ) |= x if x istrue in M, and extend this inductively to arbitrary formulas. Note the difference
to Chapter 4 where the second base does not exist and the constraints allow not
additional boolean variables.
All encodings of termination conditions allow to further automatically translate constraints of form s > t with respect to a class of reduction orders to Boolean(or SMT) constraints. Therefore one can treat order constraints as an instance of
MaxSAT/MaxSMT. When encoding order constraints w.r.t. specific classes of reduction orders, one needs to carefully distinguish termination constraints andorder constraints.
Let ψ be a termination constraint. We write Rules(ψ) for the set of all rulesthat appear in ψ. We associate with each rule ` → r ∈ Rules(ψ) a fresh booleanb for the constraint generated by replacing each ` → r ∈variable x`→r , and write ψ685.3 Automation
Rules(ψ) by the associated variable x`→r in ψ. In the following we write R( M,)for the TRS{` → r ∈ Rules(ψ) | ( M, ) |= x`→r }.
The next lemma shows how to find a solution (a TRS) to a termination constraint
by solving an order constraint.
Lemma 5.3.1. Let ψ be a termination constraint. Suppose ( M, ) is a model such that^

( M, ) |= ψb ∧¬ x`→r ∨ ` > r.

`→r ∈Rules(ψ)

Then R( M,) |= ψ.
Proof. The proof is by induction on the structure of ψ. We only show the imporb = x`→r . Since ( M ) |= x`→r wetant base case here. Let ψ = ` → r. Then ψhave by definition ` → r ∈ R( M,) . Moreover since ( M, ) satisfies the part^¬ x`→r ∨ ` > r`→r ∈Rules(ψ)

we have `  r. Thus R is terminating. Hence R |= ψ.
Lemma 5.3.1 is useful to automate the search for a TRS that satisfies a termination constraint. Nevertheless another questions remains, namely given a set of
constrained equalities C how to compute a TRS R such that C JRK = ∅.
In general there is no complete way to find a suitable TRS among candidates.
To find a suitable measure we use the the following approach. For a TRS R withC JRK = ∅ we have R |= ¬C for all (s ≈ t, C ) ∈ C . If C JRK 6= ∅ there exists some(s ≈ t, C ) ∈ C with R |= C. Then it makes sense to try to orient s ≈ t, since whenorientable, the equation is at least joinable in the next iteration.
To sum up, we try to solve the joinability problem of a CES C by iteratively
enumerating candidate TRSs. Similarly to Chapter 4 we write
Maximize S subject to ϕ
for the problem of finding an assignment that maximizes the number of satisfied elements in the set S while satisfying ϕ. Given k failed (i.e. C JRK 6= ∅)TRSs R1 , . . . , Rk , we solve the following maximal satisfaction problem ψ overtermination constraints:
Maximize{¬C ∨ s → t ∨ t → s}(s≈t,C)∈C

subject to

k
^

¬

^

Ri

i =1

69

Chapter 5: Constrained Equalities
This can be translated to the following satisfaction problem χ over order constraints:
Maximize{¬Cb ∨ xs→t ∨ xt→s }(s≈t,C)∈C
k
^
i =1

¬(

^
`→r ∈Rix`→r ) ∧subject to^¬ x`→r ∨ ` > r`→r ∈Rules(ψ)

Then the following lemma holds.
Lemma 5.3.2. Suppose ( M, ) |= χ. Then R( M,) |= ψ.
Proof. Quite similar to Lemma 5.3.1.
If the satisfaction problem is not satisfiable, we have exhaustively computed all
potential TRSs over the candidate equations w.r.t. our measure.

5.4 Experiments
We implemented both completion and rewriting induction. In both cases, the
SMT solver Yices [22] is used to solve ordered constraint problems. Encoded isthe class of all lexicographic path orders and the class of all Knuth-Bendix pathorders. The tests were single-threaded run on a system equipped with an Intel
Core Duo L7500 with 1.6 GHz and 2 GB of RAM, using a timeout of 10 seconds
for rewriting induction, and a timeout of 60 seconds for completion. A full list of
all results can be found in Appendix B.

Completion
A straight-forward implementation of completion fails. The set of critical pairs
is exponential at worst, and maximizing the set of oriented equations yields exponential growth in practice. For example for group-theory [49], which consistsof only three equations initially, after a few iterations several hundred equations
are contained in C .
Moreover, some equations tend to generate a lot of critical pairs, a problem
which all completion procedures face. Several selection heuristics have been proposed to avoid such equations. In our implementation we use a similar approach.
Instead of taking the whole equational part of C as candidates for the TRS R, weonly select certain equations from C . We write C <d for{(s ≈ t, C ) ∈ C | |s| + |t| < d}70

5.4 Experiments
and we write C n for the set of the n smallest (w.r.t. the size of the equationalpart) constrained equalities in C . We refine the encoding from Section 4.2 to thefollowing maximality problem over termination constrains:
Maximize{¬C ∨ s → t ∨ t → s}(s≈t,C)∈(C <d )nsubject to

k
^

¬

^

Ri

i =1

In our implementation we fix d = 20, we start with parameter n set to 7, andincrease n by 7 with each iteration. These values were experimentally chosen;larger parameters could not be processed by our tool.
One should remark at this point the difference between Maximal Completion(Chapter 4), and the current approach. In Maximal Completion, equations in
S(C) are directly reduced. The condition for soundness of the procedure —specific to completion — needs to be ensured separately. Here however, theconditions for soundness are directly encoded in the constraint part of S(C).
The test-bed consists of 115 equational systems contained in the distribution of
mkbTT.1 Table 5.1 gives a summary of the overall results. For comparison we also
include results from Maxcomp, for comparison here with a timeout of 60 seconds.
The experiments clearly show that maximal completion is more effective thanthe current constraint based approach. From our observation there are two reasons for it. The first one is that maintaining termination constraints for eachequation and evaluating them creates some non-trivial overhead. The second
reason however is maximality. In the approach based on constrained equations
we optimize the selection of a TRS among candidate equations with respect tothe number of unjoined equations. Thus equations that would create additional
critical pairs will not be selected. Theoretically this should increase the performance.
However maximality ensures that adding such equations can never be harmful.
And in practice in a lot of cases it is quite beneficial to add such equations because
it decreases the chance to miss an important equation, i.e. the selection strategy
becomes less important as illustrated in Example 4.3.1. Moreover the additionaltime spent for constructing additional critical pairs is marginal.

Rewriting Induction
The set Expd is a subset of all critical pairs. Thus, in Rewriting Induction, theset C grows much slower compared to Completion, and no specific selection
is necessary. In fact, in practice it rarely happens that the proof fails due tocomputational resources. Rather, a failed proof attempt is due to other reasons,such as the need for additional lemmata. Thus our implementation follows theapproach described in Section 4.2.
1 http://cl-informatik.uibk.ac.at/software/mkbtt/

71

Chapter 5: Constrained Equalities

Table 5.1: Summary for 115 equational systems
LPO

KBO

Maxcomp Constraints

Maxcomp Constraints

completed

86

47

69

33

failure

6

6

3

3

timeout

23

62

43

79

Table 5.2: Summary for 73 inductive conjectures
LPO

KBO

success

32

21

timeout

41

52

The test-bed consists of 73 (valid) inductive conjectures from the (no longer
maintained) Dream Corpus of Inductive Conjectures, and from [66]. Results of a
prototype implementation are depicted in Table 5.2.
To the best of our knowledge there are no fully automated inductive theorem
provers except for [66], which is an adaptation of multi-completion to inductive
theorem proving, called multi-context rewriting induction. They report 35 solved
conjectures on the Dream Corpus. The combined number of examples solved
by our approach using the class of LPOs and KBOs on the Dream Corpus is 32.
Thus our approach has a quite comparable performance. Moreover multi-context
rewriting induction uses a termination tool to construct a reduction order on the
fly. Of course, this is more powerful than a constraint encoding of all LPOs andKBOs. While no detailed data are provided in [66] we strongly suspect that thesmall difference in proven conjectures can be mostly attributed to that. One has
to clearly state that despite its benefits the fact that not all methods of showing
termination can be encoded to constraints is the biggest drawback of our method.

72

5.5 Related Work

5.5 Related Work
We compare existing frameworks and their proof techniques with our framework
based on constrained equalities. For existing frameworks see also Chapter 3.
• Completion. Proving soundness of completion procedures is intricate, especially when inter-reduction is used. The first complete proof of Knuthand Bendix’ procedure including inter-reduction was due to Huet [40] andappeared roughly eleven years afterwards. Moreover it only shows soundness for one particular implementation of the algorithm, and even minor
modifications can easily violate soundness [69, 75]. In order to address thisproblem, Dershowitz, Plaisted, Bachmair and Hsiang [12, 11] recast Huet’s
completion in inference rules. They employed a new proof technique called
proof orderings, which significantly simplifies soundness-proofs in completion. Due to its universality, nowadays this framework is the most popular
way to formalize various completion procedures, including ordered completion, inductionless induction, and rewriting induction. In our soundness proof, a simple reflection for joinability problems is used instead of
the proof ordering method.
• Multi-Completion [51]. The above framework of inference rules requires a
fixed reduction order, which is used to show the necessary termination of
the generated systems. Since it is hard to know a suitable order a priori,
often one has to restart the process with another order, which usually requires user interactions. Kondo and Kurihara introduced an efficient data
structure, the node, to run completion procedures with different orders inparallel. Adaptations are highly efficient and have been used for several
settings ([66, 84]). However each adaptation requires careful formulation as
well as a specific soundness proof which seems a non-trivial task. Usually,soundness is established by extracting a single run out of the procedure,
and then applying the proof-ordering approach.
• Maximal Completion [46]. The original maximal completion can be simulated if > is always associated to equalities. Inter-reduction was not available in maximal completion but by using constrained equalities we can fully
recover this functionality. Folklore suggests that inter-reduction improves
efficiency in completion, but in our approach this is not the case as seen inexperimental data. This is because rather than reducing terms, avoiding adiverging processes is more critical for a successful run. Moreover, by notusing inter-reduction, more equalities are shared among different orderings, which avoids missing suitable equalities. The overhead costs, i.e. the73

Chapter 5: Constrained Equalities
increased amount of time needed for processing equalities are neglectablecompared to other costs.
Soundness in Maximal Completion is ensured directly from Knuth andBendix’ criterion (Theorem 2.4.5). This, together with a lack of explicit configurations — which are needed to maintain the joinability requirements in
inductive reasoning — prohibit to formulate other procedures in it.
We conclude this chapter by emphasizing the advantages of our framework
based on constrained equalities. For one, it is universal enough to formulate
several completion procedures with minimal effort. Here we showed formulations for completion, inductionless induction and rewriting induction. But otherprocedures can be easily expressed as well by varying the parameters S and
F. Secondly, proofs for soundness can easily be established using a reflection.
Lastly, experiments indicate practical feasibility. One has to note however, thatMaximal Completion’s practical strength is unparalleled, and future work should
investigate data-structures to improve scalability, as done in multi-completion.

74

Chapter 6
Confluence and Relative Termination

For terminating TRSs, confluence follows from local confluence, which itself canbe tested by the joinability of critical pairs. Since the construction of criticalpairs relies purely on syntactical properties, critical pairs can be effectively computed, and a confluence test can be fully automated. For non-terminating TRSs,
confluence is undecidable. For non-terminating but left-linear TRSs, confluence
criteria can be given by restricting the shape of the join-relation. Essential hereis that left-linearity allows to trace untouched redexes over several rewrite steps
using the notion of residuals (cf. Chapter 4 of [75]). Together with the absence of(non-trivial) critical pairs, this allows to derive effectively automatable confluence
criteria.
Unfortunately, for non-terminating and non-left-linear TRSs, none of these approaches work. The following example, due to Huet, gives an intuition for theunderlying problems:
Example 6.0.1 ([39]). Consider the following TRS:
1 : f ( x, x ) → a

2 : f ( x, g( x )) → b

3 : c → g (c)which is non-confluent sincea ← f (c, c) → f (c, g(c)) → b
and a and b are not joinable.

75

Chapter 6: Confluence and Relative Termination
Joinability of critical pairs does not imply confluence in the absence of termination, as can be inferred from Example 6.0.1, where the set of critical pairs is
empty. In orthogonal systems, rewriting residuals of one step after another stepor vice-versa results in the same end term, but non-left-linear rules destroy thisproperty. Thus, in the case of non-left-linear and non-terminating TRSs, not only
can none of the abstract notions like local confluence be utilized, also none of thetechnical tools, such as (syntactical) critical pairs or residuals are applicable, andno established tool-set is available.
Therefore one has to fundamentally modify these notions to yield new criteria.
Existing approaches [31, 44] use an extended notion of critical pairs to formulate
suitable joinability conditions. These extensions however come with a price topay, as they require equational unification, which itself is undecidable. Thus
even if sound criteria can be formulated with these extended notions, extra careis needed to ensure computability. For example, Jouannaud and Kirchner’s result
is practically limited to TRSs where associativity and commutativity (AC) are thecause of non-termination, since there, effective algorithms to solve AC-unification
exist. Gomi et al. developed a sound, but incomplete approximation algorithm
to practically apply their criterion.
In Section 6.1, we present a new confluence criterion for non-left-linear andnon-terminating TRSs, which is based on (modest) syntactic restrictions and relative termination, and show its application with some examples. Then we givea proof in Section 6.2. Our criterion also requires joinability of extended criticalpairs. However we provide a result on unification in Section 6.3, that ensures thatjoinability can be tested by computing syntactic unifiers only. With it we develop
a fully automatic procedure and evaluate it experimentally in Section 6.4. Finallyour result is compared with existing works in Section 6.5.

6.1 Confluence Criterion
We first need a few non-standard notions in term rewriting to state our main
result. We write →1 /→2 for →2∗ · →1 · →2∗ , and →R/S for →R /→S .
Definition 6.1.1. A TRS R is relatively terminating over a TRS S (we also say R/Sis terminating), if →R/S is terminating.
In Definition 2.4.4, we defined syntactical critical pairs. We now give an extended notion of overlaps and critical pairs. An extended rewrite rule is a pair(`, r ) of terms with ` 6∈ V , and an extended TRS (eTRS) is a set of extended rewrite
rules.
Definition 6.1.2. Let R1 , R2 , S be eTRSs. An S -overlap (`1 → r1 , p, `2 → r2 )σ of R1
on R2 consists of a variant `1 → r1 of a rule in R1 and a variant `2 → r2 of a rule in76

6.1 Confluence Criterion

R2 , a position p ∈ P osF (`2 ), and a substitution σ, such that the following conditions
hold:• `1 σ ↔∗S `2 | p σ, and• if p = ε, then `1 → r1 and `2 → r2 may not be variants of each other
The pair (`2 σ[r1 σ ] p , r2 σ) induced from the overlap is an S -extended critical pair (orsimply S -critical pair) of `1 → r1 and `2 → r2 at p, written`2 σ[r1 σ] p R1 ←S ∝ →R2 r2 σ.
We will simply write CPS (R) for R ←S ∝ →R , namely the S -critical pairs originatingfrom S -overlapping rules from R on R.
Example 6.1.3 (continued from Example 6.0.1). Consider again Example 6.0.1 andthe TRSs R = {1, 2} and S = {3}. Then e.g.

( f ( x, x ) → a, e, f ( x, g( x )) → b ){ x7→c}is an S -overlap of R. Its induced critical pair is (b, a).
It should be remarked that the definition of (S -)critical pairs includes pairs
originating from non-minimal unifiers. Usually, they are excluded to guarantee finiteness of the set of critical pairs. Thus, for example taking the previous
Definition 2.4.4, even when considering only a TRS R (and no eTRS), the inclusion CP∅ (R) ⊆ CP(R) does not hold in general. However due to the existence of mgu’s for critical pairs (see Section 6.3), we may restate Knuth andBendix’ criterion (Theorem 2.4.5) as: A terminating TRS is confluent if and only
if CP∅ (R) ⊆ ↓R .
Let REN(t) denote a linear term resulting from replacing in t each variableb for the eTRS
occurrence by a fresh variable. We write R{REN(`) → r | ` → r ∈ R}.
Definition 6.1.4. A TRS S is strongly non-overlapping on R if Sb has no (syntactic)
b . We write SNO(R, S) if both S is strongly non-overlapping on R, andoverlaps on R
R is strongly non-overlapping on S .
Example 6.1.5 (continued from Example 6.0.1). Consider again Example 6.0.1. We
have SNO({1, 2}, {3}). But SNO({1}, {2}) does not hold, since{d1} = {f ( x1 , x2 ) → a} and {d2} = {f ( x3 , g( x4 )) → b}
are syntactically overlapping, as f ( x1 , x2 ) and f ( x3 , g( x4 )) unify.

77

Chapter 6: Confluence and Relative Termination
We have now all the definitions to state our main theorem.
Theorem 6.1.6. Suppose that S is confluent, R/S is terminating, and SNO(R, S).
The union R ∪ S of the TRSs is confluent if and only if CPS (R) ⊆ ↓R∪S .
Note that the theorem is a proper generalization of Knuth and Bendix’ confluence criterion when S 6= ∅, and coincides with it when S = ∅. The next
examples illustrate Theorem 6.1.6. Note that no existing tool can prove confluence of the involved TRSs automatically (see Section 6.4).
Example 6.1.7. Consider the TRS
1 : f ( x, x ) → ( x + x ) + x

2: x + y → y + x

Take R = {1} and S = {2}. One can easily verify SNO(R, S). Termination of R/S
can be established using a termination tool such as TTT2 v1.06 [50]1 , and confluence of S
follows from orthogonality. Because of CPS (R) = ∅ ⊆ ↓R∪S , we conclude confluenceby Theorem 6.1.6.
Example 6.1.8. Consider the TRS
2 : ∞ → s( ∞ )1 : f ( x, x ) → s(s( x ))Take R = {1} and S = {2}. As in Example 6.1.7, one can easily verify the conditionsof Theorem 6.1.6, including CPS (R) = ∅ ⊆ ↓R∪S . Hence the TRS is confluent.
Example 6.1.9. Consider the TRS
1 : eq(s(n), x : xs, x : ys) → eq(n, xs, ys)2:eq(n, xs, xs) → T

3:nats → 0 : inc(nats)

4 : inc( x : xs) → s( x ) : inc(xs)Take R = {1, 2} and S = {3, 4}. Again, SNO(R, S), termination of R/S and confluence of S is established. Moreover, one can show
CPS (R) = {(eq(s, t, u), T) | s, t, u are terms and t ↔∗S u}
and thus the set is included in ↓R∪S because of confluence of S . Hence by using Theorem 6.1.6 we infer that R ∪ S is confluent.
We conclude this section by mentioning that all conditions of Theorem 6.1.6 areessential. One cannot drop SNO(R, S) nor replace joinability of S -critical pairs
by joinability of critical pairs.
1 http://colo6-c703.uibk.ac.at/ttt2/

78

6.2 Correctness of the Criterion
Example 6.1.10 (continued from Example 6.0.1). Recall that the TRS in Huet’s example consists of
1 : f ( x, x ) → a

2 : f ( x, g( x )) → b

3 : c → g (c)which is non-confluent. If one takes R = {1} and S = {2, 3}, then R/S is terminating,
S is confluent, and CPS (R) = ∅ ⊆ ↓R∪S , however SNO(R, S) is violated. If one takes
R = {1, 2} and S = {3} then, SNO(R, S), R/S is terminating, S is confluent andR ← ∝ →R = ∅ ⊆ ↓R∪S . Yet the non-joinable S -critical pair a R ← ∝ →R b exists.
Also, termination of R/S is essential. We illustrate it with another famous
non-confluent and non-left-linear TRS, due to Klop:
Example 6.1.11. Consider Klop’s example [48]
1 : f ( x, x ) → a

2 : g( x ) → f ( x, g( x ))3 : c → g (c)which is known to be non-confluent, sincea ← f (g(c), g(c)) ← f (c, g(c)) ← g(c) → g(g(c)) →∗ g(a)and a and g(a) are not joinable. If one would take R = {1, 2} and S = {3}, then
SNO(R, S), S is confluent, and CPS (R) = ∅ ⊆ ↓R∪S . However R/S is nonterminating, since rule number 2 is looping.

6.2 Correctness of the Criterion
We now give a proof of the main theorem 6.1.6. In the proof we will make useof the decreasing diagram technique [79, 81] of van Oostrom, a powerful confluence
criterion for abstract rewrite systems.
Let A = ( A, h→α iα∈ I ) be an ARS and > a well-founded order on I. For every∨α ∈ I we write −→α for{→ β | β ∈ I and β < α},
∨

∨

∨

∨

∨

and −
→∗α for (−→α )∗ . The union of −→α and α ←− is denoted by ←−−→α . For α, β ∈ I,∨∨∨
the union of −→α and −→ β is written as −→αβ .
Definition 6.2.1. Two labels α and β are decreasing with respect to > if
α ← · →β

∨

∨

∨

⊆ ←
→∗α · →=−−→∗αβ · =α ← · ←
→∗β
β · ←

Decreasingness is illustrated in Figure 6.1. An ARS A = ( A, h→α iα∈ I ) is decreasing
if there exists a well founded order > such that every two labels in I are decreasing withrespect to >.

79

Chapter 6: Confluence and Relative Termination

·

α

·

∨

α

∗

·

β

=

β

·

∨

αβ

∗

·

=

·

∗

α

∨

·

β

Figure 6.1: Decreasingness
Decreasingness allows to formulate a very powerful confluence criterion on
ARSs.
Theorem 6.2.2 ([81]). Every decreasing ARS is confluent.
We recall an example from [81] to illustrate how to use the decreasing diagram
technique to show confluence of TRSs.
Example 6.2.3. Recall the “if”-direction of Lemma 2.1.6 (Newman), which, when applied
to TRSs, states that a terminating and locally confluent TRS is confluent. Let R be aterminating and locally confluent TRS. To apply Theorem 6.2.2, we need to associate an
ARS with the TRS R. We will consider the ARS A with the set A as T (F , V ), and we
introduce labels by labeling rewrite steps by its source: We label a step s → t as s →s t.
Lastly we need to compare labels by an ordering >, here we choose > := →+R . Since R
is terminating, > is a well-founded order.
Now consider any peak s ← · →v . By the definition of source labeling we have v = s,i.e. s ← · →s , and there exist u and t such that u ← s → t. By local confluence of R,
there exists a sequence
u → R u1 → R . . . → R u n R ← t m R ← . . . R ← t1 R ← t
and thus a labeled sequence
u →u u1 →R . . . →un−1 un tm ← tm tm−1 ← . . . t1 ← t1 t ← t.
We have s > u and s > ui for all 1 ≤ i < n, and s > t and s > t j for all 1 ≤ j ≤ m.
Therefore A is decreasing, and thus by Theorem 6.2.2 confluent. Moreover confluence ofA readily implies confluence of R.
In our proof, we do not directly show confluence of the rewrite relation. Let
R and S be TRSs. We introduce an intermediate relation _, such that →R∪S ⊆_ ⊆ →∗R∪S . Confluence of this intermediate relation readily implies confluence80

6.2 Correctness of the Criterionof R ∪ S . The relation _ is defined as the union of →RS and →∗S , where RS is
the TRS{`0 σ → rτ | `0 ρ → r ∈ R and σ →∗S ρτ for some variable substitution ρ }Here σ →∗S τ means that xσ →∗S xτ for all variables x.
Remark 6.2.4. It is important to note thata) in the definition of RS , linearity of `0 can be assumed without loss of generality, andb) the inclusions →R ⊆ →RS ⊆ →∗S · →R hold.
We show confluence of _ by the decreasing diagram technique with the predecessor labeling [81]: We write b _a c if a _∗ b _ c. Labels are compared withrespect to →+R/S , denoted by >. Since termination of R / S is presupposed in thetheorem, the relation > forms a well-founded order.
The next lemma states a general property of rewriting in substitutions.
pLemma 6.2.5. Let R be a TRS. If tσ −→R u and p 6∈ P osF (t) then u →∗R tτ for some
τ with σ →=R τ.
pProof. Suppose tσ −→R u and p 6∈ P osF (t). Then there exists a variable positionq ∈ P osV (t) with q 6 p and u = (tσ )[u|q ]q . Let Q be the set of all positions of t|q
in t. Since u|q0 →R u|q holds for all q0 ∈ Q \ {q}, we have u →R (tσ)[u|q ]q0 ∈Q\{q} .
The latter term is identical to (tσ )[u|q ]q0 ∈Q . We define the substitution τ as follows:(u|q if x = t|qτ (x) =
xσ otherwise∗
One can verify σ →=R τ and ( tσ )[ u |q ]q0 ∈ Q = tτ. Hence u →R tτ.

We analyze peaks of the form ^ · _. According to the definition of _, theyfall into the three cases: (a) S∗ ← · →∗S , (b) RS ← · →∗S , and (c) RS ← · →RS . For
case (a) we can apply confluence of S to show decreasingness of the peak. The
remaining cases are more complicated. We start with a localized version of (b). In
the next Lemmata 6.2.6, 6.2.9, and 6.2.10 we assume SNO(R, S) and confluenceof S .
Lemma 6.2.6. If t RS ← s →S u then t →∗R∪S · RS∗ ← u.
pq

Proof. We perform induction on s. Suppose t RS ←− s −→S u. By the definition
of RS we may assume `1 ρ → r1 ∈ R for some linear term `1 and ρ : V → V ,s| p = `1 σ, t| p = r1 τ, and σ →∗S ρτ, as well as `2 → r2 ∈ S , s|q = `2 µ, andu|q = r2 µ. Due to SNO(R, S), neither p\q ∈ P osF (`2 ) nor q\ p ∈ P osF (`1 ) holds.
We distinguish several cases concerning the relation of p and q.

81

Chapter 6: Confluence and Relative Termination• Suppose p = ε. Then there is a variable position q1 of x1 in `1 with q1 6 q.
Since x1 ρτ S∗ ← x1 σ →S u|q1 holds, we have x1 ρτ →∗S v S∗ ← u|q1 for some v
by confluence of S . We define the substitutions µ1 and ν as follows:((u|q1 if x = x1v
if x = x1 ρ
µ1 ( x ) =ν( x ) =xσotherwisexτ otherwise
We have τ →∗S ν, and also u = `1 µ1 by linearity of `1 . Moreover, µ1 →∗S ρν
because xµ1 →∗S v = x1 ρν = xρν if x = x1 , and xµ = xσ →∗S xν otherwise.
Therefore, we obtain t = r1 τ →∗S r1 ν RS ← `1 µ1 = u.
• Suppose q = ε. We may presume V ar(`1 ) ∩ V ar(`2 ) = ∅, and thus σ = µ canbe assumed. Since `2 σ →RS t holds, by Lemma 6.2.5 we obtain t →∗RS `2 ν∗∗
for some ν with σ →=RS ν. Thus, t →RS `2 ν →S r2 ν RS ← r2 σ = r2 µ = u.
• If p = ip0 and q = jq0 for some i, j ∈ N with i 6= j, one can easily verifyqpt−→ S · RS ←− u.
• Otherwise, p = ip0 and q = iq0 for some i ∈ N. Since t|i RS ← s|i →S u|iholds, the induction hypothesis yields t|i →∗R∪S · RS∗ ← u|i . Thereforet →∗R∪S · RS∗ ← u.

In order to handle peaks of shape RS ← · →∗S we show auxiliary lemmata for
ARSs. In the next two lemmata → stands for →1 ∪ →2 and > for (→1 /→2 )+ ,and we write b → a c if a →∗ b → c.
Lemma 6.2.7. The next two properties hold:∨∨(a) For all a, b, c, d with a > b, if b ←−−→∗a c →∗ d then b ←−−→∗a d.
∨(b) For all a, b, c with a →∗ b →1∗ c there exists some d such that b →1= d −→∗a c.
Proof. (a) We distinguish three cases: If b = c, then each step of b →∗ d can be∨labeled by b itself. Since a > b was assumed, we have b ←−−→∗a d. If b 6= c then∨there exists some e and label a0 with a > a0 such that either b ←−−→∗a e → a0 c →∗ d∨or b ←−−→∗a e a0 ← c →∗ d. In both cases we have a0 →∗ c, and thus again all steps∨of c →∗ d can be labeled with a0 to obtain b ←−−→∗a d. (b) First note that the claim
trivially holds if b →1= c. Otherwise we distinguish whether a = b. If a 6= b, then∨we can label each step of b →1∗ c by b itself and obtain b −→∗a c. Otherwise there
exists some d with b →1 d →∗ c. We can label each step of d →∗ c by d. Since to∨a →1+ b and b →1 d, we have b →1 d −→∗a c.
∨

Lemma 6.2.8. Let 1 ← · →2 ⊆ →∗ · ∗1 ←. If b 1 ← a →2∗ c then b ←−−→∗a · =1 ← c.

82

6.2 Correctness of the Criterion
Proof. Let b 1 ← a →2n c. We show the claim by induction on n. If n = 0 thentrivially the claim holds. Otherwise, a →2n−1 d →2 c for some d. The induction∨
hypothesis yields b ←−−→∗a e =1 ← d for some e. We distinguish two cases.
∨∨• If d = e then b ←−−→∗a e = d →1 c. Thus b ←−−→∗a c by (1).
• Suppose d →1 e. Because we have e 1 ← d →2 c, by the assumption e →∗∨f ∗1 ← c for some f . Since a →2∗ d →1 e →∗ f holds, we obtain e −→∗a f by∨∨(2). Moreover, c →1∗ f implies c →1= · −→∗a f by (2). Hence, b ←−−→∗a · =1 ← c.
∨

Lemma 6.2.9. If t RS ← s →∗S u then t ^_∗s · R=S ← u.

Proof. By Lemma 6.2.6 we have that t RS ← s →S u implies t →∗R∪S · RS∗ ← u. The
claim follows by instantiating Lemma 6.2.8 with →1 as →RS and →2 as →S .
Lastly, peaks of case (c), of shape RS ← · →RS , are considered.
∨Lemma 6.2.10. If t RS ← s →RS u then t ^_∗s u or t →∗S · ↔CPS (R) · S∗ ← u.
pq

Proof. We perform induction on s. Suppose t RS ←−s−
→RS u. By the definition
of RS we can assume `1 ρ1 → r1 , `2 ρ2 → r2 ∈ R for some linear terms `1 , `2 andρ1 , ρ2 : V → V , ands| p = `1 σ1

t| p = r1 τ1

σ1 →∗S ρ1 τ1

s|q = `2 σ2u|q = r2 τ2

σ2 →∗S ρ2 τ2

Except for symmetric cases, the relation of p and q falls into the next four cases:• Suppose q = ε, and p ∈ P osF (`2 ). We have `1 ρ1 τ1 S∗ ← s →∗S `2 | p ρ2 τ2 .
Without loss of generality V ar(`1 ρ1 ) ∩ V ar(`2 ρ2 ) = ∅, and thus we may
assume τ = τ1 ∪ τ2 is a well-defined substitution. The substitution τ is an
S -unifier of `1 ρ1 and `2 ρ2 | p . Because xσ2 →∗S xρ2 τ holds for all x ∈ V ar(`2 ),t = (`2 σ2 )[r1 τ ] p →∗S (`2 ρ2 τ )[r1 τ ] p ↔CPS (R) r2 τ = u• Suppose q = ε, and p 6∈ P osF (`2 ) and p2 is a variable occurrence of x2
in `2 with p2 6 p. Since t| p2 RS ← x2 σ2 →∗S x2 ρ2 τ2 , Lemma 6.2.9 yields∨∨
t| p2 ^_∗s| p v R=S ← x2 ρ2 τ2 for some v. Because s = `2 σ2 , t| p2 ^_∗s| p v, and22σ2 →∗S ρ2 τ2 hold, by closure under contexts of rewrite relations and > we
obtain∨t = (`2 σ2 )[t| p2 ] p2 ^_∗s (`2 σ2 )[v] p2 →∗S (`2 ρ2 τ2 )[v] p2∨

Thus, t ^_∗s (`2 ρ2 τ2 )[v] p2 . Since x2 ρ2 τ2 →=RS v holds and `2 is linear,`2 ρ2 τ2 →=RS (`2 ρ2 τ2 )[ v ] p2

83

Chapter 6: Confluence and Relative Termination
s

s

s1

t

s2

s1

s2

v

s1

u

t

(a) S∗ ← · →∗S

∨ ∗
v
s1

s
s1

s2

=
s1

u

∨
s1

t

(b) RS ← · →∗S

s2
∗

u

(c) RS ← · →RS

Figure 6.2: Decreasingness of _.
is deduced. Here we distinguish two cases. If `2 ρ2 τ2 = (`2 ρ2 τ2 )[v] p2 , weobtain∨t ^_∗s `2 ρ2 τ2 →R u
Otherwise, `2 ρ2 τ2 →RS (`2 ρ2 τ2 )[v] p2 . Since by Lemma 6.2.5 there exists ν∗with τ2 →=RS ν such that (`2 ρ2 τ2 )[ v ] p2 →RS `2 ρ2 ν, finally we obtain∨t ^_∗s (`2 ρ2 τ2 )[v] p2 →∗RS `2 ρ2 ν →R r2 ν RS∗ ← r2 τ2 = u∨

Because s > t and s > u hold, in both cases t ^_∗s u is concluded.

• If p = ip0 and q = jq0 for some i, j ∈ N with i 6= j, one can easily verifypq∨− u, which implies t ←−−→∗s u.
t−→ RS · RS ←• Otherwise, p = ip0 and q = iq0 for some i ∈ N. Since t|i RS ← s|i →RS u|i∨holds, by the induction hypothesis t|i ←−−→∗s| u|i or t|i →∗S · ↔CPS (R) · S∗ ← u|ii∨
is deduced. Thus, t ←−−→∗s u or t →∗S · ↔CPS (R) · S∗ ← u is concluded.

Now we are ready to prove the main theorem.
Proof of Theorem 6.1.6. Suppose that S is a confluent TRS, R/S is terminating,and SNO(R, S). We show that R ∪ S is confluent if and only if CPS (R) ⊆↓R∪S . Since the “only if”-direction is trivial, we only show the “if”-direction.
Assume CPS (R) ⊆ ↓R∪S . Because confluence of _ implies confluence of R ∪ S ,according to Theorem 6.2.2 it is enough to show decreasingness of _. Let t s1 ^s _s2 u. As mentioned, following the definition of _, we distinguish three cases.
(a) If t S∗ ← s →∗S u then t →∗S v S∗ ← u for some v by confluence of S .
∨(b) If t RS ← s →∗S u then t ^_∗s v R=S ← u for some v by Lemma 6.2.9.
∨(c) If t RS ← s →RS u then t ^_∗s u for some v by Lemma 6.2.10 and joinabilityof S -critical pairs.
In all cases decreasingness is established, as seen in Figure 6.2.

84

6.3 Joinability of Extended Critical Pairs

6.3 Joinability of Extended Critical Pairs
The biggest challenge in applying Theorem 6.1.6 is to check CPS (R) ⊆ ↓R∪S
automatically. The problem is that CPS (R) may contain infinitely many pairs.
Before proceeding, we extend the notions of unifiability and unifiers from
Chapter 2. Let E and S be sets of equations, and X the set of all variables in
E . Note that a TRS can be taken for S . An S -unification problem is a finite setof equalities {s1 ≈ t1 , . . . , sn ≈ tn }. Given a substitution σ, we write E σ for{sσ ≈ tσ | s ≈ t ∈ E }.
Definition 6.3.1. Let E be an S -unification problem. An S -unifier of E is a substitution
σ such that E σ ⊆ ↔∗S .
A substitution σ is more general than a substitution σ0 on X (σ .SX σ0 ), if there
exists a substitution τ such that xσ0 ↔∗S xστ for all x ∈ X.
Definition 6.3.2. Let U be a set of S -unifiers of E .
1. U is complete if for every S -unifier of E there is a more general element in U , and
2. if in addition all elements in U are minimal with respect to .SX , we call U minimal
complete.
3. A substitution σ is an S -most general unifier (S -mgu) of E , if {σ } is a minimal
complete set of S -unifiers of E .
The special case of S = ∅ corresponds to syntactic unification, unifiers and mgu’s as
defined in Chapter 2.
A set of equalities E = { x1 ≈ t1 , . . . , xn ≈ tn } is in solved form, if the xi are
pairwise distinct variables, and none of the xi occurs in any t j . For E in solved−→
form, we write E for the induced substitution { x1 7→ t1 , . . . , xn 7→ tn }. Note thatin contrast to syntactic unifiability (S = ∅), S -unifiability does not ensure theexistence of an S -mgu in general.
The standard approach to test CPS (R) ⊆ ↓R∪S is to compute a minimal complete set of S -unifiers for `1 and `2 | p for each combination of rules `1 → r1 ,`2 → r2 and a position p ∈ P osF (`2 ). Then, joinability of its induced criticalpairs ensures joinability for all S -unifiers. However, depending on S , the computation of minimal complete sets varies, and worse, minimal complete sets may
not even exist for S -unifiable terms. In this section we give sufficient conditions
for the joinability and non-joinability of S -critical pairs without performing specific equational unification algorithms.
For the first we show that a most general unifier of strongly S -stable terms
is always a most general S -unifier. As the next lemma shows, this allows us
to compute S -critical pairs by means of syntactic unification. Here a term t

85

Chapter 6: Confluence and Relative Terminationis strongly S -stable if for every position p ∈ P osF (t) there are no term u andεsubstitution σ such that t| p σ →∗S · −→S u. Note that tσ is strongly S -stable if t
and xσ are strongly S -stable for all variables x in t.
Lemma 6.3.3. Let t be a linear term. Then (a) implies (b) wherep(a) for every σ we have that tσ −→S u implies p ∈ P osV (t),(b) for every σ we have that tσ →∗S u implies u = tτ for some τ.
Proof. By induction on the length of tσ →∗S u.
Lemma 6.3.4. If SNO(R, S) then ` is strongly S -stable for all ` → r ∈ R.
Proof. Suppose SNO(R, S) and let ` → r be a rule in R and p ∈ P osF (`).
We write t for REN(`| p ). Clearly, t is linear and by SNO(R, S) condition (a)of Lemma 6.3.3 holds for t. Thus the lemma implies that condition (b) also holds.
p

Now consider the reduction `| p σ →∗S u −→S v. It is not difficult to see that there
exists a substitution ρ with tρ = `| p σ. Then by condition (b) of Lemma 6.3.3
we have u = tτ for some τ. By condition (a) the position p must be a variableεposition, and thus p 6= ε. So `| p σ →∗S v −→ u does not hold. Hence ` must be
strongly S -stable.
In order to show the claim on mgu’s, we recall the standard inference rules forsyntactic unification from [10]. These rules are defined over sets of equalities onterms.
Eliminate
OrientDeleteDecompose{ x ≈ t} ] E{ x ≈ t} ∪ E { x 7→ t}{t ≈ x } ] E{ x ≈ t} ∪ E

if x 6∈ V ar(t)if t 6∈ V{t ≈ t} ] EE{ f (s1 , . . . , sn ) ≈ f (t1 , . . . , tn )} ] E{ s1 ≈ t1 , . . . , s n ≈ t n } ∪ E

We write =⇒ for a derivation by the inference rules. The following lemma statesthat a most general unifier can be computed by a sequence of derivations.
Lemma 6.3.5 ([10]). If s and t are unifiable, there exists E in solved form such that−→{s ≈ t} =⇒∗ E and E is an mgu of s and t.
The next lemma shows that the inference rules of syntactic unification preservestrong S -stability and S -unifiability. We say that a set E of equalities is strongly
S -stable if s and t are strongly S -stable for all s ≈ t ∈ E .

86

6.3 Joinability of Extended Critical Pairs
Lemma 6.3.6. Let S be a confluent TRS. If E1 is strongly S -stable, E1 σ ⊆ ↓S , andE1 =⇒ E2 , then E2 σ ⊆ ↓S and E2 is strongly S -stable.
Proof. Suppose E1 is strongly S -stable, E1 σ ⊆ ↓S , and E1 =⇒ E2 . We distinguishthe inference of E1 =⇒ E2 . Because the cases of Delete and Orient are trivial,
below we only consider the other two cases:• Eliminate: Suppose E1 = { x ≈ t} ] E 0 and E2 = { x ≈ t} ∪ E 0 µ, whereµ = { x 7→ t} and x 6∈ V ar(t). We claim µσ ↔∗S σ. Actually it follows fromthe assumption xσ ↓S tσ. We now prove E2 σ ⊆ ↓S . It is sufficient to showuµσ ↓S vµσ for an arbitrary u ≈ v ∈ E 0 . Because uσ ↓S vσ by assumption,
the claim yields uµσ ↔∗S vµσ. Therefore uµσ ↓S vµσ is concluded fromconfluence of S . To show strong S -stability of E2 , fix u ≈ v ∈ E 0 . Since u, v,
and xµ are strongly S -stable, so are uµ and vµ.
• Decompose: Suppose E1 = {s ≈ t} ] E 0 and E2 = {s1 ≈ t1 , . . . , sn ≈tn } ∪ E 0 with s = f (s1 , . . . , sn ) and t = f (t1 , . . . , tn ). Since E is strongly
S -stable, and thus s and t are, si and ti are also strongly S -stable for all
1 6 i 6 n. Furthermore, due to strong S -stability of s and t, sσ ↓S tσ
implies si σ ↓S ti σ for all 1 6 i 6 n. Therefore, the claim holds.

We arrive at the aforementioned sufficient condition.
Theorem 6.3.7. Let S be a confluent TRS. An mgu of strongly S -stable terms s and t
is an S -mgu of s and t.
Proof. Let µ be an arbitrary mgu of strongly S -stable terms s and t. Since µ is
trivially an S -unifier of s and t, it is enough to show that µ is more general thanan arbitrary S -unifier σ of s and t. By using Lemma 6.3.5 there is an E in solved−→
form such that {s ≈ t} =⇒∗ E and E is an mgu of s and t. Because sσ ↔∗S tσ
and S is confluent, we have {s ≈ t}σ ⊆ ↓S , and thus E σ ⊆ ↓S is obtained byinduction on the length of =⇒∗ using Lemma 6.3.6. Since E is in solved form,
−
→
−
→
−
→
xσ ↓S x E σ holds for all x ∈ D om( E ). This means σ ↔∗S E σ. Since µ is an−→mgu, there is a substitution ρ with E = µρ. Thus σ ↔∗S µρσ. Hence µ is moregeneral than σ.
When automating Theorem 6.1.6, confluence of S and SNO(R, S) can be assumed. Therefore, according to Theorem 6.3.7 and Lemma 6.3.4, a syntactical
overlap by an mgu µ is also an S -overlap by S -mgu µ. Thus joinability of its
syntactical critical pairs implies joinability of S -critical pairs induced by any S unifier.

87

Chapter 6: Confluence and Relative Termination
Example 6.3.8 (continued from Example 6.1.9). We consider again the example with
R = {1, 2} and S = {3, 4}. Take the first and second rules renamed:
1 : eq(s(n), x : xs, x : ys) → eq(n, xs, ys)

2 : eq(m, zs, zs) → T

We know that there is an overlap between 1 and 2 at root position with mguµ = {m 7→ s(n), zs 7→ x : xs, ys 7→ xs}.
Elsewhere, even S -overlaps cannot occur. The induced critical pair (eq(n, xs, xs), T) is
trivially joinable by the second rule. Hence CPS (R) ⊆ ↓R∪S holds.
Confluence of S cannot be dropped in Theorem 6.3.7.
Example 6.3.9. Consider the TRS S
g( x, y) → f ( x, x )g( x, y) → f ( x, y)

The terms f ( x1 , x1 ) and f ( x, y) are both strongly S -stable, and the substitutionµ = { x 7 → x1 , y 7 → x1 }is a most general unifier. However, µ is not an S -mgu, because µ is not more generalthan the other S -unifier { x1 7→ x }.
Unjoinability of S -critical pairs can be tested in a similar way to checking nonconfluence of a TRS with the function TCAP ([87]).
Definition 6.3.10 ([29]). Let t be a term, and R a TRS. We define TCAPR (t) inductively as a fresh variable, when t is a variable or when t = f (t1 , . . . , tn ) and ` andu unify for some (renamed) rule ` → r ∈ R, and u, otherwise. Here u stands forf (TCAPR (t1 ), . . . , TCAPR (tn )).
Lemma 6.3.11. Let `1 → r1 , `2 → r2 ∈ R and p ∈ P osF (`2 ). If `1 σ ↔∗R `2 | p σ, and
TCAPR (r2 ) and TCAPR (`2 [r1 ] p ) do not unify, R is not confluent.
Proof. Using the fact that if sσ ↓R tτ then TCAPR (s) and TCAPR (t) must unify,see [87].
Example 6.3.12 (continued from Example 6.0.1). Recall R = {1, 2} and S = {3}:1 : f ( x, x ) → a

2 : f (y, g(y)) → b

3 : c → g (c)where variables are renamed in rule 2. We denote i-th rule by `i → ri . While `1 and `2 |εare (R ∪ S)-unifiable with { x, y 7→ c}, we have
TCAPR∪S (`2 [r1 ]ε ) = a

and

TCAPR∪S (r2 ) = b

which do not unify. Thus, by Lemma 6.3.11, R ∪ S is not confluent.

88

6.3 Joinability of Extended Critical Pairs
In automation we need to test S -unifiability of `1 and `2 | p . This can be automated by first-order theorem provers for unit equational problems, so-called
UEQ. We briefly describe the approach. Roughly summarized, such theorem
provers work as follows. The input is a set of equations E and goal ϕ containing
arbitrary quantifiers
Q1 x1 , . . . , Q n x n s ≈ twhere Qi stands for either ∀ or ∃ and x1 , . . . , xn are the variables appearing in s
and t. The theorem prover tries to answer whether E |= ϕ. The approach is to
first negate and skolemize ϕ which results in a formula s0 6≈ t0 . Note that if wehave Qi = ∀ for all 1 ≤ i ≤ n then both s0 and t0 are ground terms. If s0 and t0
are E -unifiable then the goal is inconsistent with the axioms and thus we have
E |= ϕ. Most theorem provers for UEQ are based on a variant of completion
called unfailing completion [12] which is refutationally complete. This means that
if E |= ϕ then unifiability will (theoretically) be detected after a finite amount oftime and thus we are guaranteed that the conjecture will be proven.
Testing S -unifiability of `1 and `2 | p means asking whether S |= ϕ where ϕ is

∃ x1 , . . . , ∃ x n `1 ≈ `2 | p
and x1 , . . . , xn are the variables of `1 and `2 | p . If we input ϕ together with S ,then the theorem prover will check S -unifiability of `1 and `2 | p which is precisely our original question. If unifiability is proven then we can employ TCAP
and Lemma 6.3.11. Depending on the power of the prover, sometimes invalid
conjectures can be refuted, i.e. it can be shown that

S 6|= ∃ x1 , . . . , ∃ xn `1 ≈ `2 | p .
Then we can conclude the absence of S -unifiers. However in this case refutational completeness2 does not hold, i.e. the theorem prover is not (theoretically)guaranteed to refute the conjecture after a finite amount of time.
Note that in contrast to [87], Lemma 6.3.11 only requires to know that S unifiability holds, but it does not require the computation of S -unifiers. In fact
most theorem provers test only unifiability without computing any concrete unifier.
By the above approach indeed non-confluence of the TRS of Example 6.3.12
can be proven automatically, see Section 6.4. As a final remark, note that fromthe absence of a syntactic unifier we may not conclude non-existence of S -criticalpairs, as illustrated in Example 6.0.1.
2 Refutational completeness here refers to being guaranteed to show the inconsistency of theaxioms w.r.t. the negated, skolemized conjecture.

89

Chapter 6: Confluence and Relative Termination

6.4 Experiments
In order to assess feasibility of our methods, we implemented Theorem 6.1.6 together with Theorem 6.3.7 for confluence, and Lemma 6.3.11 for non-confluence.
In the next subsections we mention details of our implementation and report on
experimental data.

6.4.1 Implementation
In order to automate Theorem 6.1.6 we employed TTT2 v1.06 [50] for checking
relative termination R/S and an extended version of Maxcomp [46] for testingS -unifiability, using ordered completion. To check confluence of S , we used theexisting three state-of-the-art confluence provers: ACP v0.20 [7],3 CSI v0.1 [87],4and Saigawa v1.2 [38].5 Since termination of R ∪ S cannot be assumed, we only
test joinability of S -critical pairs by at most four rewrite steps form each side.
We give a brief overview of our procedure. Given a TRS P , we output either
YES (P is confluent), NO (P is not confluent), or MAYBE (confluence of P is neither
proven nor disproven). We enumerate all possible partitions P = R ] S , and thenfor each (R, S), we test whether SNO(R, S), termination of R/S , and confluenceof S holds. If one of these conditions does not hold, we continue with the next
partition; if none is left, we return MAYBE. Otherwise, to check the last remaining
condition of Theorem 6.1.6, namely CPS (R) ⊆ ↓R∪S , we proceed in the following
way: For all tuples (`1 → r1 , p, `2 → r2 ) where `1 → r1 and `2 → r2 are rules
from R and p ∈ P osF (`2 ), we test in the following order:
1. If REN(`1 ) and REN(`2 | p ) are not syntactically unifiable, then no S -overlap
exists, and we continue with the next tuple. Otherwise,
2. if `1 and `2 | p are syntactically unifiable with σ, the current tuple forms an
S -overlap, so we test joinability of the induced critical pair.
a) If joinability holds, we continue with the next tuple.
b) If joinability cannot be established, we test whether TCAPR∪S (r2 σ)
and TCAPR∪S (`2 σ [r1 σ] p ) syntactically unify. If they are not unifiable,
return NO. Otherwise, return MAYBE
3. if `1 and `2 | p are not syntactically unifiable, we check S |= `1 ≈ `2 | p by atheorem prover:a) If unsatisfiability of the formula is detected, no S -overlap exists, andwe continue.
3 http://www.nue.riec.tohoku.ac.jp/tools/acp/
4 http://cl-informatik.uibk.ac.at/software/csi/
5 http://www.jaist.ac.jp/project/saigawa/90

6.4 Experimentsb) If satisfiability is detected, we proceed and test syntactic unifiability of
TCAPR∪S (r2 ) and TCAPR∪S (`2 [r1 ] p ). If they are not unifiable, return
NO. If they unify, return MAYBE.
c) Lastly, if the theorem prover does not provide a conclusive answer,
return MAYBE
If no tuple remains, we have established CPS (R) ⊆ ↓R∪S and return YES.
The procedure has the following properties. Let 1 : `1 → r1 and 2 : `2 → r2 beprules of R and p ∈ P osF (`2 ). Below we write 1 ←−S ∝ →2 for the S -critical pairsof `1 → r1 and `2 → r2 at p.
p• If the procedure continues after step 1) or 3a) then 1 ←−S ∝ →2 = ∅.
p

• If the procedure continues after step 2a) then 1 ←−S ∝ →2 ⊆ ↓R by Theorem 6.3.7 and Lemma 6.3.4.
p• If the procedure outputs NO then 1 ←−S ∝ →2 * ↓R by Lemma 6.3.11.
Using these properties one can show correctness of the whole procedure using
Theorem 6.1.6.

6.4.2 Experimental Results
We tested the implementation on a collection of 32 TRSs, consisting of 29 non-leftlinear non-terminating TRSs in the Confluence Problem Database (Cops Nos. 1–
116)6 and Examples 6.1.7, 6.1.8 and 6.1.9. Note that Examples 6.0.1 and 6.1.11 arepart of the 29 TRSs. The tests were single-threaded run on a system equippedwith an Intel Core Duo L7500 with 1.6 GHz and 2 GB of RAM using a timeoutof 60 seconds.
The results are depicted in Table 6.1. For more more detailed results see Appendix C. In Table 6.1, columns ACP, CSI and Saigawa show results for running
the respective tools, and ACP∗ , CSI∗ and Saigawa∗ show results when using therespective tool to show confluence of the S -part in Theorem 6.1.6.
It should be noted, that the criteria implemented by Saigawa apply only to leftlinear systems, whereas CSI is able to show confluence of non-left-linear systems
by order-sorted decomposition [25], and the implementation of ACP includes criteria based on layer preserving [59] and persistency decompositions [5], and thecriterion by Gomi et al. [33].
For overall results, there are twelve TRSs for which confluence can be shown by
ACP, CSI and Saigawa combined, in fact however all twelve can be shown by ACP
alone. Extending with Theorem 6.1.6, there are 19 TRSs, for which confluence can
6 http://coco.nue.riec.tohoku.ac.jp/

91Chapter 6: Confluence and Relative Termination

Table 6.1: Summary of experimental results (32 TRSs)
ACP

ACP∗

CSI

CSI∗

Saigawa

Saigawa∗

YES
NO

12
3

19
4

7
3

15
3

0
0

10
2

MAYBE

17
0

9
0

17
5

9
5

32
0

20
0

timeout (60 sec)

be shown by ACP∗ , CSI∗ or Saigawa∗ combined. Similar to the standalone-case,
ACP∗ subsumes both other combinations. As for Example 6.1.7, 6.1.8 and 6.1.9,
neither CSI, ACP nor Saigawa can show confluence, whereas all CSI∗ , ACP∗ andSaigawa∗ succeed. Out of the nine TRSs that ACP∗ missed, four TRSs (Cops Nos.
76, 77, 78, 109) contain AC rules, for which most likely the criterion in [44] applies
if suitable equational unification algorithms were implemented (see Section 6.5),
and five TRSs (Nos. 16, 24, 26, 27, 47) are variants of Huet’s example (Example 6.0.1) or Klop’s example (Example 6.1.11).

6.5 Related Work
Among others, we compare our criterion with three well-known criteria capableof proving confluence of non-left-linear and non-terminating TRSs. Note that forthe second criterion below we use reversibility [6] for comparison, because theoriginal criterion requires equational systems for S rather than rewrite systems.
We say that a TRS S is reversible if S ← ⊆ →∗S .
• Criteria by Non-E-Overlappingness. The criterion by Gomi et al. [31],later extended in [32] and [33], is that a non-E-overlapping TRS, that is alsostrongly weight-preserving or strongly depth-preserving, is confluent. Here Eoverlaps are a generalization of overlaps, and strong non-overlappingness
plays a major role in deriving decidable criteria for non-E-overlappingness.7
A TRS is strongly depth preserving, if for any rewrite rule and any variableappearing in both sides, the minimal depth of the variable occurrences in
the left-hand side is greater than or equal to the maximal depth of the righthand side’s occurrences. Instead of comparing the depth of the variable
7 S -overlaps are sometime called E -overlaps but should not be confused with the E-overlaps

defined by Gomi et al. [31], originally introduced by Ogawa [57].

926.5 Related Work
directly, one can also assign weights to function symbols and compare theweight of the variable occurrence, where the weight is the sum of the function symbols from root to its occurrence. For details of the definitions werefer to [33]. Consider the following TRS:f ( x, x ) → a

c → g (c)g( x ) → f ( x, x )Confluence of this TRS can be established, since it is depth-preserving androot-E-overlapping. However Theorem 6.1.6 cannot be applied, since the
TRS cannot be partitioned into a non-empty R and S , such that R/S isterminating — except for R = ∅. On the other hand, weight-preservationand depth-preservation impose strong syntactic restrictions on the variable
positions. Consider for example the TRS
1 : g( x, x ) → f ( x )2 : f ( x ) → f (f ( x ))By taking R = {1} and S = {2}, Theorem 6.1.6 can be applied. However
the second rule violates both strong depth and strong weight-preservation.
• Criteria by Extended Critical Pairs.
In [44], based on the preliminary
work in [43], Jouannaud and Kirchner show that the union of a TRS R anda reversible TRS S is confluent if R/S and B/↔S are terminating and∗∗∗R ←S ∝ →R∪S∪S −1 ⊆ →R,S · ↔S · R,S ←Here s →R,S t if there exist a rule ` → r ∈ R, a position p ∈ P os(s), anda substitution σ, such that s| p ↔∗S `σ and t = s[rσ] p . Note that S has aserious restriction: The two termination requirements prohibit application
when S is erasing or collapsing, or even when C [t] ↔∗S t for a non-empty
context C. For instance, Examples 6.1.8 and 6.1.9 cannot be handled due tothis restriction. On the other hand it is applicable for mutually overlapping
TRSs R and S , for example:
1: x + x → x

2: x + y → y + x

3 : ( x + y) + z → x + (y + z)

By taking R = {1} and S = {2, 3}, one can easily show confluence ofR ∪ S by using their criterion. However, Theorem 6.1.6 cannot be applied
because R and S overlap on each other. This criterion forms a foundationof AC-completion.
• Criteria by Relative Termination. Geser [27] introduced several pioneering applications of relative termination. A result of particular interest in93

Chapter 6: Confluence and Relative Termination
this context is the following confluence criterion: A TRS R ∪ S is confluent
if R is left-linear, S is confluent, and the inclusions∗∗
S ←∅ ∝ →R ⊆ (→S · R∪S ←) ∪ (→R · ↓R∪S )andR ←∅ ∝ →R ⊆ ↓R∪S

hold. In contrast to Theorem 6.1.6, overlaps between rules in R and S pose
no problem. The following example, due to Geser, shows the power of his
approach beyond pure left-linear systems:
1 : c(s( x ), s(y)) → c( x, y)

2 : c( x, x ) → f (c( x, x ))Then confluence can be established by taking R = {1} and S = {2},whereas Theorem 6.1.6 is not applicable. 8 The reason for being able to handle overlaps between R and S is, that with the restriction of left-linearityof the R-part, joinability of syntactical critical pairs suffices to establish
confluence. On the other hand, the requirement of left-linearity prevents
application for Examples 6.1.7, 6.1.8 and 6.1.9, except for choosing R = ∅.

8 All current confluence tools fail to show confluence of the one rule TRS consisting of rulenumber 2.

94

Chapter 7
Conclusion and Future Work

We have developed a new framework for completion, called maximal completion, that allows to characterize it as an optimization problem over constraints.
The framework has been adapted to allow a similar maximality-based approachfor various adaptations of completion to inductive theorem proving by meansof constrained equalities. Moreover we showed a new and easily automatable
criterion for confluence of non-left-linear and non-terminating TRSs.
In all the above our implementations followed very closely the theoreticalframeworks to show their practical effectiveness. Nevertheless, to make our results accessible and useful in other domains, highly practical tools have to be
developed. Especially in Chapter 5 experimental results show potential for improvements. In fact such optimization is currently being undertaken in preparation for [4]. Preliminary results indicate that in fact vast improvements in performance can be achieved by optimizing the implementation.
Maximal completion’s main drawback is that it is currently restricted to methods of showing termination that can be encoded to Boolean constraints. It istherefore crucial to recapitulate termination techniques into maximal termination to extend the capability of Maxcomp. In particular, the dependency pairmethod [8] and semantic labeling [89] are known to be extremely powerful techniques of showing termination of TRSs. Techniques that to show maximal termination based on these methods would greatly benefit maximal completion.

95

Chapter 7: Conclusion and Future Work
The application of completion to theorem proving is an important direction.
Several first order theorem provers like Waldmeister [53] are based on unfailingcompletion [12]. In Chapter 6 we briefly mention an extension of maximal completion. Due to its very ad-hoc nature these extensions are not covered in thisthesis. A thorough investigation should be conducted on how to apply maximal
completion in unfailing completion to construct more effective theorem provers.
Constrained Equalities give a framework to fully automate rewriting induction and other inductive proof methods. As mentioned in the introduction, theuser provided reduction order is only one among many obstacles in constructing
inductive proofs. Several methods have been proposed to extend rewriting induction, for example to deal with non-orientable equations [1] or to to constructneeded lemmata automatically [3, 71, 78]. It is worthwhile to investigate if andhow these techniques can be incorporated in our approach.
Last but not least, in Chapter 6 we presented a generalization of Knuth andBendix’ confluence criterion, which can deal with non-left-linear, non-terminating
TRSs and can be fully automated. As seen in Section 6.5, conditions requiredin our criterion are related to the results by Jouannaud and Kirchner [44] andGeser [27]. Both exploit relative termination to overcome the problem of nontermination, however still relative termination poses a strict restriction. In thecase of left-linear TRSs, Hirokawa and Middeldorp employed critical pair steps [38]to relax this restriction. The resulting criterion generalizes both Knuth-Bendix’
criterion and orthogonality (left-linearity and non-overlappingness). We anticipate that this and our result can be combined by using such critical pair steps.
However deriving such a combined criterion is tightly related to the long-standing
open conjecture that every strongly non-overlapping, right-linear TRS is confluent.1
In our approach we separate a TRS into two parts and use local properties
such as confluence of the S -part and relative termination. To separate these parts
we employ strong non-overlappingness. In the absence of such local properties
direct criteria weaken the notion of strong non-overlappingness — as SNO(R, R)
is too restrictive — to non-ω-overlappingness [57], non-E-overlappingness [32] orpersistence [82]. It is interesting to investigate whether such weakening is also
possible in our scenario.

1 The RTA Open Problem #58: http://rtaloop.mancoosi.univ-paris-diderot.fr/

96

Appendix A
Experimental Data for Chapter 4
Table A.1 contains the list of all experimental results. Here × denotes failure,i.e. no more rules are orientable, no new critical pairs can be generated and thetool gives up. The symbol ∞ denotes that the tool in question did not provide a
result within 600 seconds.
Table A.1: Experimental results for Maxcomp
LPO
problem

mkbTT

KBO

MaxcompmkbTT

termination tool

MaxcompmkbTT

Slothrop

AD93.Z22

∞

∞

∞

∞

∞

∞

ASK.93.1

0.01

0.10

0.02

0.01

0.01

0.98

ASK.93.2
ASK.93.5

∞
∞

∞
∞

∞
∞

∞
∞

∞
∞

∞
∞

ASK.93.6

16.75

1.06

10.93

0.83

5.73

10.81

aufgabe3.2

0.01

0.00

0.01

0.01

0.01

0.95

aufgabe3.3

0.01

0.01

0.01

0.01

0.01

0.87

BD94.collapse 0.05

0.01

0.08

0.01

0.03

1.18

BD94.peano

0.03

0.01

∞

∞

0.02

1.22

BD94.sqrt

0.02

0.00

0.03

0.01

0.02

1.00

BGK94.D08

0.70

37.48

∞
∞
∞
∞

∞
∞
∞
∞

∞

BGK94.D16

∞
∞
∞
∞

74.91

∞
∞
∞
∞

BGK94.M08

0.74

0.24

1.25

0.49

0.59

7.72

BGK94.M10

1.20

0.81

2.24

0.94

20.97

BGK94.M12

1.83

41.69

3.65

1.42

27.18

BGK94.M14

2.73

∞
∞
∞
∞

2.06

25.88

∞

∞

BGK94.D10
BGK94.D12

BGK94.Z22W

0.88
1.18

∞
5.73
∞
∞
∞
continued on next page

51.49
52.44

97

Appendix A: Experimental Data for Chapter 4
continued from previous page
LPO
problemtermination tool

mkbTT

MaxcompmkbTT

Maxcomp

BH96.fac8

0.11

0.02

0.52

0.06

0.07

2.07

Chr89.A2

4.21

0.99

4.81

0.95

95.76

182.93mkbTT

Slothrop

Chr89.A24∞∞∞

Chr89.A3

40.06

3.17

20.85

∞
∞

∞
∞

∞
∞

fggx

0.01

0.01

0.02

0.01

0.01

0.98

fib

0.87

100.32

∞
∞
∞
×
×

7.18

∞
∞
×
×

∞
∞
∞
×
×

0.85

∞
∞
×
×

∞
∞
×
×

∞
∞
×
×

KK99.linear_assoc 0.02

0.01

0.02

0.01

0.03

0.83

Les83.fib

0.10

0.01
0.01

∞
∞

2.82

0.22

∞
∞

0.23

Les83.subset

0.09

3.27

lr.theory

0.35

0.11

0.45

2.89

1.74

7.90

LS06.CGE4
LS06.CGE5

∞
∞

∞
∞

∞
∞

∞
∞

∞
∞

∞
∞

LS94.G0

0.52

0.05

0.71

0.06

1.28

5.90

LS94.G1

LS94.P1

∞
∞
∞
∞

∞
∞
∞
∞

∞
∞
∞
∞

0.78

46.15

∞
∞
∞
∞
∞

∞
∞
∞
∞

OKW95.dt1

0.91

6.22

rl.theory
Sim91_sims2

2.36

0.17

1.21

1.76

8.07

∞

∞

∞
∞
∞
∞
∞
∞
∞

∞

∞

∞

SK90.3.01

1.20

0.09

2.23

0.61

4.16

18.85

SK90.3.02

0.03

0.01

0.03

0.02

0.05

0.97

SK90.3.03

4.69

1.01

3.88

0.05

1.59

5.54

SK90.3.04

6.72

1.75

∞

∞

99.98

SK90.3.05

1.58

0.35

1.07

0.33

3.46

SK90.3.06

4.22

0.90

SK90.3.07

∞

3.03

∞
∞

∞
∞

∞
∞

∞
∞
∞
∞

SK90.3.08

0.08

0.01

0.06

0.03

0.05

1.18

HR94.1
HR94.2
kb.fail
kb.fail1

LS94.G2
LS94.G3

98

KBO

SK90.3.09

∞

∞

∞

∞

∞

∞

SK90.3.10

0.03

0.01

0.03

0.01

0.02

0.92

SK90.3.11

0.03

0.01

0.03

0.01

0.02

1.02

SK90.3.12

×

×

×

×

×

×

SK90.3.13

0.17

0.02

0.16

0.02

0.17

1.33

SK90.3.14

0.13

0.01

0.21

0.16

0.15

1.65

SK90.3.15

∞

∞
0.12
continued on next page

0.02

0.08

1.39

continued from previous page
LPO
problemKBO

termination tool

mkbTT

MaxcompmkbTT

MaxcompmkbTT

Slothrop

SK90.3.16

0.02

0.01

0.03

0.01

0.01

0.80

SK90.3.17

0.05

0.01

0.04

0.01

0.08

1.25

SK90.3.18

0.15

0.01

∞

∞

0.30

3.50

SK90.3.19

0.15

0.09

0.26

15.11

0.32

2.73

SK90.3.20

0.35

1.34

0.42

∞

0.46

2.65

SK90.3.21

0.16

0.04

0.25

0.03

0.19

85.81

SK90.3.22

∞

4.03

∞

8.03

∞

∞

SK90.3.23

0.03

96.93

0.43

0.19

0.37

4.72

SK90.3.24

0.04

0.02

0.04

0.01

0.04

1.26

SK90.3.25

0.02

0.43

0.02

0.01

0.03

0.99

SK90.3.26

∞

∞

∞

∞

∞

SK90.3.27

13.31

21.09

36.47

0.53

72.31

∞
∞

SK90.3.28

∞

20.23

53.58

∞

∞

110.76

SK90.3.29

2.29

0.86

3.91

1.75

2.02

5.27

SK90.3.30

0.03

0.01

0.03

0.02

0.02

0.76

SK90.3.31

0.03

0.01

0.04

0.01

0.01

0.84

SK90.3.32

0.01

0.01

0.01

0.01

0.01

0.74

SK90.3.33

0.03

0.01

0.02

0.01

0.02

0.91

sl.ackermann

0.02

0.01

∞
∞
∞

0.68

∞
∞

173.03

∞

∞
∞

0.62

0.38

3.88

7.60

×
×

∞
∞
∞
∞
∞
∞

0.03

∞
∞
∞
×
×

∞
∞

2.52

262.32

2.81

∞

0.01

0.01

0.01

0.01

0.01

0.73

sl.cgesl.cge3
sl.endosl.equiv.proofs
sl.equiv.proofs.or
sl.fghsl.groups

0.45

0.08

∞

0.08

0.54

2.22

sl.groups_conj

0.11

0.02

0.18

1.10

0.21

2.49

sl.hard

0.01

0.01

0.01

0.02

0.01

0.69

slothrop.nlp-2b

∞

∞

∞

∞

∞

∞

TPDB.torpa.secr10

2.21

0.17

14.34

0.55

9.15

50.46

TPDB.torpa.secr4

4.77

35.69

15.25

31.62

17.10

35.56

TPDB.thiemann27

∞
∞

∞

∞

∞

∞

∞

0.73

5.76

42.63

15.27

203.69TPTP.BOO027-1

0.04

0.02

0.04

0.01

0.03

1.37

TPTP.COL053-1

0.01

0.01

0.01

0.01

0.01

0.67

TPTP.COL056-1

0.04

0.01

0.03

0.87

0.03

0.82

TPDB.zantema.z115

TPTP.COL060-1

×

×

0.01

0.01

0.02

1.14

TPTP.COL085-1

0.01

0.01

0.01

0.01

0.01

0.66

TPTP.GRP010-4

1.52

0.27

2.21

0.11

6.02

231.47

continued on next page99

Appendix A: Experimental Data for Chapter 4
continued from previous page
LPO
problemKBO

termination tool

mkbTT

MaxcompmkbTT

MaxcompmkbTT

Slothrop

TPTP.GRP011-4

0.48

0.09

0.62

0.10

0.63

25.42

TPTP.GRP012-4

0.28

0.03

0.34

0.03

0.48

2.13

TPTP.GRP393-2

0.01

0.01

0.01

0.01

0.01

0.68

TPTP.GRP394-3

0.33

0.06

0.42

0.07

0.51

2.68

TPTP.GRP454-1

17.13

2.65

49.63

0.14

109.87

TPTP.GRP457-1

17.18

2.66

49.98

1.62

112.73

TPTP.GRP460-1

0.89

17.74

2.91

16.99

1.76

17.80

3.26

16.91

2.40

57.20

1.00

∞
∞
∞

0.84

168.93

13.21

5.13

40.54

2.83

TPTP.GRP496-1

∞
∞
∞
∞
∞
∞
∞
∞

∞
∞
∞
∞

0.90

∞

11.13

∞
∞
∞
∞
∞
∞

241.10TPTP.HWC004-1

0.13

0.03

0.09

0.01

0.14

1.32

TPTP.HWC004-2

0.05

0.01

0.04

0.01

0.03

1.09

TPTP.SWV262-2

0.03

0.02

0.03

0.05

0.03

0.88

∞

∞

∞

∞

162.66∞

TPTP.GRP463-1
TPTP.GRP481-1
TPTP.GRP484-1
TPTP.GRP487-1
TPTP.GRP490-1
TPTP.GRP493-1

WS06.proofreduction

100

0.52

13.52
7.05

69.56

∞
×
∞
∞

Appendix B
Experimental Data for Chapter 5
Table B.2 contains the list of all experimental results of completion based on constrained equalities, and Table B.1 contains all data for rewriting induction basedon constrained equalities. Here × denotes failure, i.e. that no more rules are orientable, no new critical pairs or expansions can be generated and the tool gives
up. For rewriting induction with constrained equalities we do not provide precise timing information, instead Y denotes a successful proof. For completion thesymbol ∞ denotes a timeout. The time limit was set to 60 seconds for completionand to 10 seconds for the inductive proofs.
Table B.1: Experimental results for Induction with Constraint Equalities
problem

LPO

KBO

problem

LPO

KBO

DC #2

Y

Y

DC #3

∞

∞

DC #4

∞

∞

DC #5

Y

Y

DC #7

Y

Y

DC #22

YY

DC #23

YY

DC #25

DC #27

DC #28

DC #58Y

DC #63

∞
∞
∞
∞
∞
∞
∞

∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞

∞
∞
∞
∞

DC #47∞∞∞∞

DC #84

∞
∞
∞
∞
∞
∞
∞
∞
∞
∞

DC #110Y

Y

DC #112Y

Y

DC #115

YY

DC #29
DC #31

DC #79DC #81DC #83
DC #109
DC #111
DC #113

DC #30DC #43
DC #55
DC #60DC #64
DC #80DC #82

Y

∞
∞
∞
∞
∞

continued on next page101

Appendix B: Experimental Data for Chapter 5
continued from previous pageproblem

LPO

KBO

problem

LPO

KBO

DC #116∞
Y∞∞

DC #158

DC #208

DC #216∞∞∞∞

DC #225

Y

Y

DC #228

Y

Y

DC #229

Y

Y

DC #230

YY

DC #231

Y

DC #232∞

DC #233

DC #234

Y

DC #237∞∞∞∞

DC #270

∞
∞
∞

∞
∞
∞
∞

DC #281

Y

Y

DC #283

Y

Y

DC #287

Y

Y

DC #300

∞

Y

Y

Y

DC #318∞

DC #319

DC #349

Y

DC #370∞∞

DC #442

Y

∞
∞
∞
∞
∞

DC #301

DC #305

DC #665

Y

Y

DC #694

∞

∞
∞
∞
∞
∞

DC #699

Y∞

DC #704

YY

DC #744

Y

Y

DC #1003

Y

Y

DC #1018

Y

Y

DC #1052∞

DC #1107

∞
∞
∞

Y

mul

Y

∞
∞

sato1

Y

∞
∞
∞

DC #236

mul2
sato2

DC #375∞

DC #502

Y

Table B.2: Experimental results for Completion with Constraint Equalities
problem

LPO

KBO

problem

LPO

KBO

AD93.Z22∞∞∞

ASK.93.1

0.26

ASK.93.5∞∞∞

ASK.93.6∞∞∞

aufgabe3.2

0.01

0.01

aufgabe3.3

0.01

0.01

BD94.collapse

0.05

0.02

BD94.peano

0.01

0.01

0.01

∞
∞
∞
∞
∞
∞

∞
∞
∞
∞
∞
∞

BD94.sqrt

BGK94.D08

BGK94.D10

BGK94.M14

∞
∞
∞
∞

∞
∞
∞
∞

BH96.fac8

0.03

0.03

2.38

Chr89.A24∞∞

ASK.93.2

BGK94.D12
BGK94.M08
BGK94.M12
BGK94.Z22W
Chr89.A2

BGK94.D16
BGK94.M10

continued on next page102

continued from previous pageproblem

LPO

KBO

problem

LPO

KBO

Chr89.A3

0.01

0.02

HR94.1∞
×∞×

KK99.linear_assoc

0.01

0.01

Les83.fib

0.03

Les83.subset

0.01

lr.theory

10.04

LS06.CGE5

OKW95.dt1
Sim91_sims2

∞
∞
∞
∞
∞

SK90.3.02

0.01

∞
∞
∞
∞
∞
∞
∞
∞

SK90.3.04
SK90.3.06

∞
∞

∞
∞
∞
×
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞

fggx

kb.fail1∞∞∞
×SK90.3.08

0.03

0.07

SK90.3.10

0.01

0.01

SK90.3.12

×SK90.3.14

0.11

SK90.3.16
SK90.3.18
SK90.3.20

fibHR94.2

LS94.G1
LS94.G3

kb.fail

LS94.P1∞∞∞∞

rl.theory

1.22

SK90.3.01

1.03

SK90.3.03

4.69

SK90.3.05

3.13

SK90.3.09∞∞∞

SK90.3.11

0.07

0.08

×
∞

SK90.3.13

0.05

0.03

SK90.3.15

∞

0.06

0.01

0.01

SK90.3.17

0.01

∞

0.01

SK90.3.19

0.27

∞
∞

0.64

∞

SK90.3.21

4.50

0.08

LS06.CGE4
LS94.G0
LS94.G2

SK90.3.07∞∞

SK90.3.22∞

4.03

SK90.3.23

35.67

∞

SK90.3.24

0.06

0.04

SK90.3.25

0.18

0.01

SK90.3.26∞∞∞

SK90.3.27∞

SK90.3.28

30.88

SK90.3.29

0.03

∞
∞

SK90.3.30

0.03

0.03

SK90.3.31

0.02

0.01

SK90.3.32

0.01

0.01

SK90.3.33

0.01

0.01

sl.ackermann

0.01

∞
×

∞
∞
×

∞
∞
×

sl.fgh0.01

0.03

sl.groups

0.46

sl.groups_conj

0.08

0.08

sl.hard

0.01

∞
∞
×
∞
∞

slothrop.nlp-2b

∞
∞
∞

∞
∞
∞

TPTP.BOO027-1

0.01

0.02

TPTP.COL053-1

0.01

0.01

TPTP.COL056-1

0.01

0.01

TPTP.COL060-1

×
∞

0.01

TPTP.COL085-1

0.01

0.01

TPTP.GRP010-4∞

TPTP.GRP011-4

1.63

∞

TPTP.GRP012-4

0.10

0.10

TPTP.GRP393-2

0.01

0.01

sl.cge3
sl.equiv.proofs

TPDB.torpa.secr4
TPDB.zantema.z115

sl.cgesl.endosl.equiv.proofs.or

TPDB.torpa.secr10
TPDB.thiemann27

∞
∞

17.39

∞

continued on next page103

Appendix B: Experimental Data for Chapter 5
continued from previous pageproblem

LPO

KBO

TPTP.GRP394-3

0.29

TPTP.GRP496-1

∞
∞
∞
∞
∞

∞
∞
∞
∞
∞
∞

TPTP.GRP454-1

TPTP.GRP457-1

TPTP.HWC004-2

0.01

0.01

∞

∞

TPTP.GRP463-1
TPTP.GRP484-1
TPTP.GRP490-1

WS06.proofreduction

104

problem

LPO

KBO

TPTP.GRP493-1

∞
∞
∞
∞
∞

∞
∞
∞
∞
∞

TPTP.HWC004-1

0.01

0.01

TPTP.SWV262-2

0.03

∞

TPTP.GRP460-1
TPTP.GRP481-1
TPTP.GRP487-1

Appendix C
Experimental Data for Chapter 6
Table C.1: Experimental results for the new confluence criterion
ACP∗

CSI

CSI∗

Saigawa

Saigawa∗

Example 6.1.7 ?(0.07)

Y(0.49)?(6.32)Y(13.62)?(0.19)Y(0.55)

Example 6.1.8 ?(0.07)

Y(0.43)?(1.81)Y(10.77)?(0.19)Y(0.61)

Example 6.1.9 ?(0.07)

Y(1.03)?(6.32)Y(20.19)?(0.25)Y(1.15)

Cops #1

Y(0.19)Y(0.67)Y(0.67)Y(1.11)?(0.31)?(2.29)Cops #2

Y(0.07)Y(0.07)Y(0.67)Y(2.04)?(0.19)?(5.55)

Cops #3

Y(0.19)Y(0.13)Y(0.79)Y(2.05)?(0.25)?(4.77)

Cops #15

N(0.43)N(0.43)∞∞?(0.19)?(0.19)Cops #16?(0.13)?(2.78)?(2.96)?(12.40)?(0.19)?(2.89)Cops #17

Y(0.19)Y(0.07)?(6.39)?(39.52)?(0.19)?(13.72)

Cops #24?(0.07)?(3.44)?(6.33)?(14.94)?(0.19)?(3.56)

Cops #25

Y(0.07)Y(0.67)?(0.67)Y(1.11)?(0.19)Y(0.85)

Cops #26?(0.07)?(3.44)?(6.29)?(14.82)?(0.19)?(3.57)

Cops #27?(0.07)?(1.71)?(2.66)?(25.45)?(0.19)?(2.24)

Cops #28?(0.07)Y(0.79)?(6.33)Y(11.96)?(0.19)Y(0.91)

Cops #46

N(0.07)N(0.07)N(0.37)N(1.33)?(0.19)N(0.61)

Cops #47?(0.07)?(3.44)?(6.33)?(16.17)?(0.19)Y(3.62)

Cops #53

Y(0.25)Y(0.13)Y(0.43)Y(1.72)?(0.31)?(6.51)

Cops #55

Y(0.31)Y(0.13)Y(0.43)Y(1.74)?(0.31)?(5.43)

Cops #59?(0.13)Y(0.49)?(1.82)Y(7.75)?(0.19)Y(0.61)

Cops #70?(0.13)N(0.85)?(0.31)N(1.24)?(0.19)N(0.97)

Cops #76?(0.13)?(0.73)?(0.91)?(0.37)?(13.32)?(0.19)?(13.43)

Cops #78?(0.37)?(2.90)∞∞∞?(0.19)Cops #77∞∞∞?(0.19)?(2.84)

Cops #79

Y(0.07)Y(0.07)?(6.32)?(21.41)?(0.19)?(3.62)

Cops #89

Y(0.07)Y(0.07)?(6.35)?(35.35)?(0.19)?(2.24)problem

ACP

continued on next page105

Appendix C: Experimental Data for Chapter 6
continued from previous page

106

ACP∗

CSI

CSI∗

Saigawa

Saigawa∗?(0.07)Y(1.16)?(6.32)Y(20.05)?(0.19)Y(1.28)

Cops #94

Y(0.13)Y(0.13)Y(4.52)Y(7.01)?(0.19)Y(31.82)

Cops #97

Y(0.07)Y(0.07)Y(0.67)Y(4.05)?(0.19)Y(0.73)

Cops #98

problem

ACP

Cops #91

N(0.07)N(0.07)N(0.37)N(3.38)?(0.19)?(1.16)

Cops #107 ?(0.07)

Y(0.49)?(1.95)Y(2.42)?(0.19)Y(0.61)

Cops #108 Y(0.13)

Y(0.07)?(6.33)?(11.08)?(0.49)?(5.01)

Cops #109 ?(0.43)?(2.96)∞∞?(0.19)?(2.77)

Appendix D
Maxcomp: Installation and Usage
Maxcomp is a fully automatic completion tool for equational systems for Linux
based operating systems, written in the OCaml programming language. In thissection we briefly describe its set-up and usage.

Installation
The source code of Maxcomp is available on-line at
http://www.jaist.ac.jp/project/maxcomp
Maxcomp builds heavily on the works of others. Unfortunately, this makes

compilation and installation slightly tedious since several software packages areneeded to compile the source code. Some (OCaml, GNU make, Findlib, CamlIDL, GMP) might be available through the package system of your distribution.
Below, version numbers refer to those versions of the packages which were usedduring the development of Maxcomp. Later versions might work, but backwardcompatibility is not guaranteed. The packages are:
• Objective CAML (OCaml) 3.12, available at
http://www.caml.inria.fr• The GNU make tool 3.18, available at
http://www.gnu.org/s/make• OCaml Findlib 1.2.7, available at
http://projects.camlcity.org/projects/findlib.html• Ocamlyices 7bd6030, available athttps://github.com/polazarus/ocamlyices

OCaml Findlib should be installed before installing Ocamlyices. Moreover
after installing Findlib, the following packages, which are needed for Ocamlyices,
have to be installed. They should be installed in the following order:

107

Appendix D: Maxcomp: Installation and Usage
1. CamlIDL 1.05.13, available at
http://forge.ocamlcore.org/projects/camlidl

2. The GNU Multiple Precision Arithmetic Library (GMP) 2.5.1, available at
http://gmplib.org

This is only needed if you do not install Yices with statically linked GMP
libraries. It is recommended however to install Yices with non-staticallylinked GMP libraries.
3. Yices 1.0.29, available at
http://yices.csl.sri.com

After installation of all these packages and Ocamlyices, extract the contents of
the archive of Maxcomp into a folder:tar xzvf maxcomp-1.0.1.tar.gz

Switch to the newly generated directory, and execute makecd maxcomp-1.0.1
maketo compile and generate the Maxcomp binary.

Usage
The general usage of Maxcomp is
maxcomp <options> <file>If successful, it will output a line YES followed by the found complete TRS. Available input options are:• -lpo (default)
this option encodes constraints based on lexicographic path orders (LPO) tofind maximal terminating TRSs
• -mpothis option encodes constraints based on multiset path orders (MPO) to findmaximal terminating TRSs
• -kbothis option encodes constraints based on Knuth-Bendix orders (KBO) to findmaximal terminating TRSs

108

• -mi <d,n>this option encodes constraints based on d ∗ d matrix interpretations withcoefficients ≤ n• -K <n>this option enforces to initially compute n − 1 maximal terminating TRSs.
If omitted, the default value is set to 2, i.e. only one maximal terminating
TRS is computed
Only one of the options -lpo, -mpo, -kbo and -mi <d,n> can be activated at a time.
If multiple of those options are specified, all but the last one are ignored. We givesome examples:
maxcomp filename.es

tries to complete the equational system specified in filename.es by encoding constraints based on lexicographic path orders with parameter K initially set to 2.
maxcomp -kbo -mi 2 2 -K 4 filename.es

tries to complete the equational system specified in filename.es by encoding constraints based on 2 ∗ 2 matrix interpretations with coefficients ≤ 2, and parameter
K initially set to 4. Note that the option -kbo is ignored and could be simply omitted.
As input, Maxcomp accepts the TPDB1 plain text file format. To give some
intuition, consider the specification of group-theory, sl_groups.trs:(VAR x y z )(RULESf(x,f(y,z)) ->f(x,i(x)) -> ef(x,e) -> x)f(f(x,y),z)

Roughly, the first line lists all variables in the subsequent rules. The TPDB
format was intended to to specify term rewriting systems, and not equational
systems, but due to its popularity, it is used as the input format of Maxcomp.
Intended for TRSs, a direction -> is indicated between terms. Maxcomp however ignores this direction and treats the specified rules as equations. Therefore
writing e.g.
e -> f(x,i(x))

instead of f(x,i(x)) -> e is still valid input and specifies the same equational
system, even though it violates the variable condition of TRSs when interpreted
as a rule.
1 http://www.lri.fr/~marche/tpdb/format.html

109References[1] Takahito Aoto. Dealing with non-orientable equations in rewriting induction. In Proc. of the 17th International Conference on Rewriting Techniques andApplications, volume 4098 of Lecture Notes in Computer Science, pages 242–256,
2006.
[2] Takahito Aoto. Designing a rewriting induction prover with an increased
capability of non-orientable theorems. In Proc. of the Austrian-Japanese Workshop on Symbolic Computation in Software Science, RISC Technical Report 08-08,
pages 1–15, 2008.
[3] Takahito Aoto. Sound lemma generation for proving inductive validity ofequations. In Proc. of the IARCS Annual Conference on Foundations of Software
Technology and Theoretical Computer Science, volume 2 of Leipzig International
Proceedings in Computer Science, pages 13–24, 2008.
[4] Takahito Aoto, Nao Hirokawa, Dominik Klein, and Sarah Winkler. Constrained equalities. In preparation. 2012.
[5] Takahito Aoto and Yoshihito Toyama. Persistency of confluence. Journal of
Universal Computer Science, 3(11):1134–147, 1997.
[6] Takahito Aoto and Yoshihito Toyama. A reduction-preserving completionfor proving confluence of non-terminating term rewriting systems. Logical
Methods in Computer Science, 8(1-31):1–29, 2012.
[7] Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama. Proving confluenceof term rewriting systems automatically. In Proc. of the 21st International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer
Science, pages 93–102, 2009.
[8] Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1-2):133–178, 2000.
[9] Jürgen Avenhaus. Reduktionssysteme. Rechnen und Schließen in gleichungsdefinierten Strukturen. Springer, 1995.
[10] Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge
University Press, 1998.

111

References[11] Leo Bachmair and Nachum Dershowitz. Equational inference, canonicalproofs, and proof orderings. Journal of the ACM, 41(2):236–276, 1994.
[12] Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational proofs. In Proc. of the ACM/IEEE Symposium on Logic in Computer Science, pages 346–357, 1986.
[13] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu.
Symbolic model checking without BDDs. In Proc. of the 5th International
Conference on Tools and Algorithms for Construction and Analysis of Systems,
volume 1579 of Lecture Notes in Computer Science, pages 193–207, 1999.
[14] Garrett Birkhoff. On the structure of abstract algebras. Proceedings of theCambridge Philosophical Society, 31(4):433–454, 1935.
[15] Alan Bundy. The automation of proof by mathematical induction. In
John Alan Robinson and Andrei Voronkov, editors, Handbook of AutomatedReasoning, pages 845–911. Elsevier and MIT Press, 2001.
[16] Alonzo Church and John B. Rosser. Some properties of conversion. Transaction of the American Mathematical Society, 39:472–482, 1936.
[17] Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. Solving partial orderconstraints for LPO termination. JSAT, 5(1–4):193–215, 2008.
[18] Hubert Comon. Inductionless induction. In John Alan Robinson and Andrei
Voronkov, editors, Handbook of Automated Reasoning, pages 913–962. Elsevier
and MIT Press, 2001.
[19] Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
[20] Nachum Dershowitz. A note on simplification orderings. Information Processing Letters, 9(5):212–215, 1979.
[21] Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.
[22] Bruno Dutertre and Leonardo De Moura. A fast linear-arithmetic solver
for DPLL(T). In Proc. of the 18th International Conference on Computer Aided
Verification, volume 4144 of Lecture Notes in Computer Science, pages 81–94,
2006.
[23] Jörg Endrullis, Johannes Waldmann, and Hans Zantema. Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning, 40(2-3):195–220, 2008.

112

References[24] Michael J. Fay. First-order unification in an equational theory. In Proc. of the
4th Workshop on Automated Deduction, pages 161–167, 1979.
[25] Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp. Layer systems
for proving confluence. In Proc. of the 31st International Conference on Foundations of Software Technology and Theoretical Computer Science, volume 13 ofLeipzig International Proceedings in Computer Science, pages 288–299, 2011.
[26] Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René
Thiemann, and Harald Zankl. SAT solving for termination analysis withpolynomial interpretations. In Proc. of the 10th International Conference on
Theory and Applications of Satisfiability Testing, volume 4501 of Lecture Notes in
Computer Science, pages 340–354, 2007.
[27] Alfons Geser. Relative Termination. PhD thesis, Universität Passau, 1990.
Available as technical report 91-03.
[28] Jürgen Giesl, Peter Schneider-Kamp, and René Thiemann. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In Proc. ofthe 3rd International Joint Conference on Automated Reasoning, volume 4130 ofLecture Notes in Artificial Intelligence, pages 281–286, 2006.
[29] Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. Proving and disproving termination of higher-order functions. In Proc. of the 5th International
Symposium on Frontiers of Combining Systems, volume 3717 of Lecture Notes in
Artificial Intelligence, pages 216–231, 2005.
[30] Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke.
Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3):155–203, 2006.
[31] Hiroshi Gomi, Michio Oyamaguchi, and Yoshikatsu Ohta. On the ChurchRosser property of non-E-overlapping and strongly depth-preserving term
rewriting systems. Trans. IPSJ, 37(12):2147–2160, 1996.
[32] Hiroshi Gomi, Michio Oyamaguchi, and Yoshikatsu Ohta. On the ChurchRosser property of non-E-overlapping and weight-preserving TRS’s. Technical Report 950, RIMS Research Report, 1996.
[33] Hiroshi Gomi, Michio Oyamaguchi, and Yoshikatsu Ohta. On the ChurchRosser property of root-E-overlapping and strongly depth-preserving term
rewriting systems. Trans. IPSJ, 39(4):992–1005, 1998.
[34] Bernhard Gramlich. Completion based inductive theorem proving: An abstract framework and its applications. In Proc. of the 9th European Conferenceon Artificial Intelligence, pages 314–319. Pitman Publishing, London, 1990.

113

References[35] Bernhard Gramlich. Confluence without termination via parallel criticalpairs. In Proc. of the 21st International Colloquium, Linköping Trees in Algebra and Programming, volume 1059 of Lecture Notes in Computer Science, pages
211–225, 1996.
[36] Bernhard Gramlich. Strategic issues, problems and challenges in inductive
theorem proving. In Proc. of the 5th International Workshop on Strategies inAutomated Deduction, volume 125 of Electronic Notes in Theoretical Computer
Science, pages 5–43, 2005.
[37] Nao Hirokawa and Aart Middeldorp. Automating the dependency pairmethod. Information and Computation, 199(1-2):172–199, 2005.
[38] Nao Hirokawa and Aart Middeldorp. Decreasing diagrams and relative
termination. Journal of Automated Reasoning, 47:481–501, 2011.
[39] Gerald Huet. Confluent reductions: Abstract properties and applications toterm rewriting systems. Journal of the ACM, 27:797–821, 1980.
[40] Gerald Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 21(1):11–21, 1981.
[41] Gérard Huet and Dallas Lankford. On the uniform halting problem for term
rewriting systems. Technical Report 283, INRIA, 1981.
[42] Jean-Marie Hullot. Canonical forms and unification. In Proc. of the 5th International Conference on Automated Deduction, volume 87 of Lecture Notes in
Computer Science, pages 318–334, 1980.
[43] Jean-Pierre Jouannaud. Confluent and coherent equational term rewriting
systems: Application to proofs in abstract data types. In Proc. of the 8thInternational Colloquium on Trees in Algebra and Programming, volume 159 ofLecture Notes in Computer Science, pages 269–283, 1983.
[44] Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules
modulo a set of equations. SIAM Journal on Computing, 15(4):1155–1194,
1986.
[45] Sam Kamin and Jean J. Lévy. Two generalizations of the recursive pathordering. Unpublished manuscript, University of Illinois, 1980.
[46] Dominik Klein and Nao Hirokawa. Maximal completion. In Proc. of the 22ndInternational Conference on Rewriting Techniques and Applications, volume 10 ofLeipzig International Proceedings in Computer Science, pages 71–80, 2011.

114

References[47] Dominik Klein and Nao Hirokawa. Confluence of non-left-linear TRSs via
relative termination. In Proc. of the 18th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning, volume 7180 of Lecture Notes
in Computer Science, pages 258–273, 2012.
[48] Jan W. Klop. Combinatory reduction systems. PhD thesis, Utrecht University,
1980.
[49] Donald E. Knuth and Peter Bendix. Simple word problems in universal
algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages
263–297. Pergamon Press, 1970.
[50] Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In Proc. of the 20th International Conference on
Rewriting Techniques and Applications, volume 5595 of Lecture Notes in Computer Science, pages 295–304, 2009.
[51] Masahito Kurihara and Hisashi Kondo. Completion for multiple reduction
orderings. Journal of Automated Reasoning, 23(1):25–42, 1999.
[52] Masahito Kurihara and Hisashi Kondo. Efficient BDD encodings for partial
order constraints with application to expert systems in software verification.
In Proc. of the 17th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, volume 3029 of Lecture
Notes in Artificial Intelligence, pages 827–837, 2004.
[53] Bernd Löchner and Thomas Hillenbrand. A phytography of Waldmeister.
AI Communications, 15(2–3):127–133, 2002.
[54] Yves Métivier. About the rewriting systems produced by the Knuth-Bendix
completion algorithm. Information Processing Letters, 16(1):31–34, 1983.
[55] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML, Revised Edition. MIT Press, 1997.
[56] Maxwell H.A. Newman. On theories with a combinatorial definition of“equivalence”. Annals of Mathematics, 43(2):223–243, 1942.
[57] Mizuhito Ogawa. Chew’s theorem revisited - uniquely normalizing property of nonlinear term rewriting systems-. In Proc. of the 3rd International
Symposium on Algorithms and Computation, volume 650 of Lecture Notes in
Computer Science, pages 309–318, 1992.
[58] Enno Ohlebusch. Modular Properties of Composable Term Rewriting Systems.
PhD thesis, Universität Bielefeld, 1994.

115

References[59] Enno Ohlebusch. Modular properties of composable term rewriting systems.
Journal of Symbolic Computation, 20:1–41, 1995.
[60] Enno Ohlebusch. Advanced topics in term rewriting. Springer, 2002.
[61] Simon Peyton Jones et al. The Haskell 98 language and libraries: The revised
report. Journal of Functional Programming, 13(1):0–255, Jan 2003.
[62] Uday S. Reddy. Term rewriting induction. In Proc. of the 10th International
Conference on Automated Deduction, volume 449 of Lecture Notes in Computer
Science, pages 162–177, 1990.
[63] John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.
[64] Barry K. Rosen. Tree-manipulating systems and Church-Rosser theorems.
Journal of the ACM, 20(1):160–187, 1973.
[65] Masahiko Sakai and Mizuhito Ogawa. Weakly-non-overlapping noncollapsing shallow term rewriting systems are confluent. Information Processing Letters, 110(18–19):810–814, 2010.
[66] Haruhiko Sato and Masahito Kurihara. Multi-context rewriting induction
with termination checkers. IEICE Transactions, 93-D(5):942–952, 2010.
[67] Haruhiko Sato, Masahito Kurihara, Sarah Winkler, and Aart Middeldorp.
Constraint-based multi-completion procedures for term rewriting systems.
IEICE Transactions, 92-D(2):220–234, 2009.
[68] Haruhiko Sato, Sarah Winkler, Masahito Kurihara, and Aart Middeldorp.
Multi-completion with termination tools (system description). In Proc. of
the 4th International Joint Conference on Automated Reasoning, Lecture Notes in
Computer Science, pages 306–312, 2008.
[69] Andrea Sattler-Klein. About changing the ordering during Knuth-Bendix
completion. In Proc. of the 11th Annual Symposium on Theoretical Aspects ofComputer Science, volume 775 of Lecture Notes in Computer Science, pages 175–
186, 1994.
[70] Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish, andJürgen Giesl. Proving termination using recursive path orders and SAT solving. In Proc. of the 6th International Symposium Frontiers of Combining Systems,
volume 4720 of Lecture Notes in Computer Science, pages 267–282, 2007.
[71] Satoshi Shimazu, Takahito Aoto, and Yoshihito Toyama. Automatedlemma generation for rewriting induction with disproof. Computer Software,26(2):41–55, 2009. (in Japanese).

116

References[72] Joachim Steinbach and Ulrich Kühler. Check your ordering—termination
proofs and open problems. Technical Report SR-90-25, Universität Kaiserslautern, 1990.
[73] Aaron Stump, Garrin Kimmell, and Roba El Haj Omar. Type preservation asa confluence problem. In Proc. of the 22nd International Conference on Rewriting
Techniques and Applications, volume 10 of Leipzig International Proceedings in
Computer Science, pages 345–360, 2011.
[74] Aaron Stump and Bernd Löchner. Knuth-Bendix completion of theories ofcommuting group endomorphisms. Information Processing Letters, 98(5):195–
198, 2006.
[75] TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in TheoreticalComputer Science. Cambridge University Press, 2003.
[76] Yoshihito Toyama. On the Church-Rosser property for the direct sum ofterm rewriting systems. Journal of the ACM, 34(1):128–143, 1987.
[77] Yoshihito Toyama. Commutativity of term rewriting systems. In K. Fuchi
and L. Kott, editors, Programming of Future Generation Computers II, pages
393–407. North-Holland, 1988.
[78] Pascal Urso and Emmanuel Kounalis. Sound generalizations in mathematical induction. Theoretical Computer Science, 323(1-3):443–471, 2004.
[79] Vincent van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259–280, 1994.
[80] Vincent van Oostrom. Development closed critical pairs. In Proc. of the
2nd International Workshop on Higher-Order Algebra, Logic, and Term Rewriting,Selected Papers, volume 1074 of Lecture Notes in Computer Science, pages 185–
200, 1995.
[81] Vincent van Oostrom. Confluence by decreasing diagrams, converted. In
Proc. of the 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 306–320, 2008.
[82] Rakesh M. Verma. Unique normal forms and confluence of rewrite systems:
Persistence. In Proc. of the 14th International Joint Conference on Artificial Intelligence, volume 1, pages 362–370, 1995.
[83] Ian Wehrman, Aaron Stump, and Eric M. Westbrook. Slothrop: KnuthBendix completion with a modern termination checker. In Proc. of the 17th International Conference on Rewriting Techniques and Applications, Lecture Notes
in Computer Science, pages 287–296, 2006.

117

References[84] Sarah Winkler and Aart Middeldorp. Termination tools in ordered completion. In Proc. of the 5th International Joint Conference on Automated Reasoning,volume 6173 of Lecture Notes in Artificial Intelligence, pages 518–532, 2010.
[85] Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara.
Optimizing mkbtt (system description). In Proc. of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leipzig International Proceedings in Computer Science, pages 373–384, 2010.
[86] Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara.
Multi-completion with termination tools. Journal of Automated Reasoning, toappear.
[87] Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. CSI - A confluence tool. In Proc. of the 23th International Conference on Automated Deduction,
volume 6803 of Lecture Notes in Artificial Intelligence, pages 499–505, 2011.
[88] Harald Zankl, Nao Hirokawa, and Aart Middeldorp. KBO orientability.
Journal of Automated Reasoning, 43(2):173–201, 2009.
[89] Hans Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.

118

Index
A, 21↔, 22↔∗ , 22↔+ , 22A, 38
w, 38→∗ , 22→+ , 22→= , 22→, 21→A , 21→α , 21≈, 31≈E , 32→E , 32>mul , 24>kbo , 30>rpo , 30_, 80
p−→R , 28→R , 28
B, 29↓, 22↓A , 22→R/S , 76→1 · →2 , 21
→1 /→2 , 76
←S ∝ → , 77
p\q, 26., 25[α]A , 32ε, 25

f A , 32`i , 33|=, 32|t| x , 26ϕ, 50|t|, 26t| p , 25
B , 47
CPS , 77
C R, 63
Dom, 26
Expd, 47
E > , 63−→
E , 85F un(t), 25
NF( A), 22
N, 30
C JRK, 63
P os(t), 25
P osF (t), 26
R(C), 51, 64
RS , 81b , 52Re , 52R
b , 77
R
S(C), 51, 64
SR (C), 64
F , 25
SNO(R, S), 77
TCAP, 88
T (F , V ), 25
T, 51

119

IndexV , 25
V ar(t), 25
Abstract Rewrite System, 21
algebra, 31
arity, 25
ARS, 21
assignment
variable-, 32
Birkhoff’s theorem, 32
carrier, 32
CES, 63
Church-Rosser, 23
closurereflexive, 22
symmetric, 22transitive, 22
collapsing, 28
complete, 23
for an ES, 33
completion
Knuth-Bendix-, 38
MKBTT, 44
multi-, 41
unfailing, 89
with termination tools, 40
composition, 21, 22
confluent, 23
constant, 25
constrained equality, 63
constraint
order, 53
termination, 62
constructor symbols, 47
context, 26
critical pair, 28
S -extended-, 77
trivial-, 28
decreasing, 79
diagrams, 79

120depth-preserving
strongly, 92
domain, 26
encompassment, 38
equation, 31
equational step, 32
equivalent, 32
erasing, 28
eTRS, 76
evaluation, 32
expandable, 47
extended rewrite rule, 76
extended TRS, 76
faircompletion, 39
multi-completion, 43
F -algebra, 31
function symbols, 25
defined-, 47
ground joinable, 63
identity, 22
inductionless induction, 47
inductive theorem, 33
inductively reducible, 47
left-R, 47
instance, 27
joinability reflection, 63
ground-, 63
joinable, 22
KBO, 30
Knuth-Bendix order, 30
labeled, 21
linear, 28
left-, 28
right-, 28
locally confluent, 23
maximalIndexcompletion, 51
TRS, 51
mgu, 27
S -, 85
model of an ES E , 32
monotonic, 27
multiset, 24
extension, 24
finite, 24
non-overlapping, 28
normal form, 22of a, 22
normalizing, 22order, 23
Knuth-Bendix-, 30
partial-, 23
pre-, 23
reduction-, 27
rewrite-, 27
simplification, 29
simplification-, 29
strict-, 23
total-, 24
well-, 24
well-founded-, 24
orthogonal, 28
overlap, 28
S -, 76
persistentequations, 38
rules, 38
position, 25
basic-, 47
precedence, 29
quasi-reducible, 47
reduced TRS, 52
reduct, 22
reflection, 63

refutational complete, 89
relationinverse, 22
join, 22
relatively terminating, 76
reversible, 92
rewriterelation, 27
rules, 27
step, 28
rewrites, 22
Rewriting Induction, 48
Inference Rules, 47
root
position, 25
symbol, 25
runof completion, 38
of multi-completion, 42
signature, 25sort, 31
stable, 27
strongly
S -stable, 86
non-overlapping, 77
substitution, 26
composition of a-, 27
ground-, 27variable-, 27
subterm, 25
relation, 29
TCAP, 88
term, 25
basic-, 47
ground-, 26
instance of a-, 27
linear-, 26
size of a-, 26
terminating, 22
TRS, 27121

Indexunifiable
syntactically, 27
unification problem
S -, 85
in solved form, 85
unifier, 27
S -, 85
uniquely normalizing, 22
universe, 32
variable, 25
variable renaming, 27
variant of a rule, 28
weakly Church-Rosser, 23
weight function, 30
weight-preserving
strongly, 92
well-founded, 23

122

Publications
in peer-reviewed international journals and conferences(i) Dominik Klein and Nao Hirokawa: “Confluence of Non-Left-Linear TRSs
via Relative Termination”. Proceedings of the 18th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning, volume 7180 ofLecture Notes in Computer Science, pages 258–273, 2012.
(ii) Dominik Klein and Nao Hirokawa: “Maximal Completion”. Proceedings ofthe 22nd International Conference on Rewriting Techniques and Applications, volume 10 of Leipzig International Proceedings in Informatics, pages 71-80, 2011.
(iii) Dominik Klein, Frank G. Radmacher and Wolfgang Thomas: “Moving in a
network under random failures: A complexity analysis”. Science of Computer
Programming, Article In Press.
(iv) Dominik Klein, Frank G. Radmacher and Wolfgang Thomas: “The Complexity of Reachability in Randomized Sabotage Games”. Fundamentals of
Software Engineering, Revised Selected Papers, volume 5961 of Lecture Notes in
Computer Science, pages 162-177, 2009.
in domestic proceedings(v) Dominik Klein: “Solving Randomised Sabotage Games for Navigation in
Networks”. Informatiktage 2008. Fachwissenschaftlicher Informatik-Kongress,
volume S-6 of Lecture Notes in Informatics, pages 15-18, 2008.

123