Completion procedures as Semidecision procedures ^{∗}

Maria Paola Bonacina Jieh Hsiang Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794-4400, USA {bonacina,hsiang}@sbcs.sunysb.edu

December 14, 1990

Abstract

In this paper we give a new abstract framework for the study of Knuth-Bendix type completion procedures, which are regarded as semidecision procedures for theorem proving.

First, we extend the classical proof orderings approach started in [6] in such a way that proofs of different theorems can also be compared. This is necessary for the application of proof orderings to theorem proving derivations. We use proof orderings to uniformly define all the fundamental concepts in terms of proof reduction.

A completion procedure is given by a set of inference rules and a search plan. The inference rules determine what can be derived from given data. The search plan chooses at each step of the derivation which inference rule to apply to which data. Each inference step either reduces the proof of a theorem or deletes a redundant sentence. Our definition of redundancy is based on the assumed proof ordering. We have shown in [16] that our definition subsume those given in [50, 13].

We prove that if the inference rules are refutationally complete and the search plan is fair, a completion procedure is a semidecision procedure for theorem proving. The key part of this result is the notion of fairness. Our definition of fairness is the first definition of fairness for completion procedures which addresses the theorem proving problem. It is new in three ways: it is target oriented, that is it keeps the theorem to be proved into consideration, it is explicitly stated as a property of the search plan and it is defined in terms of proof reduction, so that expansion inferences and contraction inferences are treated uniformly. According to this definition of fairness, it is not necessary to consider all critical pairs in a derivation for the derivation to be fair. This is because not all critical pairs are necessary to prove a given theorem. Considering all critical pairs is an unnecessary source of inefficiency in a theorem proving derivation.

We also show that the process of diproving inductive theorems by the so called inductionless induction method is a semidecision process. Finally, we present according to our framework, some equational completion procedures based on Unfailing Knuth-Bendix completion.

∗Research supported in part by grants CCR-8805734, INT-8715231 and CCR-8901322, funded by the National Science Foundation. The first author is also supported by Dottorato di ricerca in Informatica, Universitá degli Studi di Milano, Italy.

1 Introduction

The Knuth-Bendix completion procedure [49] computes a possibly infinite confluent rewrite system equivalent to a given set of equations [38]. If a set of equations E and an equation s ≃ t are given, it semidecides whether s ≃ t is a theorem of E, as first remarked in [51, 39]. These results hold if the procedure does not fail on an unoriented equation. Unoriented equations can be handled by adopting the Unfailing Knuth-Bendix method [35, 11], which gives a ground confluent set of equations.

Many completion procedures, related to Knuth-Bendix to different extents, have been designed. They include procedures for equational theories with special sets of axioms [54, 41, 7], Horn logic with equality [50, 27], first order logic [31, 32, 46, 8], first order logic with equality [33, 34, 36, 37, 57, 60, 12, 13], inductive theorem proving in equational and Horn theories [40, 29, 50] and logic programming [20, 21, 22, 15]. Surveys have been given in [24, 25].

A completion procedure is composed of inference rules and a search plan. The inference rules determine what can be derived from given data. The search plan chooses at each step of the derivation which inference rule to apply to which data and therefore it determines the unique derivation that the procedure computes from a given input.

The interpretation of Knuth-Bendix completion as generator of confluent systems is by far the most well known one, whereas theorem proving is basically regarded as a side effect of the generation of a confluent system. This view of completion is not acceptable from the theorem proving perspective, because a procedure which is guaranteed to eventually generate a confluent system cannot be efficient as theorem prover. In this work we reverse the traditional way of presenting completion procedures: we present them as semidecision procedures with the generation of confluent systems as a special side effect.

The interpretation of completion as semidecision procedure appeared first in [39]. Huet proved that if the search plan is fair, the limit of an unfailing Knuth-Bendix derivation is a confluent rewrite system and, as a consequence, if a theorem s ≃ t is given to the procedure, it semidecides the validity of s ≃ t. The same result was obtained in a more general framework in [6].

We decouple the interpretation of completion as semidecision procedure from the interpretation of completion as generator of confluent systems. We prove that if the inference rules are refutationally complete and the search plan is fair, a completion procedure is a semidecision procedure. Refutational completeness means that for all unsatisfiable inputs, there exist successful derivations by the inference rules of the strategy. Fairness means that whenever successful derivations exist, the search plan guarantees that the computed derivation is successful, that is all the inference steps which are necessary to prove the goal are eventually done. In particular, all the critical pairs which are necessary to prove the goal are eventually considered. We give a new definition of fairness to capture this concept.

This notion of fairness is the key difference between completion for theorem proving and completion for the generation of confluent systems. In Huet’s landmark paper [39] and in all the following work on completion [6, 9, 57, 13], fairness of a derivation consists in eventually considering all critical pairs. We call this property uniform fairness in order to distinguish it from fairness for theorem proving. Uniform fairness is necessary for the limit of a derivation to be confluent, but it is not necessary for theorem proving, because not all the critical pairs are necessary to prove a given theorem. All the definitions of fairness of completion procedures appeared so far in the literature [39, 9, 57, 13] require uniform fairness, because they do not separate theorem proving from the generation of a confluent system.

Therefore, we have proved Huet’s classical result from weaker, strictly theorem proving oriented hypotheses, which do not imply any confluence property of the limit of the derivation, since such properties are not necessary for theorem proving. In our view, a completion procedure is first a theorem proving procedure, which also has the property of eventually generating confluent sets if it is uniformly fair.

The so called inductionless induction method is covered by the semidecision concept as well: completion for inductionless induction [40] is a semidecision procedure for disproving inductive theorems.

We conclude our work by presenting some completion procedures for equational logic: we show that the basic Unfailing Knuth-Bendix procedure [35, 11] and some of its extensions, such as the AC-UKB procedure [54, 41, 7, 1] with Cancellation laws [36], the S-strategy [35] and the Inequality Ordered Saturation strategy [3] fit nicely in our framework. To our knowledge, this is the first presentation of these extensions of the UKB procedure as sets of inference rules.

Our entire approach to completion procedures is coherently based on a notion of proof reduction. In theorem proving, one wants to reduce one single proof, the proof of the target theorem: the derivation halts successfully if the target has been reduced to some trivially true theorem, such as s ≃ s, whose proof is empty. In traditional completion, one wants to reduce all proofs: for instance, in Knuth-Bendix completion all equational proofs have to be reduced to rewrite proofs. In this proof reduction framework, fairness guarantees that the proof of the target is eventually reduced, whereas uniform fairness guarantees that all proofs are eventually reduced.

In order to formalize all concepts in terms of proof reduction, we need a notion of well founded proof ordering. Our starting point is the proof orderings approach originally given in [6, 9]. However, proof orderings as in [6] do not apply to a theorem proving derivation, because they allow to compare only two proofs of the same theorem. In theorem proving, the target is modified by inference steps applying to the theorem itself. Therefore, we give a new notion of proof ordering, where proofs of different theorems can be compared.

In this paper we concentrate on theorem proving. In [16], we compare our study of fairness with previous definitions of fairness in [9, 57, 13]. In [17], we complete our framework with a full generalization of Huet’s theorem in [39] and of its extensions in [50, 13] for uniformly fair derivations.

In the following we assume that the reader is familiar with basic concepts and notations about theorem proving, term rewriting systems, completion procedures and orderings. We refer to [25, 26] for basic definitions and notations.

2 Completion procedures for theorem proving

2.1 Proof orderings for theorem proving

Given a finite set of sentences S, we denote by T h(S) the theory of S, T h(S) = {φ|S ⊧ φ}, and we say that S is a presentation of the theory T h(S). The input for a theorem proving procedure is a pair (S; φ), where S is a presentation of a theory and φ the target. A theorem proving problem is to decide whether φ ∈ T h(S) and a theorem proving derivation is a sequence of deductions

(S_{0}; φ_{0}) ⊢ (S_{1}; φ_{1}) ⊢ … ⊢ (S_{i}; φ_{i}) ⊢ …,

where at each step the problem of deciding φ_{i} ∈ T h(S_{i}) reduces to the problem of deciding φ_{i+1} ∈ T h(S_{i+1}). A step (S_{i}; φ_{i}) ⊢ (S_{i+1}; φ_{i}), where the presentation is modified, is a forward reasoning step. A step (S_{i}; φ_{i}) ⊢ (S_{i}; φ_{i+1}), where the target is modified, is a backward reasoning step, which derives a new goal from the current one. Informally, the derivation halts successfully at stage k if φ_{k} ∈ T h(S_{k}) is trivially true and therefore it can be asserted that φ_{0} ∈ T h(S_{0}). In this section we introduce a notion of proof ordering, which allows us to describe a theorem proving derivation as a proof reduction process.

We denote proofs by capital Greek letters: Υ(S, φ) denotes a proof of φ from axioms in S. Proofs are often represented as trees whose nodes are labeled by sentences: the tree associated to Υ(S, φ) has φ as label of the root, elements in S as labels of the leaves and a node ψ has children ψ_{1} … ψ_{n} if ψ is derived from ψ_{1} … ψ_{n} by a step in Υ(S, φ). In equational logic, such a proof can also be represented as a chain [6]

s_{1} ↔_{l_{1}≃r_{1}} s_{2} ↔_{l_{2}≃r_{2}} … ↔_{l_{n−1}≃r_{n−1}} s_{n},

where s_{1} ↔_{l_{1}≃r_{1}} s_{2} means that the equality of s_{1} and s_{2} is established by the equation l_{1} ≃ r_{1} because s_{1} and s_{2} are c[l_{1}σ] and c[r_{1}σ] for some context c and substitution σ. We write s →_{l≃r} t if s ≻ t is known a priori.

An ordering on proofs is defined in general starting from some ordering on the data involved in the proofs. We recall that a simplification ordering on terms is a monotonic and stable ordering, i.e. s ≻ t implies c[sσ] ≻ c[tσ] for all contexts c and substitutions σ, with the property that a term is greater than any of its subterms. A simplification ordering is well founded. A complete simplification ordering is also total on the set of ground terms. Some well known simplification orderings are the recursive path ordering [19], the lexicographic path ordering [45] and the Knuth-Bendix ordering [49]. Such orderings are surveyed in [23]. Our first basic assumption is to have a complete simplification ordering ≻ on terms. We prefer to have a simplification ordering, even if a well founded, monotonic and stable ordering total on ground terms is sufficient. Given a complete simplification ordering ≻ on terms, it is possible to define complete simplification orderings on equations, clauses and sets of clauses based on ≻, as shown for instance in [37].

A proof ordering is a monotonic, stable and well founded ordering on proofs [6]. As an example we give the following proof ordering from [27]:

Example 2.1 A proof ordering to compare two ground equational proofs Υ(E, s ≃ t) = s ↔_{E}^{∗} t and Υ′(E′, s ≃ t) = s ↔_{E′}^{∗} t, can be defined as follows. We associate to a ground equational step s ↔_{l≃r} t the triple (s, l, t), if s ≻ t. We compare these triples by the lexicographic combination >^{e} of the complete simplification ordering ≻, the strict encompassment ordering ^{•} > and again the ordering ≻. The encompassment ordering ^{•}≥ is the composition of the subterm ordering and the subsumption ordering: t ^{•}≥s if t|u = sσ for some position u and substitution σ; t ^{•}>s if t ^{•}≥s and s ≠ t [25]. Then we compare two proofs Υ(E, s ≃ t) and Υ′(E′, s ≃ t) by the multiset extension >^{e}_{mul} of >^{e}.

The proof orderings defined in [6] allow us to compare only two proofs Υ(S, φ) and Υ′(S′, φ) of the same theorem φ in different presentations S and S′ of a theory. This notion of proof ordering is not suitable for theorem proving, because in a theorem proving derivation

