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

Title

Maximal Completion

Author(s)Klein, Dominik; Hirokawa, Nao

Citation

Proceedings of the 22nd International Conference
on Rewriting Techniques and Applications(RTA'11), 10: 71‑80

Issue Date

2011‑04‑26

Type

Conference Paper

Text version

publisher

URL

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

Rights© Dominik Klein and Nao Hirokawa; licensed under
Creative Commons License NC‑ND. 22ndInternational Conference on Rewriting Techniquesand Applications (RTA 11). Editor: M. Schmidt‑
Schauß; pp. 71‒80.

Description

Japan Advanced Institute of Science and Technology

Maximal Completion∗
Dominik Klein1 and Nao Hirokawa1
1

School of Information Science
Japan Advanced Institute of Science and Technology
Nomi, Japan{dominik.klein,hirokawa}@jaist.ac.jp

Abstract
Given an equational system, completion procedures compute an equivalent and complete (terminating and confluent) term rewrite system. We present a very simple and efficient completion
procedure, which is based on MaxSAT solving. Experiments show that the procedure is comparable to recent powerful completion tools.
1998 ACM Subject Classification F.4.2 Grammars and Other Rewriting Systems
Keywords and phrases Term Rewriting, Knuth-Bendix Completion, Multi-completion
Digital Object Identifier 10.4230/LIPIcs.RTA.2011.71
Category System Description

1

Introduction

Completion tries to construct from an equational system (ES) an equivalent complete(confluent and terminating) term rewrite system (TRS). The standard completion procedureby Knuth and Bendix [14] and Huet [12] takes not only a target ES but also a reduction
order as a parameter. This reduction order is used to ensure termination of a resulting
complete TRS. Because the choice of a reduction order is critical for getting a successful
run of the procedure, several attempts have been made to automatically find such an order.
Here we mention the pioneering work of Kurihara and Kondo [16] on running completion
using multiple orders in parallel and the approach by Wehrman et al. [23] to automaticallyconstruct a reduction order using a termination tool on the fly. Very recently Sato et al. [21]showed how both approaches can be combined.
We present a new completion procedure, dubbed maximal completion. This procedure
induces a set of (exponentially) many TRSs to find a desired complete TRS from the set.
Via a natural encoding into maximal satisfiability problems, the procedure can be easily
implemented by a MaxSAT (or MaxSMT) solver. Experiments by our completion tool
Maxcomp show that this approach performs comparable with the above approaches. The
tool Maxcomp is available at:
http://www.jaist.ac.jp/project/maxcomp/This paper is concerned with constructing complete term rewriting systems only. But weanticipate that our approach can be adapted for unfailing completion [6], which gives up theaim of trying to construct a complete system. Instead it only aims to construct a ground∗

The research described in this paper is supported by the Grant-in-Aid for Young Scientists (B) 22700009
of the Japan Society for the Promotion of Science.

© Dominik Klein and Nao Hirokawa;
licensed under Creative Commons License NC-ND
22nd International Conference on Rewriting Techniques and Applications (RTA’11).
Editor: M. Schmidt-Schauß; pp. 71–80
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

72

Maximal Completion

complete (ground terminating and ground confluent) system, which is effectively used infirst-order theorem proving.
The paper is structured as follows: In Section 2 we introduce maximal completion, and its
automation techniques are described in Section 3. Section 4 relates the procedure to existing
ones. Empirical results are reported in Section 5, where our tool Maxcomp is comparedwith the state-of-art completion tools Slothrop [23] and mkbTT [25]. Finally, we conclude
the presentation in Section 6 by mentioning potential future work. Throughout the paper,
we assume familiarity with term rewriting in general, and most notions and notations areborrowed from [3, 22].

2

Maximal Completion

A TRS is complete if it is terminating and confluent. We say that R is a complete TRS
for an ES E if R is a complete TRS with ↔∗R = ↔∗E . The completion problem is to find acomplete TRS for a given E.
To derive a procedure for completion, we recall the definition of critical pairs. An overlap(`1 → r1 , p, `2 → r2 )µ of a TRS R consists of variants `1 → r1 and `2 → r2 of rewrite rulesof R without common variables, a non-variable position p ∈ Pos(`2 ), and a most generalunifier µ of `1 and `2 |p . If p =  then we require that `1 → r1 and `2 → r2 are not variantsof the same rewrite rule. The induced critical pair is `2 µ[r1 µ]p ≈ r2 µ, and the set of all suchpairs of R is written as CP(R). Note that pairs (s, t) of terms are denoted by s ≈ t or s → tdepending on the contexts. Below, we write ↓R for the joinability relation →∗R · R∗ ←.
I Lemma 1. R is a complete TRS 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 [14, 11], confluenceof R follows from CP(R) ⊆ ↓R and termination of R. Moreover, E ⊆ ↓R and R ⊆ ↔∗E yield↔∗R = ↔∗E . The “only if”-direction is immediate from ↔∗E ⊆ ↔∗R ⊆ ↓R .
J
Lemma 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 hold for 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 .
I Definition 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.
I Theorem 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. Let t↓R denote a fixed
normal form of t with respect to R. We say that a TRS R is over 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)Dominik Klein and Nao Hirokawa

73

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.
I Lemma 4. The following claims hold:(a) Let R ⊆ R0 ⊆ ↔∗E and R0 terminating. 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 straightforward from the first claim, and theconverse is trivial.
J
We illustrate maximal completion with an example. In examples the inverse t ≈ s of anindexed rule i : s ≈ t is denoted as i0 .
I Example 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 thejoin-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(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 many superfluous
rules. It is known that this problem is resolved by computing reduced TRSs (cf. [12]). A
TRS R is reduced if ` ∈ NF (R \ {` → r}) and r ∈ NF (R) for all rules ` → r ∈ R. We writeb for the reduced TRSRe | ` ∈ NF (Re \ {` → r})}{` → r ∈ R
e = {` → r↓R | ` → r ∈ R}. The TRS R
b fulfills the desired property:
where Rb is complete for E.
I Lemma 6. If a TRS R is complete for E, then R
b is complete and ↔∗ = ↔∗ (see [19]).
Proof. Using the fact that R
R
b
R

J

b is {1, 2, 3, 8}.
I Example 7 (continued from Example 5). The reduced version R
As Example 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 tothe subsequent two sections for further discussion on R(C) and S(C).

R TA ’ 1 1

74

Maximal Completion

3

Automation

We describe how to automate the approach of Section 2.

3.1

Computing R(C)

Since termination is undecidable, for automation we compute maximal elements in 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 tocheck termination of each of them to compute maximal elements. We present a solution
using MaxSAT solving.
In last years, SAT/SMT-encodings of termination conditions based on existing subclassesof reduction orders have been extensively investigated, and today they are well-established.
Here we mention recursive path orders [17, 7], Knuth-Bendix orders [26] and orders basedon matrix interpretations [9]. 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 can be 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. We construct thefollowing optimization problem ψ:Maximize_(s > t) ⊕ (t > s)s≈t∈C

subject to

k
^

_

`>r

i=1 `→r∈(C∪C −1 )\Ri

where C1 ⊕ C2 stands for the exclusive-or (C1 ∧ (¬C2 )) ∨ ((¬C1 ) ∧ C2 ). Since each ` > r
can be encoded w.r.t. a particular class of reduction orders to Boolean constraints, ψ canbe treated as an instance of MaxSAT/MaxSMT. A solution yields a maximal subset oforiented 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.
Finally, in our implementation we do not compute all maximal terminating TRSs. Thisis 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 acomplete TRS R ∈ R(C), but we fail to select it. Since R is a terminating TRS over C ∪ S(C),by Lemma 4 (a) there exists a maximal terminating, complete TRS R0 ∈ R(C ∪ S(C)) withR ⊆ R0 . Thus when missing the complete TRS R in one iteration, there is still a chance toselect R0 in the next one.

3.2

Filtering S(C)Our implementation of the parameter function S(C) follows closely the proposed one ofSection 2 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. [3, 25, 23]) that selectDominik Klein and Nao Hirokawa

75

only certain kinds of equalities. We also heuristically select equalities, since otherwise thenumber of critical pairs grows too fast and our implementation fails to handle it. In order toaddress it, we first normalize the equalities to filter out all those whose size exceeds a boundd. Then, we select n smallest equalities. 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nfor the set of the n smallest equalities in C. With these notations, S(C) can be described asfollows:[
S(C) ={s↓R ≈ t↓R | s ≈ t ∈ E ∪ CP(R) and s↓R 6= t↓R }<d nR∈ R(C)

4

Related Work and Comparison

We relate our procedure ϕ to existing completion methods. Due to their algorithmic nature
precise simulations are difficult, but we capture their main features. We say that S is aninter-reduced version of a terminating TRS R, if S is a terminating reduced TRS whose rules
are obtained by rewriting rules in R by R itself.
Knuth-Bendix Completion [14, 12]. Let > be a reduction order for the Knuth-Bendix
completion procedure and for the orientable part {` → r ∈ C ∪ C −1 | ` > r} we write C > .
This procedure 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 [16]. Multi-completion uses a class of reduction orders >1 , . . . , >n
to run Knuth-Bendix completion in parallel. 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 }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 of compatibility checks as wellas computations of normal forms. In order to gain efficiency Kondo and Kurihara [16]provided a specialised data structure, so-called node for sharing these computations
among the orders.
Completion with termination tools [23]. This procedure does not require a reduction
order as an input parameter, because during its process a necessary reduction order isconstructed on the fly:R(C) = {R}andS(C) = {s↓R0 ≈ t↓R0 }where, R is a TRS over C whose termination is shown by a termination tool, R0 is aninter-reduced version of R, and s ≈ t ∈ C ∪ CP(R0 ). Unlike a fixed single reduction
order, a termination tool can find a number of terminating TRSs over C, which avoids
failure of Knuth-Bendix completion. But its drawback is a similar problem as withmulti-completion. In the paper [23] a heuristic for the best search strategy is suggested
to select one of the terminating TRSs. This approach significantly extends the power of
Knuth-Bendix completion, and has been adopted in their completion tool Slothrop.

R TA ’ 1 1

76

Maximal Completion

Multi-completion with termination tools [21, 25]. 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 a termination tool,
R0 is an inter-reduced version of some R ∈ R(C), and s ≈ t ∈ C ∪ CP(R0 ). A variant of
the node data structure in multi-completion provides a compact representation of R(C)as well as an efficient algorithm to compute it. This approach has been implemented in
the very effective completion tool mkbTT.
As described in the earlier sections, maximal completion only computes maximal terminating TRSs, which are often much fewer than all terminating TRSs, but it does not miss acomplete TRS. This is the main idea of our approach. One drawback is the current limited
power of maximal termination provers. Theoretically, Brute force search allows using atermination tool to compute maximal terminating TRSs. However, it is practically infeasible
due to exponentially many calls of the termination tool.
Another difference is the definition of S(C). Except for maximal completion, all procedures
use a singleton of an equality for S(C) and its selection is critical for successful runs. The
next example illustrates this.
I Example 8. Recall the ES E in Example 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-condition of ϕ.
Thus, ϕ({1, 2, 3}) = ϕ({1, . . . , 4}), where 4 is the single equality in S({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 hold again.
We continue the run with ϕ({1, . . . , 4}) = ϕ({1, . . . , 5}), where 5 in S({1, . . . , 4}) is
5:(x + y) + z ≈ s((p(x) + y) + z)(iii) Generally, 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 apriori. This is why mkbTT provides several selection strategies 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 one in Slothrop, and a sophisticated but complex data
structure like that of multi-completion.

Dominik Klein and Nao Hirokawa

77

Table 1 Summary for all 115 equational systems

5

LPO

KBO

mkbTT Maxcomp

mkbTT Maxcomp

mkbTT

termination tool
Slothrop

completed

70

86

67

69

81

71

failure

6

6

3

3

3

4

timeout

39

23

45

43

31

40

Experiments

We implemented maximal completion in the tool Maxcomp. The tool employs the SMT
solver Yices [8] to support LPO and KBO. Concerning parameter K for R(C) in Section 3,
at the beginning we use K = 2 to compute two maximal terminating TRSs. During therecursion of ϕ, we increase K whenever S(C) ⊆ C. Moreover, we fix n = 7 and d = 20 for
S(C), simply motivated by the fact that our tool cannot process larger n and d due to thenumber of equalities. If, at some point, no new equalities are generated and all maximal
terminating TRSs are computed (i.e. parameter K cannot be increased anymore), the toolstops with failure.
We compare Maxcomp with the two existing completion tools Slothrop and mkbTT. Since
the latter two tools require termination provers, we used AProVE [10] for Slothrop, and for
mkbTT its internally supplied prover TTT2 [15]. The test-bed consists of 115 equational
systems from the distribution of mkbTT.1 The tests were single-threaded run on a systemequipped with an Intel Core Duo L7500 with 1.6 GHz and 2 GB of RAM using a timeout of
300 seconds.
Table 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 as default. More detailed
results for a selected number of systems3 are depicted in Table 2, where we omitted systems
that could be solved by all tools with every termination method, or that could not be solved byany tool. Moreover for the two scalable systems BGK.Dxx and BGK.Mxx, that are constructedby using a natural number as an input parameter, only the largest ones considered, BGK.D16
and BGK.M14, are shown here. Numbers denote execution time in seconds, × denotes thetool stopped with failure, and ∞ denotes timeout.
It should be noted that the complete systems found by using a termination tool aremostly different from those found with LPO or KBO, since the reduction order constructedusing a termination tool is usually different from them. Also, for fairness it should be notedthat by choosing specific, suitable selection strategies for each equational system individually,
mkbTT can complete more systems than with its default selection strategy. To name one1

http://cl-informatik.uibk.ac.at/software/mkbtt/
mkbtt -s lpo for LPO, and mkbtt -s kbo for KBO.
3
The complete list is available at http://www.jaist.ac.jp/project/maxcomp/.
2

R TA ’ 1 1

78

Maximal Completion

Table 2 Experimental results

problem

LPO

KBO

termination tool

mkbTT Maxcomp

mkbTT Maxcomp

mkbTT

Slothrop

BGK94.D16

∞

37.48

∞

∞

74.91

∞

BGK94.M14

2.73

∞

5.73

∞

2.06

25.88

Chr89.A3

40.06

3.17

20.85

∞

∞

∞

fib

0.87

100.32

∞

∞

0.85

7.18

Les83.fib

0.10

0.01

∞

∞

0.23

2.82

Les83.subset

0.22

0.01

∞

∞

0.09

3.27

OKW95.dt1.theory

0.78

46.15

∞

∞

0.91

6.22

rl.theory

2.36

0.17

∞

1.21

1.76

8.07

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

∞

∞

0.12

0.02

0.08

1.39

SK90.3.18

0.15

0.01

∞

∞

0.30

3.50

SK90.3.22

∞

4.03

∞

8.03

∞

∞

SK90.3.27

13.31

21.09

36.47

0.53

72.31

∞

SK90.3.28

∞

20.23

53.58

∞

∞

110.76slothrop.ackermann

0.02

0.01

∞

∞

0.03

0.68

slothrop.cge

∞

∞

∞

∞

173.03∞slothrop.endo

∞

0.62

∞

0.38

3.88

7.60

slothrop.equiv.proofs

×

×

∞

∞

2.52

262.32slothrop.equiv.proofs.or

×

×

∞

∞

2.81

∞

slothrop.groups

0.45

0.08

∞

0.08

0.54

2.22

TPDB.zantema.z115

∞

0.73

5.76

42.63

15.27

203.69TPTP.COL060.1.theory

×

×

0.01

0.01

0.02

1.14

TPTP.GRP454.1.theory

17.13

2.65

49.63

0.14

109.87∞

TPTP.GRP457.1.theory

17.18

2.66

49.98

1.62

112.73∞

TPTP.GRP460.1.theory

∞

0.89

17.74

2.91

16.99

∞

TPTP.GRP463.1.theory

∞

1.76

17.80

3.26

16.91

∞

TPTP.GRP481.1.theory

∞

2.40

∞

57.20

∞

69.56

TPTP.GRP484.1.theory

∞

0.52

∞

13.52

∞

∞

TPTP.GRP487.1.theory

∞

1.00

∞

7.05

∞

×

TPTP.GRP490.1.theory

∞

0.84

168.93

13.21

∞

∞

TPTP.GRP493.1.theory

∞

5.13

40.54

2.83

∞

∞

TPTP.GRP496.1.theory

∞

0.90

∞

11.13

∞

241.10WS06.proofreduction

∞

∞

∞

∞

162.66∞

Dominik Klein and Nao Hirokawa

79

example, mkbTT completes SK90.3.22 with LPO and selection strategy old [25] withinroughly 40 seconds, however times out after 300 seconds with all other predefined 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.
Lastly, concerning the timeout, with very few exceptions, a higher timeout seems not toaffect the results. 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. The parameter K mostly remains unchanged at 2, and for the vast
majority of successful runs does not exceed 5, the maximum being 14.

6

Conclusion and future work

We have illustrated a very compact framework for (Knuth-Bendix) completion and demonstrated how to effectively automate it by employing modern MaxSAT solvers. Despite relyingon (not very powerful) simplification orders to show termination in our implementation,
experimental results indicate practical viability and, within the test-scenario as indicatedhere, competitiveness compared to all other known approaches. To conclude, we mention
potential future work:
Recapitulating termination techniques into maximal termination is crucial to extend
the capability of maximal completion. We plan to implement matrix interpretations [9],which are a recently emerged very powerful class of reduction orders: For instance, alexicographic combination of matrix interpretations can prove termination of a complete
TRS for the system CGE2 [23]. Moreover, adaptation of the dependency pair method [2]and semantic labeling [27] for maximal termination is an important challenge.
In order to achieve better scalability the growth of S(C) in the iteration of ϕ needs tobe limited. In Knuth-Bendix completion and its variants, inter-reduction is employed
as well as the application of various critical pair criteria ([4, 13]). We expect that thesetechniques can be adapted in our framework.
Last but not least, application to theorem proving is an important direction. There arevariations of Knuth-Bendix completion including unfailing completion [5] and rewriting
induction [20, 1], which are very successfully employed in powerful theorem provers
like Waldmeister [18]. However, these variations require a fixed reduction order. Veryrecently Winkler and Middeldorp [24] adapted multi-completion with termination tools
for unfailing completion to overcome this restriction. We anticipate that our approach
can be integrated in these settings.
Acknowledgements We thank Sarah Winkler and Aart Middeldorp for their valuablecomments.
References
1
2
3
4

T. Aoto. Dealing with non-orientable equations in rewriting induction. In RTA 2006,
volume 4098 of LNCS, pages 242–256, 2006.
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. TheoreticalComputer Science, 236(1-2):133–178, 2000.
F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998.
L. Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic
Computation, 6(1):1–18, 1988.

R TA ’ 1 1

80

Maximal Completion

5
6
7
8
9
10

11
12
13

14
15
16
17

18
19
20
21
22
23
24
25
26
27

L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In LICS,
pages 346–357. IEEE Computer Society, 1986.
L. Bachmair, N. Dershowitz, and D. A. Plaisted. Resolution of Equations in Algebraic
Structures: Completion without Failure, volume 2, pages 1–30. Academic Press, 1989.
M. Codish, V. Lagoon, and P. Stuckey. Solving partial order constraints for LPO termination. In RTA 2006, volume 4098 of LNCS, pages 4–18, 2006.
B. Dutertre and L. D. Moura. A fast linear-arithmetic solver for dpll(t). In CAV, pages
81–94, 2006.
J. Endrullis, J. Waldmann, and H. Zantema. Matrix interpretations for proving terminationof term rewriting. Journal of Automated Reasoning, 40(2-3):195–220, 2008.
J. Giesl, P. Schneider-Kamp, and R. Thiemann. AProVE 1.2: Automatic termination
proofs in the dependency pair framework. In IJCAR 2006, volume 4130 of LNAI, pages
281–286, 2006.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting
systems. Journal of the ACM, 27(4):797–821, 1980.
G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm.
Journal of Computer and System Sciences, 21(1):11–21, 1981.
D. Kapur, D. R. Musser, and P. Narendran. Only prime superpositions need be consideredin the Knuth-Bendix completion procedure. Journal of Symbolic Computation, 6(1):19–36,
1988.
D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor,
Computational Problems in Abstract Algebra, pages 263–297. 1970.
M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp. Tyrolean termination tool 2. In RTA
2009, volume 5595 of LNCS, pages 295–304, 2009.
M. Kurihara and H. Kondo. Completion for multiple reduction orderings. Journal ofAutomated Reasoning, 23(1):25–42, 1999.
M. Kurihara and H. Kondo. Efficient BDD encodings for partial order constraints withapplication to expert systems in software verification. In IEA/AEI, volume 3029 of LNAI,
pages 827–837, 2004.
B. Löchner and T. Hillenbrand. A phytography of Waldmeister. AI Communications,15(2–3):127–133, 2002.
Y. Métivier. About the rewriting systems produced by the Knuth-Bendix completion algorithm. Information Processing Letters, 16(1):31–34, 1983.
U. S. Reddy. Term rewriting induction. In CADE 1990, volume 449 of LNCS, pages
162–177, 1990.
H. Sato, S. Winkler, M. Kurihara, and A. Middeldorp. Multi-completion with termination
tools (system description). In IJCAR 2008, LNCS, pages 306–312, 2008.
TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer
Science. Cambridge University Press, 2003.
I. Wehrman, A. Stump, and E. M. Westbrook. Slothrop: Knuth-Bendix completion with amodern termination checker. In RTA 2006, LNCS, pages 287–296, 2006.
S. Winkler and A. Middeldorp. Termination tools in ordered completion. In IJCAR 2010,
volume 6173 of LNAI, pages 518–532, 2010.
S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara. Optimizing mkbtt (system description). In RTA 2010, LIPIcs, 2010.
H. Zankl, N. Hirokawa, and A. Middeldorp. KBO orientability. Journal of AutomatedReasoning, 43(2):173–201, 2009.
H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.