(S_{0}; φ_{0}) ⊢ (S_{1}; φ_{1}) ⊢ … ⊢ (S_{i}; φ_{i}) ⊢ …

both the presentation and the target are transformed. In order to compare the proof of φ_{i} in S_{i} and the proof of φ_{i+1} in S_{i+1}, we need a proof ordering such that two proofs Υ(S, φ) and Υ′(S′, φ′) may be comparable. Proof orderings with this property do exist and can actually be obtained quite easily. For instance the proof ordering of the previous example can be transformed into a proof ordering for proofs of different theorems as follows:

Example 2.2 We can compare any two ground equational proofs Υ(E, s ≃ t) = s ↔_{E}^{∗} t and Υ′(E′, s′ ≃ t′) = s′ ↔_{E′}^{∗} t′ by comparing the pairs ({s, t}, s ↔_{E}^{∗} t) and ({s′, t′}, s′ ↔_{E′}^{∗} t′) by the lexicographic combination >_{u} of the multiset extension ≻_{mul} of the ordering ≻ on terms and the multiset extension >^{e}_{mul} of >^{e}.

Henceforth a proof ordering is a monotonic, stable, well founded ordering on proofs. The minimum proof is the empty proof. We denote by true the theorem whose proof is empty. For instance in equational logic, true is a trivial equality s ≃ s. Given a pair (S; φ), we can select a minimal proof among all proofs of φ from S:

Definition 2.1 Given a proof ordering >_{p}, we denote by Π(S, φ) a minimal proof of φ from S with respect to >_{p}, i.e. a proof such that for all proofs Υ(S, φ) of φ from S, Υ(S, φ) ≮_{p} Π(S, φ).

Having introduced this notion of proof ordering, we can regard a theorem proving derivation

(S_{0}; φ_{0}) ⊢ (S_{1}; φ_{1}) ⊢ … ⊢ (S_{i}; φ_{i}) ⊢ …,

as a process of reducing Π(S_{0}, φ_{0}) to the empty proof and φ_{0} to true. At each step Π(S_{i}, φ_{i}) is replaced by Π(S_{i+1}, φ_{i+1}) and the derivation halts successfully at stage k if Π(S_{k}, φ_{k}) is empty and φ_{k} is true.

Our generalization of the classical notion of proof orderings is more significant than it may seem at a first glance. Proof orderings were introduced in [6] to prove correctness of the Knuth-Bendix completion procedure as a procedure which generates possibly infinite, confluent term rewriting systems. A derivation by Knuth-Bendix completion in that context is a process of transforming a presentation

S_{0} ⊢ S_{1} ⊢ … ⊢ S_{i} ⊢ . . ..

In other words, it is a purely forward derivation. Since the purpose of such a derivation is to transform a presentation, it is sufficient to be able to compare Π(S_{i}, φ) and Π(S_{i+1}, φ) for any theorem φ in the theory.

This is not the case in theorem proving, since the purpose of a derivation is to prove a specific theorem. Theorem proving requires backward reasoning, since a theorem proving problem includes a target. Furthermore, backward reasoning is necessary to obtain a target-oriented and therefore presumably efficient procedure. The classical proof orderings approach does not apply to theorem proving because it does not provide for backward reasoning. On the other hand, our proof orderings approach applies to both theorem proving and traditional completion.

2.2 Inference rules and search plans

Since completion procedures are theorem proving strategies with special properties, we start by introducing some basic concepts about theorem proving strategies.

A theorem proving strategy is a pair P =< I; Σ >, where I is a set of inference rules and Σ is a search plan. Inference rules in I decide what consequences can be deduced from the available data and Σ decides which inference rule and which data to choose next. We discuss first the inference rules and next the search plan. The general form of an inference rule f is:

f: \frac{S}{S′}

where S and S′ are sets of sentences. The rule says that given S, the set S′ can be inferred. We distinguish between expansion inference rules and contraction inference rules, as they are called in [27]. An expansion inference rule expands a given set S into a new set S′ by deriving new sentences from sentences in S:

f: \frac{S}{S′} where S ⊂ S′.

A contraction inference rule contracts a given set S into a new set S′ by either deleting some sentences in S or replacing them by others:

f: \frac{S}{S′} where S ⊈ S′.

Different schemes for inference rules, called deduction and deletion, are given in [13]. We further distinguish between inference rules which transform the presentation and inference rules which transform the target. We assume that targets are clauses and therefore can be regarded as sets of literals:

• Presentation inference rules:

– Expansion inference rules: f: \frac{(S; φ)}{(S′; φ)} where S ⊂ S′.

– Contraction inference rules: f: \frac{(S; φ)}{(S′; φ)} where S ⊈ S′.

• Target inference rules:

– Expansion inference rules: f: \frac{(S; φ)}{(S; φ′)} where φ ⊂ φ′.

– Contraction inference rules: f: \frac{(S; φ)}{(S; φ′)} where φ ⊈ φ′.

Example 2.3 Deduction of a critical pair in Unfailing Knuth-Bendix completion is an expansion inference rule on the presentation, since it adds to the given set a new equation:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{p ≃ q, l ≃ r, p[r]_{u}σ ≃ qσ\}; ŝ ≃ t̂)} \begin{matrix}p|u ∉ X & (p|u)σ = lσ \\ pσ ⪯̸ qσ, p[r]_{u}σ \end{matrix}

where X is the set of variables, σ is a most general unifier and ≻ is the assumed complete simplification ordering on terms. Simplification of the target is a contraction inference rule:

\frac{(E ∪ \{l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{l ≃ r\}; ŝ[rσ]_{u} ≃ t̂)} \begin{matrix}ŝ|u = lσ \\ ŝ ≻ ŝ[rσ]_{u} \end{matrix}

The inference rules are required to be sound. A presentation inference rule is sound if T h(S′) ⊆ T h(S), since an application of a presentation rule involves the presentation only. A target inference rule is sound if T h(S ∪ {φ′}) ⊆ T h(S ∪ {φ}).

Deduction by presentation rules is deduction of consequences from the axioms or forward reasoning. A target rule applies to both the presentation and the target to infer a new target: deduction by target rules is backward reasoning. The Knuth-Bendix procedure computing critical pairs and simplifying rewrite rules to obtain a canonical system performs exclusively forward reasoning. If a theorem to be proved is given as target, the procedure also performs some backward reasoning, when it simplifies the target.

Finally, a search plan Σ decides which inference rule should be applied to what data at any given step during a derivation. It may set a precedence on the inference rules and a well founded ordering on data and proceed accordingly:

Example 2.4 A Simplification-first search plan [35] for Unfailing Knuth-Bendix completion is a search plan where Simplification has priority over Deduction. Therefore Deduction is considered only if Simplification does not apply to any equation. Equations can be sorted by the multiset extension ≻_{mul} of the ordering on terms, or by size, or by age such as in a first-in first-out plan.

2.3 Completion procedures

A completion procedure has then three components < I_{p}, I_{t}; Σ >, where I_{p} is the set of presentation inference rules, I_{t} is the set of target inference rules and Σ is the search plan.

A derivation by a completion procedure is a process of proof reduction. A target inference step modifies the target and therefore it affects the proof of the target. We require that the proof of the target is reduced:

Definition 2.2 A target inference step (S; φ) ⊢ (S; φ′) is proof-reducing if Π(S, φ) ≥_{p} Π(S, φ′). It is strictly proof-reducing if Π(S, φ) >_{p} Π(S, φ′).

Example 2.5 Simplification of the target as given in Example 2.3 is strictly proof-reducing. We assume the proof ordering >_{u} introduced in Example 2.2. We have {ŝ, t̂} ≻_{mul}{ŝ′, t̂′}, since ŝ ≻ ŝ′ and t̂= t̂′, assuming ŝ is simplified to ŝ′. Therefore Π(E, ŝ ≃ t̂) >_{u} Π(E, ŝ′ ≃ t̂′).

For a presentation inference step we allow more flexibility:

Definition 2.3 Given two pairs (S; φ) and (S′; φ′), the relation (S; φ) >_{p,T} (S′; φ′) holds if

1. either Π(S, φ) >_{p} Π(S′, φ′)

2. or

(a) Π(S, φ) = Π(S′, φ′),

(b) ∀ψ ∈ T , Π(S, ψ) ≥_{p} Π(S′, ψ) and

(c) ∃ψ ∈ T such that Π(S, ψ) >_{p} Π(S′, ψ).

Definition 2.4 A presentation inference step (S; φ) ⊢ (S′; φ) is proof-reducing on T if (S; φ) >_{p,T} (S′; φ) holds. It is strictly proof-reducing if Π(S, φ) >_{p} Π(S′, φ).

The condition (S_{i}; φ_{i}) >_{p,T} (S_{i+1}; φ_{i+1}) says that either the step reduces the proof of the target, or it reduces the proof of at least one theorem in T , while it does not increase the proof of any theorem in T . A step which reduces the proof of the target is proof-reducing, regardless of its effects on other theorems. On the other hand, an inference step on the presentation may not immediately decrease the proof of the target and still be necessary to decrease it eventually. Such a step is proof-reducing too, if it does not increase any proof and strictly decreases at least one.

Example 2.6 Deduction of a critical pair as given in Example 2.3 is proof-reducing. We assume the proof ordering >_{u} introduced in Example 2.2. Given two equations l ≃ r and p ≃ q, a critical overlap of l ≃ r and p ≃ q is any proof s ←_{l≃r} v →_{p≃q} t, where v is c[pτ] for some context c and substitution τ and (p|u)τ = lτ for some non variable subterm p|u of p. The Deduction rule applied to l ≃ r and p ≃ q generates the critical pair p[r]_{u}σ ≃ qσ, where σ is the mgu of p|u and l and therefore τ = σρ for some substitution ρ. Such a Deduction step affects a minimal proof by replacing any occurrence of the critical overlap s ←_{l≃r} v →_{p≃q} t by the equational step s ↔_{p[r]_{u}σ≃qσ} t, justified by the critical pair. We have {(v, l, s), (v, p, t)} >^{e}_{mul}{(s, p[r]_{u}σ, t)} or {(v, l, s), (v, p, t)} >^{e}_{mul}{(t, qσ, s)}, depending on whether s ≻ t or t ≻ s, since v ≻ s, t. Therefore Π(E, ψ) >_{u} Π(E ∪ {p[r]_{u}σ ≃ qσ}, ψ) if the minimal proof of ψ in E contains a critical overlap between l ≃ r and p ≃ q, Π(E, ψ) = Π(E ∪ {p[r]_{u}σ ≃ qσ}, ψ) otherwise.

This notion of proof reduction applies to presentation inference steps which are either expansion steps or contraction steps which replace some sentences by others. A contraction step which deletes sentences without adding any cannot reduce any minimal proof. In order to characterize these steps, we introduce a notion of redundancy:

Definition 2.5 A sentence φ is redundant in S on domain T if ∀ψ ∈ T , Π(S, ψ) = Π(S∪{φ}, ψ).

A sentence is redundant in a presentation if adding it to the presentation does not affect any minimal proof.

Example 2.7 An inference rule of Unfailing Knuth-Bendix completion, which deletes an equation without adding any is Functional subsumption:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{l ≃ r\}; ŝ ≃ t̂)} (p ≃ q) ^{•} >(l ≃ r)

where (p ≃ q) ^{•} >(l ≃ r) means that p = c[lσ] and q = c[rσ] for some context c and substitution σ, where either c is not empty or σ is not a renaming of variables. An equation p ≃ q subsumed by l ≃ r is redundant according to the proof ordering >^{e}_{mul} and therefore to the proof ordering >_{u} as defined in Example 2.2. No minimal proof contains a step s ↔_{p≃q} t since the step s ↔_{l≃r} t is smaller: either {(s, p, t)} >^{e}_{mul}{(s, l, t)} or {(t, q, s)} >^{e}_{mul}{(t, r, s)}, depending on whether s ≻ t or t ≻ s, since p ^{•} >l and q ^{•} >r.

A notion of redundant clauses was introduced in [57] and in [13], where the term “redundant” was first used. We show in [16] that redundant clauses according to [57] and [13] are also redundant in our sense.

Definition 2.6 An inference step (S; φ) ⊢ (S′; φ′) is reducing on T if either it is proof-reducing on T or it deletes a sentence which is redundant in S on domain T .

Definition 2.7 An inference rule f is reducing if all the inference steps (S; φ) ⊢_{f}(S′; φ′) where f is applied are reducing.

We have finally all the elements to define a completion procedure:

Definition 2.8 A theorem proving strategy C =< I_{p}, I_{t}; Σ > is a completion procedure on domain T if for all pairs (S_{0}; φ_{0}), where S_{0} is a presentation of a theory and φ_{0} ∈ T , the derivation

(S_{0}; φ_{0}) ⊢_{C}(S_{1}; φ_{1}) ⊢_{C} … ⊢_{C}(S_{i}; φ_{i}) ⊢_{C} … has the following properties:

• monotonicity: ∀i ≥ 0, T h(S_{i+1}) ⊆ T h(S_{i}),

• relevance: ∀i ≥ 0, φ_{i+1} ∈ T h(S_{i+1}) if and only if φ_{i} ∈ T h(S_{i}) and

• reduction: ∀i ≥ 0, the step (S_{i}; φ_{i}) ⊢_{C}(S_{i+1}; φ_{i+1}) is reducing on T .

The domain T is the set of sentences where the inference rules of the completion procedure are reducing. For instance, for the Knuth-Bendix completion procedure T is the set of all equations. For the Unfailing Knuth-Bendix procedure, T is the set of all ground equations.

The monotonicity and relevance properties establish the soundness of the presentation and the target inference rules respectively. Monotonicity ensures that a presentation inference step does not create new elements which are not true in the theory, while relevance ensures that a target inference step replaces the target by a new target in such a way that proving the latter is equivalent to proving the former. For instance, a simplification step which reduces a target φ to φ′ satisfies the relevance requirement because if φ′ is true, φ is true as well. An interesting expansion inference rule for the target, called Ordered saturation will be described in detail in Section 3.3.

Reduction is the property which characterizes completion procedures. Clearly, if all the inference rules of a procedure are reducing, the procedure has the reduction property. We shall see in the second part that the inference rules of the known equational completion procedures are reducing. Most inference rules are reducing because they are suitably restricted by the complete simplification ordering ≻ on terms. A complete simplification ordering on data turns out to be a key element in characterizing a theorem proving strategy as a completion procedure.

2.4 Completion procedures as semidecision procedures

Given an input pair (S_{0}; φ_{0}), a completion procedure works by reducing the proof Π(S_{0}, φ_{0}). If the proof of the target is minimal, the process halts. Since the empty proof is smaller than any other proof, the computation halts at stage k if Π(S_{k}, φ_{k}) is empty and φ_{k} is true.

A procedure is complete if, whenever φ_{0} is a theorem of S_{0}, the derivation from (S_{0}; φ_{0}) reduces φ_{0} to true and halts. Completeness involves both the inference rules and the search plan. First, it requires that whenever φ_{0} ∈ T h(S_{0}), there exist successful derivations by the inference rules of the procedure. Second, it requires that whenever successful derivations exist, the search plan guarantees that the computed derivation is successful. We call these two properties refutational completeness of the inference rules and fairness of the search plan respectively.

In order to describe them, we introduce a structure called I-tree. Given a theorem proving problem (S_{0}; φ_{0}) and a set of inference rules I, the application of I to (S_{0}; φ_{0}) defines a tree, the I-tree rooted at (S_{0}; φ_{0}). The nodes of the tree are labeled by pairs (S; φ). The root is labeled by the input pair (S_{0}; φ_{0}). A node (S; φ) has a child (S′; φ′) if (S′; φ′) can be derived from (S; φ) in one step by an inference rule in I. The I-tree rooted at (S_{0}; φ_{0}) represents all the possible derivations by the inference rules in I starting from (S_{0}; φ_{0}).

A set I of inference rules is refutationally complete if whenever φ_{0} ∈ T h(S_{0}), the I-tree rooted at (S_{0}; φ_{0}) contains successful nodes, nodes of the form (S; true). More precisely, we define completeness as follows:

Definition 2.9 A set I = I_{p} ∪ I_{t} of inference rules is refutationally complete if whenever φ ∈ T h(S) and Π(S, φ) is not minimal, there exist derivations

(S; φ) ⊢_{I}(S_{1}; φ_{1}) ⊢_{I} … ⊢_{I}(S′; φ′) such that Π(S, φ) >_{p} Π(S′, φ′).

A set of inference rules is refutationally complete if it can reduce the proof of the target whenever it is not minimal. Since a proof ordering is well founded, it follows that if φ ∈ T h(S), the I-tree rooted at (S; φ) contains successful nodes. The advantage of giving the definition of completeness in terms of proof reduction is that the problem of proving completeness of I is reduced to the problem of exhibiting a suitable proof ordering.

Given a completion procedure C =< I_{p}, I_{t}; Σ >, I = I_{p} ∪ I_{t}, the I-tree rooted at (S_{0}; φ_{0}) represents the entire search space that the procedure can potentially derive from the input (S_{0}; φ_{0}). The search plan Σ selects a path in the I-tree: the derivation from input (S_{0}; φ_{0}) controlled by Σ is the path selected by Σ in the I-tree rooted at (S_{0}; φ_{0}). Once both a set of inference rules and a search plan are given, the derivation from (S_{0}; φ_{0}) is unique. A pair (S_{i}; φ_{i}) reached at stage i of the derivation is a visited node in the I-tree. Each visited node (S_{i}; φ_{i}) has generally many children, but the search plan selects only one of them to be (S_{i+1}; φ_{i+1}). A search plan Σ is fair if whenever the I-tree rooted at (S_{0}; φ_{0}) contains successful nodes, the derivation controlled by Σ starting at (S_{0}; φ_{0}) is guaranteed to reach a successful node. Similar to completeness, we define fairness in terms of proof reduction:

Definition 2.10 A derivation

(S_{0}; φ_{0}) ⊢_{C}(S_{1}; φ_{1}) ⊢_{C} … ⊢_{C}(S_{i}; φ_{i}) ⊢_{C} … controlled by a search plan Σ is fair if and only if for all i ≥ 0, if there exists a path

(S_{i}; φ_{i}) ⊢_{I} … ⊢_{I}(S′; φ′) in the I-tree rooted at (S_{0}; φ_{0}) such that Π(S_{i}, φ_{i}) >_{p} Π(S′, φ′), then there exists an (S_{j}; φ_{j}) for some j > i, such that Π(S′, φ′) ≥_{p} Π(S_{j}, φ_{j}). A search plan Σ is fair if all the derivations controlled by Σ are fair.

If the inference rules allow to reduce the proof of the target at (S_{i}; φ_{i}), a fair search plan guarantees that the proof of the target will be indeed reduced at a later stage (S_{j}; φ_{j}).

If the inference rules are complete and the search plan is fair, a completion procedure on domain T is a semidecision procedure for T h(S) ∩ T for all presentations S:

Theorem 2.1 Let C =< I_{p}, I_{t}; Σ > be a completion procedure. If the set I = I_{p} ∪ I_{t} of inference rules is refutationally complete and the search plan Σ is fair, then for all derivations

(S_{0}; φ_{0}) ⊢_{C}(S_{1}; φ_{1}) ⊢_{C} … ⊢_{C}(S_{i}; φ_{i}) ⊢_{C} …, where φ_{0} ∈ T h(S_{0}), ∀i ≥ 0, if Π(S_{i}, φ_{i}) is not minimal, then there exists an (S_{j}, φ_{j}), for some j > i, such that Π(S_{i}, φ_{i}) >_{p} Π(S_{j}, φ_{j}).

Proof: if Π(S_{i}, φ_{i}) is not minimal, then by completeness of the inference rules, there exists a path (S_{i}; φ_{i}) ⊢_{I} … ⊢_{I}(S′; φ′) such that Π(S_{i}, φ_{i}) >_{p} Π(S′, φ′). By fairness of the search plan, there exists an (S_{j}; φ_{j}), for some j > i, such that Π(S_{i}; φ_{i}) >_{p} Π(S′, φ′) ≥_{p} Π(S_{j}, φ_{j}). □

Corollary 2.1 If a completion procedure C on domain T has refutationally complete inference rules and fair search plan, then for all inputs (S_{0}; φ_{0}), if φ_{0} ∈ T h(S_{0}) then

• the derivation (S_{0}; φ_{0}) ⊢_{C}(S_{1}; φ_{1}) ⊢_{C} … ⊢_{C}(S_{i}; φ_{i}) ⊢_{C} … halts at stage k for some k ≥ 0 and

• φ_{k} = true.

Proof: if φ_{0} ∈ T h(S_{0}), the derivation halts at some stage k by Theorem 2.1 and the well foundedness of >_{p}. Therefore, the proof Π(S_{k}, φ_{k}) is minimal. Since we assume a proof ordering such that any two proofs can be compared, the only minimal proof is the empty proof and φ_{k} is true. □

In the following, we often write that a completion procedure is complete as a short hand for a completion procedure with complete inference rules and fair search plan.

2.5 Completion procedures as generators of decision procedures

In this paper we regard a completion procedure as a theorem proving procedure. In [17] we extend our framework to include completion procedures as generators of decision procedures.

If the search plan of a completion procedure satisfies a stronger fairness property, which we call uniform fairness, the procedure generates a possibly infinite saturated set. Uniform fairness is the fairness property which has been required so far for completion procedures [39, 9, 57, 13]. It basically consists in eventually considering all the inference steps. Saturated set is a generalization of confluent system: a set is saturated if no non-trivial consequences can be added [50, 13]. In [17], we define both uniform fairness and saturated set in terms of our notion of redundancy and we show that our definitions are equivalent to those given in [50, 13].

If a presentation is saturated, the derivations from that presentation are linear input derivations [18], that is derivations where each inference step applies to the goal to be proved. If linear input derivations from a saturated set are guaranteed to be well founded, a saturated set is a decision procedure and the completion procedure is a generator of decision procedures.

The well foundedness of the derivations is implied by additional requirements, which depend on the logic. In equational logic, a derivation s →^{∗} ∘ ←^{∗} t made only of well founded simplification steps by a confluent rewrite system is a well founded linear input derivation and a confluent system is a decision procedure. Sufficient conditions for well-foundedness of derivations for ground targets in Horn logic with equality are also known [50, 13].

In [17], we give a full generalization of the classical results in [39], which covers also the extensions to Horn logic with equality in [50, 13].

Very few theories have a finite saturated presentation and even fewer satisfy the additional requirement for a saturated presentation to be a decision procedure. Therefore, the interpretation of completion as semidecision procedure which we have developed here is more useful in practice.

3 Completion procedures in equational logic

In the second part of this work we give a new presentation of some Knuth-Bendix type completion procedures for equational logic, in the framework developed so far.

3.1 Unfailing Knuth-Bendix completion

The Unfailing Knuth-Bendix procedure [35, 11] is a semidecision procedure for equational theories. A presentation is a set of equations E_{0} and a theorem is an equational theorem ∀x̄s_{0} ≃ t_{0}. A derivation by UKB has the form

(E_{0}; ŝ_{0} ≃ t̂_{0}) ⊢_{UKB}(E_{1}; ŝ_{1} ≃ t̂_{1}) ⊢_{UKB}… (E_{i}; ŝ_{i} ≃ t̂_{i}) ⊢_{UKB}…

where we denote by ŝ_{0} ≃ t̂_{0} an equality which contains only universally quantified variables and therefore can be regarded as a ground equality. A derivation halts at stage k if ŝ_{k} and t̂_{k} are identical. We assume that ≻ is a complete simplification ordering such that ∀s, true ≺ s and we extend the encompassment ordering to equations: (p ≃ q) ^{•}≥(l ≃ r) if p|u = lσ and q|u = rσ, (p ≃ q) ^{•} >(l ≃ r) if (p ≃ q) ^{•} ≥(l ≃ r) but (p ≃ q) ≠ (l ≃ r). At each step of the completion process the pair (E_{i+1}; ŝ_{i+1} ≃ t̂_{i+1}) is derived from the pair (E_{i}; ŝ_{i} ≃ t̂_{i}) by applying one of the following inference rules:

• Presentation inference rules:

– Simplification:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{p[rσ]_{u} ≃ q, l ≃ r\}; ŝ ≃ t̂)} \begin{matrix}p|u = lσ & p ≻ p[rσ]_{u} \\ p ^{•} >l ∨ q ≻ p[rσ]_{u} \end{matrix}

– Deduction:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{p ≃ q, l ≃ r, p[r]_{u}σ ≃ qσ\}; ŝ ≃ t̂)} \begin{matrix}p|u ∉ X & (p|u)σ = lσ \\ pσ ⪯̸ qσ, p[r]_{u}σ \end{matrix}

– Deletion:

\frac{(E ∪ \{l ≃ l\}; ŝ ≃ t̂)}{(E; ŝ ≃ t̂)}

– Functional subsumption:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{l ≃ r\}; ŝ ≃ t̂)} (p ≃ q) ^{•} >(l ≃ r)

• Target inference rules:

– Simplification:

\frac{(E ∪ \{l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{l ≃ r\}; ŝ[rσ]_{u} ≃ t̂)} \begin{matrix}ŝ|u = lσ \\ ŝ ≻ ŝ[rσ]_{u} \end{matrix}

– Deletion:

\frac{(E; ŝ ≃ ŝ\})}{(E; true)}

The main inference rule of UKB is Simplification. A simplification step consists in applying an equation in E_{i} to simplify either another equation in E_{i} or the goal ŝ_{i} ≠ t̂_{i}. The step is performed only if p ≻ p[rσ]_{u}, that is a term is replaced by a smaller term. The condition p ^{•}>l ∨ q ≻ p[rσ]_{u} is explained as follows. If q ≻ p, that is simplification applies to the smaller side of p ≃ q, the condition q ≻ p[rσ]_{u} is trivially satisfied and no other restriction is needed. If q ⊁ p, simplification applies to the greater side of p ≃ q or p ≃ q is not ordered. If p ^{•} >l, either p is a proper instance of l or l matches a proper subterm of p. Otherwise, p =^{•} l, that is p and l are equal up to variables renaming, but q ≻ p[rσ]_{u}, that is the newly generated term p[rσ]_{u} is smaller than both sides of the simplified equation p ≃ q. We are going to see in a few paragraphs (Lemma 3.1) how these conditions ensures that Simplification is proof-reducing.

The Deduction inference rule is the only expansion rule of UKB. It works by checking for a superposition between two equations p ≃ q and l ≃ r. Two given equations superpose if there exists a non variable subterm, say p|u, which unifies with mgu σ with a side l of the other equation l ≃ r. This means that the term pσ is equal to both qσ and p[r]_{u}σ. The new equation p[r]_{u}σ ≃ qσ is called a critical pair. A critical pair is generated only if pσ ⪯̸ qσ, p[r]_{u}σ, that is the two equations are applied according to the simplification ordering. The original definitions of Simplification and Deduction given in [35] have slightly different conditions. Simplification requires that lσ ≻ rσ and superposition requires that pσ ⪯̸ qσ and lσ ⪯̸ rσ. We adopt here the conditions given in [27], because they put weaker requirements on simplification and stronger requirements on superposition than the original ones. However, these conditions may be more expensive to compute, since they require to perform both substitution application and term replacement.

The Functional subsumption inference rule deletes an equation p ≃ q because it is subsumed by another equation l ≃ r, that is p = c[lσ] and q = c[rσ] for some context c and substitution σ, where either c is not empty or σ is not a renaming of variables.

Simplification is the most important among the above inference rules, because it reduces dramatically the number and the size of the generated equations. A search plan for UKB should give to Simplification the highest priority among all the inference rules, so that the target and the presentation are always kept fully simplified. A search plan with this property is called Simplification-first [35]. If Simplification is not applied, the Deduction inference rule rapidly saturates the memory space with equations, making impossible to reach a proof in reasonable time.

In order to characterize the UKB procedure as a completion procedure, we define a proof ordering >_{UKB} to compare the proofs Π(E_{i}, ŝ_{i} ≃ t̂_{i}). We use the ordering >_{u} introduced in Example 2.2. We recall that we write and equational proof step s ↔_{l≃r} t meaning that s and t are c[lσ] and c[rσ] for some context c and substitution σ. We write s →_{l≃r} t if s ≻ t is known a priori. Then Π(E_{i}, ŝ_{i} ≃ t̂_{i}) >_{UKB} Π(E_{j}, ŝ_{j} ≃ t̂_{j}) holds if and only if ({ŝ_{i}, t̂_{i}}, ŝ_{i} ↔_{E_{i}}^{∗} t̂_{i}) >_{u} ({ŝ_{j}, t̂_{j}}, ŝ_{j} ↔_{E_{j}}^{∗} t̂_{j}) holds.

Lemma 3.1 The presentation inference rules of the UKB procedure are reducing.

Proof: we show that Deduction and Simplification are proof-reducing, Deletion and Functional subsumption delete redundant equations:

• the proof for Deduction was given in Example 2.6.

• A Simplification step where an equation p ≃ q is simplified to p[rσ]_{u} ≃ q by an equation l ≃ r, affects a minimal proof by replacing a step s ↔_{p≃q} t by two steps s →_{l≃r} v ↔_{p[rσ]_{u}≃q} t.

– If t ≻ s, we have {(t, q, s)} >^{e}_{mul}{(s, l, v), (t, q, v)} since t ≻ s and s ≻ v.

– If s ≻ t,

∗ if p ^{•} >l, we have
· if t ≻ v, {(s, p, t)} >^{e}_{mul}{(s, l, v), (t, q, v)} since p ^{•} >l and s ≻ t,

· if v ≻ t, {(s, p, t)} >^{e}_{mul}{(s, l, v), (v, q, t)} since p ^{•} >l and s ≻ v;

∗ if p =^{•} l and q ≻ p[rσ]_{u}, t ≻ v follows from q ≻ p[rσ]_{u} by stability and monotonicity

of ≻ and we have {(s, p, t)} >^{e}_{mul}{(s, l, v), (t, q, v)} since t ≻ v and s ≻ t.

• A trivial equation l ≃ l is redundant: no minimal proof contains a step s ↔_{l≃l} s since the subproof given by the single term s is smaller: {(s, l, s)} >^{e}_{mul}{ϵ}, where the empty triple ϵ is the proof complexity of s.

• the proof for Functional subsumption was given in Example 2.7. □

Lemma 3.2 The target inference rules of the UKB procedure are strictly proof-reducing.

Proof: the proof for Simplification was given already in Example 2.5. For a Deletion step we have {ŝ_{i}, t̂_{i}} ≻_{mul}{true}, since true is smaller than any term. Therefore Π(E_{i}, ŝ_{i} ≃ t̂_{i}) >_{UKB} Π(E_{i}, ŝ_{i+1} ≃ t̂_{i+1}). □

We can then show that UKB is a completion procedure:

Theorem 3.1 The Unfailing Knuth-Bendix procedure is a completion procedure on the domain T of all ground equalities.

Proof: for all equational presentations E_{0} and for all ground targets ŝ_{0} ≃ t̂_{0} the derivation

(E_{0}; ŝ_{0} ≃ t̂_{0}) ⊢_{UKB}(E_{1}; ŝ_{1} ≃ t̂_{1}) ⊢_{UKB}… (E_{i}; ŝ_{i} ≃ t̂_{i}) ⊢_{UKB}… has the monotonicity, relevance and reduction properties. Monotonicity and relevance follow by soundness of the inference rules, which is proved among others in [39, 6, 9]. Reduction follows from Lemma 3.1 and Lemma 3.2. □

If a fair search plan is provided, the UKB procedure is a semidecision procedure for equational theories:

Theorem 3.2 (Hsiang and Rusinowitch 1987) [35], (Bachmair, Dershowitz and Plaisted 1989)

[11] An equation ∀x̄s ≃ t is a theorem of an equational theory E if and only if the Unfailing Knuth-Bendix procedure derives true from (E; ŝ ≃ t̂).

3.2 Extensions: AC-UKB and cancellation laws

Many equational problems involve associative and commutative (AC) operators. An AC function f satisfies the equations

f(f(x, y), z) ≃ f(x, f(y, z)) (associativity) and

f(x, y) ≃ f(y, x) (commutativity).

Handling associativity and commutativity as any other equation turns out to be very inefficient, since commutativity may generate a very high number of equations through the Deduction inference rule. Also, many instances of commutativity may not be ordered by the chosen simplification ordering, so that simplification does not apply as often as it is desirable to reduce the size and the number of the equations.

The efficiency of the UKB strategy can be greatly improved if associativity and commutativity are not given in the input, but built in the inference rules. The UKB procedure with associativity and commutativity built in the inference rules is called AC-UKB [1]. The basic idea is to replace syntactic identity by equality modulo AC. Let AC be a set of associativity and commutativity axioms. Two terms s and t are equal modulo AC, if s ≃ t is a theorem of AC, which we write s =_{AC} t. The inference rules of the UKB procedure are modified in such a way that any two terms which are equal modulo AC are regarded as identical.

The first modification is to require that the complete simplification ordering on terms ≻ is in some sense “compatible” with replacing identity by equality modulo AC. More precisely, this “compatibility” requirement is a commutation property. Given two relations R and S, we say that R commutes over S if S ∘ R ⊆ R ∘ S, where ∘ is composition of relations. The complete simplification ordering ≻ is required to commute over =_{AC}: this means that for any two terms s and t, if there is a third term r such that s =_{AC} r and r ≻ t, there is also a term r′ such that s ≻ r′ and r′ =_{AC} t. Secondly, matching and unification are replaced by AC-matching and AC-unification. A term s matches a term t modulo AC if there is a substitution σ such that sσ =_{AC} t. Similarly, two terms s and t unify modulo AC if there is a substitution σ such that sσ =_{AC} tσ. Finally, the strict encompassment ordering ^{•}> is replaced by the ordering ^{•}>_{AC}, that is s ^{•} >_{AC}t if and only if s ^{•} >r and r =_{AC} t for some term r.

The set of inference rules of the UKB procedure is therefore modified as follows:

• Presentation inference rules:

– Simplification:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{p[rσ]_{u} ≃ q, l ≃ r\}; ŝ ≃ t̂)} \begin{matrix}p|u =_{AC} lσ & p ≻ p[rσ]_{u} \\ p ^{•} >_{AC}l ∨ q ≻ p[rσ]_{u} \end{matrix}

– Deduction:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{p ≃ q, l ≃ r, p[r]_{u}σ ≃ qσ\}; ŝ ≃ t̂)} \begin{matrix}p|u ∉ X & (p|u)σ =_{AC} lσ \\ pσ ⪯̸ qσ, p[r]_{u}σ \end{matrix}

– Extension:

\frac{(E ∪ \{f(p, q) ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{f(p, q) ≃ r, f(p, q, z) ≃ f(r, z)\}; ŝ ≃ t̂)} \begin{matrix}f is AC \\ f(p, q) ⪯̸ r \end{matrix}

– Deletion:

\frac{(E ∪ \{l ≃ l\}; ŝ ≃ t̂)}{(E; ŝ ≃ t̂)}

– Functional subsumption:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{l ≃ r\}; ŝ ≃ t̂)} (p ≃ q) ^{•} >_{AC}(l ≃ r)

• Target inference rules:

– Simplification:

\frac{(E ∪ \{l ≃ r\}; ŝ ≃ t̂)}{(E ∪ \{l ≃ r\}; ŝ[rσ]_{u} ≃ t̂)} \begin{matrix}ŝ|u =_{AC} lσ \\ ŝ ≻ ŝ[rσ]_{u} \end{matrix}

– Deletion:

\frac{(E; ŝ ≃ ŝ)}{(E; true)}

This set of inference rules is obtained from the set of inference rules of the UKB procedure by replacing identity by equality modulo AC as explained above and by adding a new inference rule, called Extension. The Extension inference rule is a specialized version of the Deduction inference rule, designed to compute superpositions of equations in E onto associativity axioms. Namely, if f(p, q) ≃ r is an equation in E, f is AC and f(p, q) ⪯̸ r, the equation f(p, q) ≃ r trivially superposes onto the associativity axiom f(f(x, y), z) ≃ f(x, f(y, z)), yielding the critical pair f(p, f(q, z)) ≃ f(r, z), which we write in flattened form as f(p, q, z) ≃ f(r, z). These critical pairs are called extended rules. Computing the extended rules is sufficien to ensure completeness of the AC-UKB procedure: no other critical pairs between E and AC need to be computed [54].

The extension of UKB to AC-UKB is feasible because algorithms for AC-matching and ACunification are available. An algorithm for AC-unification, its application in a completion procedure and the extended rules first appeared in [58, 59, 54]. The correctness of the AC-unification algorithm was proved in [28]. General theoretical frameworks for working with equations modulo a set of axioms A are given in [41] and in [7]. These results are surveyed in [25] and more specifically for unification problems in [44].

The UKB or AC-UKB procedure can be further improved by building in the inference rules for the cancellation laws. A function F is right cancellable if it satisfies the right cancellation law

∀x, y, z f(x, y) = f(z, y) ⊃ x = z

The left cancellation law is defined symmetrically. Cancellation laws may reduce considerably the size of the equations. They are implemented as inference rules as follows [36]:

Cancellation 1:

\frac{(E ∪ \{f(p, u) ≃ f(q, v)\}; ŝ ≃ t̂)}{(E ∪ \{f(p, u) ≃ f(q, v), pσ ≃ qσ\}; ŝ ≃ t̂)} uσ = vσ

Cancellation 2:

\frac{(E ∪ \{f(d_{1}, d_{2}) ≃ y\}; ŝ ≃ t̂)}{(E ∪ \{f(d_{1}, d_{2}) ≃ y, d_{1}σ ≃ x\}; ŝ ≃ t̂)} \begin{matrix}y ∈ V (d_{1}) & σ = \{y ↦ f(x, d_{2})\} \\ y ∉ V (d_{2}) & x is a new variable \end{matrix}

Cancellation 3:

\frac{(E ∪ \{f(p_{1}, q_{1}) ≃ r_{1}, f(p_{2}, q_{2}) ≃ r_{2}\}; ŝ ≃ t̂)}{(E ∪ \{f(p_{1}, q_{1}) ≃ r_{1}, f(p_{2}, q_{2}) ≃ r_{2}, p_{1}σ ≃ p_{2}σ\}; ŝ ≃ t̂)} \begin{matrix}q_{1}σ = q_{2}σ \\ r_{1}σ = r_{2}σ \end{matrix}

where the function f is right cancellable. In Cancellation 2, if the substitution σ = {y ↦ f(x, d_{2})} is applied to the given equation, it becomes f(d_{1}σ, d_{2}) ≃ f(x, d_{2}), since y does not occur in d_{2}. The cancellation law reduces this equation to d_{1}σ ≃ x.

In order to prove that the UKB procedure with the cancellation inference rules is a completion procedure, we need to prove that the Cancellation inference rules are proof-reducing. We adopt the proof ordering >_{UKBC} defined as follows: a ground equational step s ≃ t justified by an equation l ≃ r has complexity measure (s, lσ, l, t), if s is c[lσ], t is c[rσ] and s ≻ t. Complexity measures are compared by the lexicographic combination >^{ec} of the orderings ≻, ^{•}>, ^{•}> and ≻. Proofs are compared by the lexicographic combination >_{uc} of the multiset extansions ≻_{mul} and >^{ec}_{mul}: Π(E_{i}, ŝ_{i} ≃ t̂_{i}) >_{UKBC} Π(E_{j}, ŝ_{j} ≃ t̂_{j}) if and only if ({ŝ_{i}, t̂_{i}}, ŝ_{i} ↔_{E_{i}}^{∗} t̂_{i}) >_{uc} ({ŝ_{j}, t̂_{j}}, ŝ_{j} ↔_{E_{j}}^{∗} t̂_{j}). The proof of Lemma 3.1 is unaffected if >_{UKBC} replaces >_{UKB}.

Lemma 3.3 The Cancellation inference rules are proof-reducing.

Proof: we show that if (E_{i}; ŝ_{i} ≃ t̂_{i}) ⊢_{UKB}(E_{i+1}; ŝ_{i} ≃ t̂_{i}) is a Cancellation step, then if Π(E_{i}, ŝ ≃ t̂) ≠ Π(E_{i+1}, ŝ ≃ t̂), that is the inference step affects the proof of ŝ ≃ t̂, Π(E_{i}, ŝ ≃ t̂) >^{ec}_{mul} Π(E_{i+1}, ŝ ≃ t̂) holds.

• An application of the rule Cancellation 1 to an equation f(p, u) ≃ f(q, v) affects any minimal proof in E_{i} which contains a step s ↔ t such that s = c[f(p, u)τ], t = c[f(q, v)τ] and τ ^{•}≥ σ, where ^{•}≥ is the subsumption ordering and σ is the mgu such that uσ = vσ of the application of Cancellation 1. The step s ↔_{f(p,u)≃f(q,v)} t has complexity (s, f(p, u)τ, f(p, u), t), if s ≻ t. In the minimal proofs in E_{i+1} the step s ↔_{f(p,u)≃f(q,v)} t is replaced by a step s ↔_{pσ≃qσ} t justified by the new equation pσ ≃ qσ generated by the application of Cancellation 1. The step s ↔_{pσ≃qσ} t has complexity (s, pτ, pσ, t). Since f(p, u)τ ^{•} >pτ, {(s, f(p, u)τ, f(p, u), t)} >^{ec} {(s, pτ, pσ, t)} follows. A symmetric argument applies if t ≻ s.

• An application of the rule Cancellation 2 to an equation f(d_{1}, d_{2}) ≃ y affects any minimal proof in E_{i} which contains a step s ↔ t such that s = c[f(d_{1}, d_{2})τ], t = c[yτ] and τ ^{•}≥ σ, where σ is {y ↦ f(x, d_{2})}. Since y ∈ V (d_{1}), we have f(d_{1}, d_{2})τ ≻ yτ by the subterm property and therefore s ≻ t by monotonicity, so that the step s ↔ t has complexity (s, f(d_{1}, d_{2})τ, f(d_{1}, d_{2}), t). In the minimal proofs in E_{i+1} the step s ↔ t is replaced by a step s ↔_{d_{1}σ≃x} t justified by the new equation d_{1}σ ≃ x generated by the application of Cancellation 2. The step s ↔_{d_{1}σ≃x} t has complexity (s, d_{1}τ, d_{1}σ, t). Since f(d_{1}, d_{2})τ ^{•}>d_{1}τ, {(s, f(d_{1}, d_{2})τ, f(d_{1}, d_{2}), t)} >^{ec}_{mul}{(s, d_{1}τ, d_{1}σ, t)} follows.

• An application of the rule Cancellation 3 to two equations f(p_{1}, q_{1}) ≃ r_{1} and f(p_{2}, q_{2}) ≃ r_{2} affects any minimal proof in E_{i} which contains a subproof s ↔ u ↔ t such that s = c[f(p_{1}, q_{1})τ], u = c[r_{1}τ], t = c[f(p_{2}, q_{2})τ] and τ ^{•}≥ σ, where σ is the mgu such that q_{1}σ = q_{2}σ and r_{1}σ = r_{2}σ of the application of Cancellation 3. It follows that q_{1}τ = q_{2}τ and r_{1}τ = r_{2}τ too. The subproof s ↔ u ↔ t is replaced in any minimal proof in E_{i+1} by a single step s ↔_{p_{1}σ≃p_{2}σ} t justified by the new equation p_{1}σ ≃ p_{2}σ generated by the application of Cancellation 3.

1. If s ≻ t ≻ u, the subproof s ↔ u ↔ t has complexity {(s, f(p_{1}, q_{1})τ, f(p_{1}, q_{1}), u), (t, f(p_{2}, q_{2})τ, f(p_{2}, q_{2}), u)} and the step s ↔_{p_{1}σ≃p_{2}σ} t has complexity (s, p_{1}τ, p_{1}σ, t). Since f(p_{1}, q_{1})τ ^{•} >p_{1}τ, the result follows. A symmetric argument applies if t ≻ s ≻ u.

2. If s ≻ u ≻ t, the subproof s ↔ u ↔ t has complexity {(s, f(p_{1}, q_{1})τ, f(p_{1}, q_{1}), u), (u, r_{1}τ, r_{1}, t)} and the step s ↔_{p_{1}σ≃p_{2}σ} t has complexity (s, p_{1}τ, p_{1}σ, t). Since f(p_{1}, q_{1})τ ^{•}>p_{1}τ, the result follows. A symmetric argument applies if t ≻ u ≻ s.

3. If u ≻ s ≻ t, the subproof s ↔ u ↔ t has complexity {(u, r_{1}τ, r_{1}, s), (u, r_{1}τ, r_{1}, t)} and the step s ↔_{p_{1}σ≃p_{2}σ} t has complexity (s, p_{1}τ, p_{1}σ, t). Since u ≻ s, the result trivially follows. A symmetric argument applies if u ≻ t ≻ s. □

The UKB or AC-UKB procedure enriched with the inference rules for cancellation is complete [36]. Most of the experimental results reported in [1, 2, 14, 3, 5] are obtained by AC-UKB with the inference rules for cancellation.

3.3 Efficiency of the Unfailing Knuth-Bendix procedure

The UKB procedure is complete, but it is not very efficient in general. The main source of inefficiency is the Deduction inference rule, that is the forward reasoning component of UKB. All the backward reasoning steps are Simplification steps, which are strictly proof-reducing. On the other hand, a Deduction step is guaranteed to reduce the proof of some theorem, but not necessarily the proof of the target. The UKB procedure is inefficient because it generates many critical pairs which do not help in proving the target.

Therefore, our goal is to reduce the number of critical pairs generated or equivalently to perform less forward reasoning and more backward reasoning.

For the forward reasoning part, a possible approach to the problem consists in designing search plans which generate first the critical pairs that are estimated to be likely to reduce the proof of the target. Since the effect of a critical pair on the target cannot be completely determined a priori, such a search plan is based on heuristical criteria that measure how useful a critical pair is expected to be with respect to the task of simplifying the goal. Some examples of these heuristics are given in [3, 4].

For the backward reasoning part, we observe that if the target ŝ_{i} ≃ t̂_{i} is fully simplified with respect to E_{i}, ŝ_{i} ≃ t̂_{i} is minimal in the ordering ≻_{mul} among all the ground equations E-equivalent to the input target s_{0} ≃ t_{0}, where E = ⋃_{0≤j≤i} E_{j}. If a Simplification-first plan is adopted, UKB maintains a minimal target. Therefore, it could seem that no improvement can be obtained on the target side. However, we shall see that this is not the case.

The notion of minimal target is relative to the assumed partially ordered set (poset) of targets. If we assume the poset of ground equalities ordered by ≻_{mul}, ŝ_{i} ≃ t̂_{i} is minimal among the ground equations E-equivalent to the input target s_{0} ≃ t_{0}. The situation changes if we assume as poset of targets the poset of disjunctions of ground equalities ordered by an ordering ≻′_{mul} defined as follows: N_{1} ≻′_{mul} N_{2} if min(N_{1}) ≻_{mul} min(N_{2}), where N_{1} and N_{2} are disjunctions of ground equalities and min(N) is the smallest equality in N according to ≻_{mul}. Since the equalities are ground and the simplification ordering is total on ground, there is a smallest element in a disjunction and this ordering is well defined. Furthermore, the poset of equalities is embedded^{1} in the poset of disjunctions.

1Given two posets P_{1} = (D_{1}, >_{1}) and P_{2} = (D_{2}, >_{2}), an embedding h: P_{1} → P_{2} is an injective function h: D_{1} → D_{2} which preserves the ordering: for all x, y ∈ D_{1}, x >_{1} y implies h(x) >_{2} h(y). The function which maps a ground equality into the disjunction given by the ground equality itself is clearly an embedding of the poset of ground equalities into the poset of disjunctions of ground equalities, since the smallest element in a disjunction given by a single equality is the equality itself.

We show why the backward reasoning part of UKB is not guaranteed to compute a minimal target if the poset of disjunctions is assumed. Let (E_{i}; ŝ_{i} ≃ t̂_{i}) be the current stage in an UKB derivation and l ≃ r be an un-orientable equation in E_{i}, such that ŝ_{i}|u = lσ for some position u and substitution σ, but ŝ_{i} ≺ ŝ_{i}[rσ]_{u}. In other words, l matches a subterm of ŝ_{i} but Simplification does not apply because ŝ_{i} would not be replaced by a smaller term. However, we assume that the target ŝ_{i}[rσ]_{u} ≃ t̂_{i} is generated nonetheless and that by simplification it reduces to an equation which is smaller than ŝ_{i} ≃ t̂_{i}, that is ŝ_{i}[rσ]_{u} →_{E_{i}}^{∗} ŝ′, t̂_{i} →_{E_{i}}^{∗} t̂′ and {ŝ′, t̂′} ≺_{mul}{ŝ_{i}, t̂_{i}}. If these conditions hold, we have that the disjunction ŝ_{i} ≃ t̂_{i} ∨ ŝ′ ≃ t̂′ is smaller than the disjunction given by ŝ_{i} ≃ t̂_{i} alone in the poset of disjunctions defined above. Therefore, if we assume the poset of disjunctions as posets of targets, it is not true that UKB maintains a minimal target.

The intuition behind the choice of considering disjunctions of equalities rather than equalities is that if we consider more than one target equality, we have a greater chance to find a short proof. In order to work on disjunctions of equalities, we need to add to the UKB procedure an expansion inference rule, so that the target is eventually expanded into a disjunction of ground equalities. Such an expansion inference rule must satisfy the relevance requirement, so that proving the validity of any of the equalities in the disjunction is equivalent to prove the input target s_{0} ≃ t_{0}. Also, the application of such rule must be restricted, in order to avoid the generation of a high number of target equalities, which may slow down the search for a solution.

This new inference rule is superposition of an un-orientable equation onto a target equality ŝ ≃ t̂ to generate a new target equality. A newly generated target equality is first simplified as much as possible and then it is kept only if it is smaller than ŝ ≃ t̂:

Ordered saturation:

\frac{(E ∪ \{l ≃ r\}; N ∪ \{ŝ ≃ t̂\})}{(E ∪ \{l ≃ r\}; N ∪ \{ŝ ≃ t̂, ŝ′ ≃ t̂′\})} \begin{aligned}ŝ|u = lσ & ŝ[rσ]_{u} →_{E}^{∗} ŝ′ & t̂→_{E}^{∗} t̂′ \\ & \{ŝ′, t̂′\} ≺_{mul}\{ŝ, t̂\} \end{aligned}

Ordered saturation applies if ŝ ≺ ŝ[rσ]_{u}, since if ŝ ≻ ŝ[rσ]_{u} holds, simplification would apply. The target equality ŝ′ ≃ t̂′ might have a shorter proof than the other target equalities. We do not know which one has the shortest proof. We keep all of them to broaden our chance of reaching the proof as soon as possible.

In addition, we need to modify the Deletion inference rule, since the computation halts successfully as soon as an equality in the disjunction is reduced to a trivial equality:

Deletion:

\frac{(E; N ∪ \{ŝ ≃ ŝ\})}{(E; true)}

The procedure obtained by adding Ordered saturation to UKB and by modifying Deletion as above, is called the Inequality Ordered-Saturation strategy (IOS) [3]. A derivation by the IOS strategy has the form

(E_{0}; N_{0}) ⊢_{IOS}(E_{1}; N_{1}) ⊢_{IOS} … ⊢_{IOS}(E_{i}; N_{i}) ⊢_{IOS} … where the set N_{0} contains the initial goal ŝ_{0} ≃ t̂_{0} and at stage i, N_{i} is the current set of target equalities. The derivation halts at stage k if N_{k} contains a target ŝ_{i} ≃ t̂_{i} such that ŝ_{i} and t̂_{i} are identical and the clause in N_{k} reduces to true.

In order to show that the IOS strategy is a completion procedure, we assume a proof ordering >_{IOS} defined as follows: Π(E; N) >_{IOS} Π(E′; N′) if and only if Π(E; min(N)) >_{UKB} Π(E′; min(N′)). In other words the proof of a disjunction is represented by the proof of the smallest target in the disjunction.

Lemma 3.4 The Ordered saturation inference rule is proof-reducing.

Proof: we show that if (E_{i}; N_{i}) ⊢_{IOS}(E_{i}; N_{i+1}) is an Ordered saturation step, then Π(E_{i}, N_{i}) ≥_{IOS} Π(E_{i}, N_{i+1}). Since N_{i} ⊂ N_{i+1}, min(N_{i}) ⪰_{mul} min(N_{i+1}) and the result follows. □

Theorem 3.3 The Inequality Ordered-Saturation strategy is a completion procedure.

Proof: it follows from Theorem 3.1 and Lemma 3.4. □

The IOS strategy has been implemented and observed to perform better than the UKB procedure [3]. In practice, few target equalities are kept, so that the overhead of handling them is negligible with respect to the advantage of keeping more than one target.

3.4 The S-strategy

The S-strategy [35] is an extension of the UKB procedure to the logic of equality and inequality. A presentation is a set of equations E_{0} and a theorem φ is a sentence Q̄x̄ s_{0} ≃ t_{0} ∨… ∨ s_{n} ≃ t_{n}, where Q̄x̄ is any sequence of quantifier-variable pairs. A theorem φ in this form is transformed into a target N_{0} = s_{0} ≃ t_{0} ∨…∨s_{n} ≃ t_{n}, where all variables are implicitly existentially quantified, by replacing all the universally quantified variables by constants and by dropping the quantifiers. If φ is ∀x̄s_{0} ≃ t_{0}, N_{0} is ŝ_{0} ≃ t̂_{0} and the S-strategy reduces to the UKB procedure. A computation has the form

(E_{0}; N_{0}) ⊢_{S}(E_{1}; N_{1}) ⊢_{S} … ⊢_{S}(E_{i}; N_{i}) ⊢_{S} …

where ∀i ≥ 0, E_{i} is a set of equalities and N_{i} is a disjunction of target equalities with existentially quantified variables. A derivation halts at stage k if N_{k} contains a target s_{i} ≃ t_{i} whose sides are unifiable. The set of inference rules of UKB is modified as follows:

• Presentation inference rules:

– Simplification:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; N)}{(E ∪ \{p[rσ]_{u} ≃ q, l ≃ r\}; N)} \begin{matrix}p|u = lσ & p ≻ p[rσ]_{u} \\ p ^{•} >l ∨ q ≻ p[rσ]_{u} \end{matrix}

– Deduction:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; N)}{(E ∪ \{p ≃ q, l ≃ r, p[r]_{u}σ ≃ qσ\}; N)} \begin{matrix}p|u ∉ X & (p|u)σ = lσ \\ pσ ⪯̸ qσ, p[r]_{u}σ \end{matrix}

– Deletion:

\frac{(E ∪ \{l ≃ l\}; N)}{(E; N)}

– Functional subsumption:

\frac{(E ∪ \{p ≃ q, l ≃ r\}; N)}{(E ∪ \{l ≃ r\}; N)} (p ≃ q) ^{•} >(l ≃ r)

• Target inference rules:

– Simplification:

\frac{(E ∪ \{l ≃ r\}; N ∪ \{s ≃ t\})}{(E ∪ \{l ≃ r\}; N ∪ \{s[rσ]_{u} ≃ t\})} \begin{matrix}s|u = lσ \\ s ≻ s[rσ]_{u} \end{matrix}

– Deduction:

\frac{(E ∪ \{l ≃ r\}; N ∪ \{s ≃ t\})}{(E ∪ \{l ≃ r\}; N ∪ \{s ≃ t, s[r]_{u}σ ≃ tσ\})} \begin{matrix}s|u ∉ X & (s|u)σ = lσ \\ sσ ⪯̸ s[r]_{u}σ \end{matrix}

– Deletion:

\frac{(E; N ∪ \{s ≃ t\})}{(E; true)} sσ = tσ

The Deduction inference rule applies to both equalities and inequalities. In the second case no ordering based condition applies to the inequality. The Deletion rule for the target is modified because the target contains variables: a contradiction is detected when the two sides of a target equality unify.

In order to characterize the S-strategy as a completion procedure, we define the following ordering: Π(E_{i}; N_{i}) >_{S} Π(E_{i+1}; N_{i+1}) if and only if Π(Ê_{i}; ŝ_{i} ≃ t̂_{i}) >_{UKB} Π(Ê_{i+1}; ŝ_{i+1} ≃ t̂_{i+1}), where ∀i ≥ 0, Ê_{i} ∪ {ŝ_{i} ≠ t̂_{i}} is the smallest finite unsatisfiable set of ground instances of clauses in E_{i} ∪ ¬N_{i}. We show that this ordering is well defined. First we show how the pair (Ê_{i}; ŝ_{i} ≃ t̂_{i}) is defined. N_{i} is a theorem of E_{i} if and only if E_{i} ∪ ¬N_{i} is unsatisfiable, where N_{i} is a disjunction of equations s_{0} ≃ t_{0} ∨… ∨ s_{n} ≃ t_{n} with existentially quantified variables and therefore ¬N_{i} is a conjunction of inequalities s_{0} ≠ t_{0} ∧ … ∧ s_{n} ≠ t_{n} with universally quantified variables. By the Herbrand Theorem [18], the set E_{i} ∪ ¬N_{i} is unsatisfiable if and only if there is a finite subset of ground instances of the clauses in E_{i} ∪¬N_{i} which is unsatisfiable. Since ¬N_{i} is a set of inequalities with universally quantified variables, an unsatisfiable ground instance of E_{i}∪¬N_{i} needs to contain just one ground inequality: Ê_{i} ∪ {ŝ_{i} ≠ t̂_{i}} is the smallest such set with respect to the ordering ≻_{mul}. Since ≻ is total on ground terms, there exists a smallest set.

The above definition of the ordering >_{S} says that the complexity of the proof Π(E_{i}; N_{i}) is measured by the complexity of the ground proof Π(Ê_{i}; ŝ_{i} ≃ t̂_{i}) and that the impact of the inference steps on Π(E_{i}; N_{i}) is measured by the impact of the inference steps on Π(Ê_{i}; ŝ_{i} ≃ t̂_{i}). This approach is correct if to every inference step on (E_{i}; N_{i}) corresponds an inference steps on (Ê_{i}; ŝ_{i} ≃ t̂_{i}) and vice versa. In order to prove this, we need the following lemma, which rephrases for the S-strategy the Paramodulation Lifting Lemma. We recall that a ground substitution is E-irreducible if it does contain any pair {x ↦ t} such that t can be simplified by an equation in E.

Lemma 3.5 (Peterson 1983) [55], (Hsiang and Rusinowitch 1987) [37] If σ is a ground, Eirreducible substitution, then for all inference rules f of S-strategy, if (Eσ; sσ ≃ tσ) ⊢_{f}(E′; s′ ≃ t′), then (E; s ≃ t) ⊢_{f}(E′′; s′′ ≃ t′′), where E′ and s′ ≃ t′ are instances of E′′ and s′′ ≃ t′′ respectively.

Lemma 3.6 (E_{i}; N_{i}) ⊢_{S}(E_{i+1}; N_{i+1}) if and only if (Ê_{i}; ŝ_{i} ≃ t̂_{i}) ⊢_{S}(Ê_{i+1}; ŝ_{i+1} ≃ t̂_{i+1}).

Proof: ⇒) An inference step on (E_{i}; N_{i}) is trivially an inference step on (Ê_{i}; ŝ_{i} ≃ t̂_{i}), since an inference step on non ground clauses is trivially an inference step on all their instances. ⇐) Since (Ê_{i}; ŝ_{i} ≃ t̂_{i}) is minimal, Ê_{i} ⊆ E_{i}σ and ŝ_{i} ≃ t̂_{i} ∈ N_{i}σ for an E_{i}-irreducible substitution σ. Therefore, by Lemma 3.5, an inference step on (Ê_{i}; ŝ_{i} ≃ t̂_{i}) is an inference step on (E_{i}; N_{i}). □

We can finally state the following theorem:

Theorem 3.4 The S-strategy is a completion procedure on the domain T of all ground equalities.

Proof: monotonicity and relevance follow from the soundness of the inference rules. By the definition of the ordering >_{S}, the inference rules of S-strategy are proof-reducing if they are proofreducing on ground proofs with respect to the ordering >_{UKB}. This follows from Lemma 3.1 and Lemma 3.2, since target Deduction is just target Simplification if the target is ground. □

If a fair search plan is provided, the S-strategy is is a semidecision procedure for theories in the logic of equality and inequality:

Theorem 3.5 (Hsiang and Rusinowitch 1987) [35] A sentence Q̄x̄ s_{0} ≃ t_{0} ∨ … ∨ s_{n} ≃ t_{n} is a theorem of an equational theory E if and only if the S-strategy derives true from (E; s_{0} ≃ t_{0} ∨… ∨ s_{n} ≃ t_{n}).

4 Semidecision procedures for disproving inductive theorems

The Knuth-Bendix completion procedure has been also applied to disprove inductive theorem in equational theories. This method has been called inductionless induction, proof by consistency or proof by the lack of inconsistency by several authors [53, 30, 40, 52, 42, 29, 47, 48, 10, 43]. Extensions of this method to Horn logic with equality are explored in [50].

First of all, we show that a completion procedure applied to disprove inductive theorems is a semidecision procedure. We denote by G(S) the set of all ground terms on the signature of a presentation S and we use Ran(σ) to represent the range of a substitution σ, so that a ground substitution is a substitution such that Ran(σ) ⊂ G(S). A clause φ is an inductive theorem of S, written S ⊧_{Ind} φ, if and only if for all ground substitutions σ, φσ ∈ T h(S). We denote by Ind(S) the set of all the inductive theorems of S, Ind(S) = {φ| S ⊧_{Ind} φ}, by GT h(S) the set of all the ground theorems of S, GT h(S) = {φ| φ ∈ T h(S), φ ground} and by G(φ) the set of all the ground instances of φ, G(φ) = {φσ| Ran(σ) ⊂ G(S)}.

The set Ind(S) is not semidecidable. Even if we have a decision procedure for G(φ)∩GT h(S), we still cannot prove that φ is an inductive theorem, because the set G(φ) is infinite. However, the complement problem, that is proving that φ is not an inductive theorem of S, is semidecidable in certain theories.

If φ ∉ Ind(S), then there is a ground instance φσ such that φσ ∉ GT h(S). Therefore GT h(S ∪ {φ}) ≠ GT h(S), since φσ ∈ GT h(S ∪ {φ}) for all ground instances φσ. Thus, we can prove that φ is not an inductive theorem of S by proving the following target:

Φ_{0} = ∃σ Ran(σ) ⊂ G(S) ∃ψ ∈ S ∪ {φ} such that ψσ ∈ GT h(S ∪ {φ}) − GT h(S). If there exists an oracle O to decide such target, a completion procedure C =< I_{p}, I_{t}; Σ; O > equipped with the oracle O will be a semidecision procedure for disproving inductive theorems. A derivation has the form

(S ∪ {φ}; Φ_{0}) ⊢_{C}(S_{1}; Φ_{1}) ⊢_{C} … (S_{i}; Φ_{i}) ⊢_{C} …, where at each step the target is

Φ_{i} = ∃σ Ran(σ) ⊂ G(S) ∃ψ ∈ S_{i} such that ψσ ∈ GT h(S_{i}) − GT h(S). No inference step applies to the target: the procedure takes as input the presentation S∪{φ} given by the original presentation and the inductive conjecture and it proceeds by applying inference rules to the presentation until it obtains a presentation S_{k} such that the oracle applied to S_{k} answers positively and replaces Φ_{k} by true.

In the equational case, an oracle to decide Φ_{i} is available only under the assumption that the input set of equations E is ground confluent. Under this hypothesis, Φ_{i} is true if and only if there are two ground E-irreducible terms s and t such that s_{i}σ →_{E}^{∗} s, t_{i}σ →_{E}^{∗} t and s ≃ t ∈ GT h(E_{i}). Therefore, we can restrict our attention to ground E-irreducible terms.

A first oracle was given in [40] for equational presentations satisfying the principle of definition: the signature of E is given by the disjoint union of a set C of constructors and a set D of defined symbols, such that the set T (C) of all ground constructor terms is free and all function symbols in D are completely defined on C, that is for all ground term t ∈ T (F), there exists a unique ground constructor term t′ ∈ T (C) such that t ↔_{E}^{∗} t′.

A more general oracle was proposed in [42] for the Knuth-Bendix completion procedure and extended to the UKB procedure in [10]. This test is based on ground reducibility: a term t is ground E-reducible if for all ground substitutions σ, tσ is E-reducible. Ground E-reducibility is decidable [56] only if E is a ground confluent rewrite system. Therefore, the test in [42, 10] applies only if the input presentation E is ground confluent and all its equations can be oriented into rewrite rules.

In order to characterize an inductive theorem proving strategy as a completion procedure, we define the proof of the target Φ_{i} as follows:

Π(S_{i}, Φ_{i}) = Π(S_{i}, min{ψσ| ψ ∈ S_{i}, ψσ ∈ GT h(S_{i}) − GT h(S)}), that is the proof of the target is the proof of the smallest ground instance of some clause in S_{i} which is a theorem in S_{i} but not in S.

In the equational case, a completion procedure which eventually generates a ground confluent set of equations, is able to reduce the proofs of all ground theorems and therefore the proof of the target. However, this is not necessary. Since the proof of the target is the proof of the smallest ground theorem which is not a theorem of the original presentation, we can restrict our attention to a smaller set of ground theorems:

Definition 4.1 (Fribourg 1986) [29] Given a ground confluent presentation E, a set of substitutions H is E-inductively complete if for all ground substitutions ρ, there exist a substitution σ ∈ H and a ground substitution τ such that ρ →_{E}^{∗} στ.

We denote by H_{E} one such set and by IT_{E} the domain of all the ground equations which are instances of substitutions in H_{E}, that is IT_{E} = {(l ≃ r)στ|σ ∈ H_{E}, (l ≃ r)στ is ground}. The proof of the target is the proof of the smallest ground theorem which is not a theorem of the original presentation. This smallest ground theorem is in IT_{E} and therefore reducing the proofs of the theorems in IT_{E} is sufficient to guarantee that the proof of the target is reduced, as was first proved in [29] for the application of Knuth-Bendix completion to disprove inductive theorems in equational theories:

Theorem 4.1 (Fribourg 1986) [29] A completion procedure C =< I_{p}, I_{t}; Σ; O > on the domain IT_{E}, with complete inference rules and fair search plan is a semidecision procedure for the complement of Ind(E) for all equational presentations E, for which the oracle O is computable.

As a consequence, the Deduction inference rule of UKB can be restricted in such a way that a superposition between l ≃ r and p ≃ q at position u in p ≃ q is performed only if the set of mgus {σ|lσ = (p|u)σ, l ≃ r ∈ E_{i}} is E-inductively complete. The position u is called completely superposable in [29]. This result requires an algorithm to detect the completely superposable positions. An equivalent characterization is the following: a position u in p is completely superposable if for all ground instances (p|u)ρ there is an equation l ≃ r in E such that (p|u)ρ = lσ and lσ ≻ rσ. This shows that the problem of detecting completely superposable positions is basically an instance of the ground reducibility problem. However, if the presentation satisfies the principle of definition, a position u is completely superposable if p|u is a term which has a defined symbol at the root and only constructor symbols and variables at the positions below the root. Therefore, the above theorem can be applied in practice to presentations satisfying the principle of definition.

5 Conclusions

We have given a new abstract framework for the study of Knuth-Bendix type completion procedures, which are regarded as semidecision procedures for theorem proving.

All the fundamental concepts are uniformly defined in terms of proof reduction with respect to a well founded proof ordering. In order to do this, we have given a new, more general notion of proof ordering, such that also proofs of different theorem can be compared.

A completion procedure is given by a set of inference rules and a search plan. We have emphasized the distinction between these two components throughout our work. This distinction is often overlooked in the literature, where most theorem proving strategies are presented by giving the set of inference rules only, whereas the search plan is what ultimately turns a set of inference rules into a procedure.

If the inference rules are refutationally complete and the search plan is fair, a completion procedure is a semidecision procedure for theorem proving. The key part of this result is the notion of fairness. Our definition of fairness is the first definition of fairness for completion procedures which addresses the theorem proving problem. It is new in three ways: it is target oriented, that is it keeps the theorem to be proved into consideration, it is explicitly stated as a property of the search plan and it is defined in terms of proof reduction, so that expansion inferences and contraction inferences are treated uniformly. We have also shown that the process of diproving inductive theorems by the so called inductionless induction method is a semidecision process.

In the second part of this work, we have presented some equational completion procedures based on Unfailing Knuth-Bendix completion, which include the AC-UKB procedure with Cancellation laws, the S-strategy and the Inequality Ordered Saturation strategy. These extensions of UKB had not been presented in a unified framework for completion before.

Directions for further research include the study of efficient, fair, but not uniformly fair, search plans and the full extension of this approach to completion procedures for Horn and first order logic with equality.

References

[1] S.Anantharaman and J.Mzali, Unfailing Completion modulo a set of equations, Technical Report, LRI, Université de Paris Sud, 1989.

[2] S.Anantharaman, J.Hsiang and J.Mzali, SbReve2: A Term Rewriting Laboratory with (AC)-Unfailing Completion, in N.Dershowitz (ed.), Proceedings of the Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, USA, April 1989, Springer Verlag, Lecture Notes in Computer Science 355, 533–537, 1989.

[3] S.Anantharaman, J.Hsiang, Automated Proofs of the Moufang Identities in Alternative Rings, Journal of Automated Reasoning, Vol. 6, No. 1, 76–109, 1990.

[4] S.Anantharaman, N.Andrianarivelo, Heuristical Criteria in Refutational Theorem Proving, in A.Miola (ed.), Proceedings of the Symposium on the Design and Implementation of Systems for Symbolic Computation, 184–193, Capri, Italy, April 1990.

[5] S.Anantharaman, N.Andrianarivelo, M.P.Bonacina, J.Hsiang, SBR3: A Refutational Prover for Equational Theorems, to appear in M.Okada, S.Kaplan (eds.), Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990.

[6] L.Bachmair, N.Dershowitz, J.Hsiang, Orderings for Equational Proofs, in Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, 346–357, Cambridge, MA, June 1986.

[7] L.Bachmair, N.Dershowitz, Completion for rewriting modulo a congruence, in P.Lescanne (ed.), Proceedings of the Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, May 1987, Springer Verlag, Lecture Notes in Computer Science 256, 192–203, 1987.

[8] L.Bachmair, N.Dershowitz, Inference Rules for Rewrite-Based First-Order Theorem Proving, in Proceedings of the Second Annual Symposium on Logic in Computer Science, Ithaca, New York, June 1987.

[9] L.Bachmair, Proofs Methods for Equational Theories, Ph.D. thesis, Department of Computer Science, University of Illinois, Urbana, IL.,1987.

[10] L.Bachmair, Proof by consistency in equational theories, in Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, 228–233, Edinburgh, Scotland, July 1988.

[11] L.Bachmair, N.Dershowitz and D.A.Plaisted, Completion without failure, in H.Ait-Kaci, M.Nivat (eds.), Resolution of Equations in Algebraic Structures, Vol. II: Rewriting Techniques, 1–30, Academic Press, New York, 1989.

[12] L.Bachmair, H.Ganzinger, On Restrictions of Ordered Paramodulation with Simplification, in Proceedings of the Tenth International Conference on Automated Deduction, Kaiserslautern, Germany, July 1990.

[13] L.Bachmair, H.Ganzinger, Completion of First-Order Clauses with Equality by Strict Superposition, to appear in M.Okada, S.Kaplan (eds.), Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990.

[14] M.P.Bonacina, G.Sanna, KBlab: An Equational Theorem Prover for the Macintosh, in N.Dershowitz (ed.), Proceedings of the Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, USA, April 1989, Springer Verlag, Lecture Notes in Computer Science 355, 548–550, 1989.

[15] M.P.Bonacina, J.Hsiang, Operational and Denotational Semantics of Rewrite Programs, to appear in Proceedings of the North American Conference on Logic Programming, Austin, TX, October 1990.

[16] M.P.Bonacina, J.Hsiang, On fairness of completion-based theorem proving strategies, Technical report, Department of Computer Science, SUNY at Stony Brook.

[17] M.P.Bonacina, J.Hsiang, The Knuth-Bendix-Huet theorem and its extensions, in preparation.

[18] C.L.Chang, R.C.Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.

[19] N.Dershowitz, Z.Manna, Proving termination with multisets orderings, Communications of the ACM, Vol. 22, No. 8, 465–476, August 1979.

[20] N.Dershowitz, N.A.Josephson, Logic Programming by Completion, in Proceedings of the Second International Conference on Logic Programming, 313–320, Uppsala, Sweden, 1984.

[21] N.Dershowitz, Computing with Rewrite Systems, Information and Control, Vol. 65, 122– 157, 1985.

[22] N.Dershowitz, D.A.Plaisted, Logic Programming Cum Applicative Programming, in Proceedings of the IEEE Symposium on Logic Programming, 54–66, Boston, MA, 1985.

[23] N.Dershowitz, Termination of Rewriting, Journal of Symbolic Computation, Vol. 3, No. 1 & 2, 69–116, February/April 1987.

[24] N.Dershowitz, Completion and its Applications, in Proceedings of Conference on Resolution of Equations in Algebraic Structures, Lakeway, Texas, May 1987.

[25] N.Dershowitz, J.-P.Jouannaud, Rewrite Systems, Technical Report 478, LRI, Université de Paris Sud, April 1989 and Chapter 15 of Volume B of Handbook of Theoretical Computer Science, North-Holland, 1989.

[26] N.Dershowitz, J.-P.Jouannaud, Notations for Rewriting, Rapport de Recherche 478, LRI, Université de Paris Sud, January 1990.

[27] N.Dershowitz, A Maximal-Literal Unit Strategy for Horn Clauses, to appear in M.Okada, S.Kaplan (eds.), Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990.

[28] F.Fages, Associative-commutative unification, in R.Shostak (ed.), Proceedings of the Seventh International Conference on Automated Deduction, Napa Valley, CA, USA, 1984, Springer Verlag, Lecture Notes in Computer Science 170, 1984.

[29] L.Fribourg, A Strong Restriction to the Inductive Completion Procedure, in Proceedins of the Thirteenth International Conference on Automata Languages and Programming, Rennes, France, July 1986, Springer Verlag, Lecture Notes in Computer Science 226, 1986.

[30] J.A.Goguen, How to prove algebraic inductive hypotheses without induction, in W.Bibel and R.Kowalski (eds.), Proceedings of the Fifth International Conference on Automated Deduction, 356–373, Les Arcs, France, 1980, Springer Verlag, Lecture Notes in Computer Science 87, 1980.

[31] J.Hsiang, N.Dershowitz, Rewrite Methods for Clausal and Nonclausal Theorem Proving, in Proceedings of the Tenth International Conference on Automata, Languages and Programming, Barcelona, Spain, July 1983, Springer Verlag, Lecture Notes in Computer Science 154, 1983.

[32] J.Hsiang, Refutational Theorem Proving Using Term Rewriting Systems, Artificial Intelligence, Vol. 25, 255–300, 1985.

[33] J.Hsiang, M.Rusinowitch, A New Method for Establishing Refutational Completeness in Theorem Proving, in J.Siekmann (ed.), Proceedings of the Eighth Conference on Automated Deduction, Oxford, England, July 1986, Springer Verlag, Lecture Notes in Computer Science 230, 141–152, 1986.

[34] J.Hsiang, Rewrite Method for Theorem Proving in First Order Theories with Equality, Journal of Symbolic Computation, Vol. 3, 133–151, 1987.

[35] J.Hsiang, M.Rusinowitch, On word problems in equational theories, in Th.Ottman (ed.), Proceedings of the Fourteenth International Conference on Automata, Languages and Programming, Karlsruhe, West Germany, July 1987, Springer Verlag, Lecture Notes in Computer Science 267, 54–71, 1987.

[36] J.Hsiang, M.Rusinowitch and K. Sakai, Complete Inference Rules for the Cancellation Laws, in Proceedings of the Tenth International Joint Conference on Artificial Intelligence, Milano, Italy, August 1987, 990–992, 1987.

[37] J.Hsiang, M.Rusinowitch, Proving Refutational Completeness of Theorem Proving Strategies: the Transfinite Semantic Tree Method, to appear in Journal of the ACM, 1990.

[38] G.Huet, Confluent reductions: abstract properties and applications to term rewriting systems, Journal of the ACM, Vol. 27, 797–821, 1980.

[39] G.Huet, A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm, Journal of Computer and System Sciences, Vol. 23, 11–21, 1981.

[40] G.Huet, J.M.Hullot, Proofs by Induction in Equational Theories with Constructors, Journal of Computer and System Sciences, Vol. 25, 239–266, 1982.

[41] J.-P.Jouannaud, C.Kirchner, Completion of a set of rules modulo a set of equations, SIAM Journal of Computing, Vol. 15, 1155–1194, November 1986.

[42] J.-P.Jouannaud, E.Kounalis, Proofs by induction in equational theories without constructors, in Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, 358–366, Cambridge, MA, June 1986.

[43] J.-P.Jouannaud, E.Kounalis, Automatic proofs by induction in equational theories without constructors, Information and Computation, 1989.

[44] J.-P.Jouannaud, C.Kirchner, Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification, Rapport de Recherche, LRI, Université de Paris Sud, November 1989.

[45] S.Kamin, J.-J.Lévy, Two generalizations of the recursive path ordering, Unpublished note, Department of Computer Science, University of Illinois, Urbana, Illinois, February 1980.

[46] D.Kapur and P.Narendran, An equational approach to theorem proving in first order predicate calculus, in Proceedings of the Ninth International Joint Conference on Artificial Intelligence, 1146–1153, Los Angeles, CA, August 1985.

[47] D.Kapur and D.R.Musser, Proof by consistency, Artificial Intelligence, Vol. 31, No. 2, 125– 157, February 1987.

[48] D.Kapur, P.Narendran and H.Zhang, Proof by induction using test sets, in J.Siekmann (ed.), Proceedings of the Eighth Conference on Automated Deduction, Oxford, England, July 1986, Springer Verlag, Lecture Notes in Computer Science 230, 99–117, 1986.

[49] D.E.Knuth, P.Bendix, Simple Word Problems in Universal Algebras, in J.Leech (ed.), Proceedings of the Conference on Computational Problems in Abstract Algebras, Oxford, England, 1967, Pergamon Press, Oxford, 263–298, 1970.

[50] E.Kounalis, M.Rusinowitch, On Word Problems in Horn Theories, in E.Lusk, R.Overbeek (eds.), Proceedings of the Ninth International Conference on Automated Deduction, 527– 537, Argonne, Illinois, May 1988, Springer Verlag, Lecture Notes in Computer Science 310, 1988.

[51] D.S.Lankford, Canonical inference, Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX, May 1975.

[52] D.S.Lankford, A simple explanation of inductionless induction, Technical report MTP-14, Mathematics Department, Louisiana Technical University, Ruston, LA, 1981.

[53] D.Musser, On proving inductive properties of abstract data types, in Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, 154–162, Las Vegas, Nevada, 1980.

[54] G.E.Peterson, M.E.Stickel, Complete sets of reductions for some equational theories, Journal of the ACM, Vol. 28, No. 2, 233–264, 1981.

[55] G.E.Peterson, A Technique for Establishing Completeness Results in Theorem proving with Equality, SIAM Journal of Computing, Vol. 12, No. 1, 82–100, 1983.

[56] D.A.Plaisted, Semantic confluence tests and completion methods, Information and Control, Vol. 65, 182–215, 1985.

[57] M.Rusinowitch, Theorem-proving with resolution and superposition: an extension of Knuth and Bendix procedure as a complete set of inference rules, Thèse d’Etat, Université de Nancy, 1987.

[58] M.E.Stickel, Unification Algorithms for Artificial Intelligence Languages, Ph.D. thesis, Carnegie Mellon University, 1976.

[59] M.E.Stickel, A unification algorithm for associative-commutative functions, Journal of the ACM, Vol. 28, No. 3, 423–434, 1981.

[60] H.Zhang, D.Kapur, First Order Theorem Proving Using Conditional Rewrite RUles, in E.Lusk, R.Overbeek (eds.), Proceedings of the Ninth International Conference on Automated Deduction, 1–20, Argonne, Illinois, May 1988, Springer Verlag, Lecture Notes in Computer Science 310, 1988.