MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Ordered Chaining Calculi for First-Order Theories of Binary Relations

Leo Bachmair Harald Ganzinger

MPI–I–95–2–009 October 1995

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Authors’ Addresses

Leo Bachmair  Harald Ganzinger
Department of Computer Science  Max-Planck-Institut für Informatik
SUNY at Stony Brook  Im Stadtwald
Stony Brook, NY 11794, U.S.A.  D-66123 Saarbrücken, Germany

           leo@sbcs.sunysb.edu                     hg@mpi-sb.mpg.de

                                            http://www.mpi-sb.mpg.de/~hg/

Publication Notes

This paper has been submitted for publication elsewhere and will be copyrighted, if accepted.

Acknowledgements

This research was supported in part by the German Science Foundation (Deutsche Forschungsgemeinschaft) under grant Ga 261/4-1, by the German Ministry for Research and Technology (Bundesministerium für Forschung und Technologie) under grant ITS 9102/ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics). The first author was also supported by the Alexander von Humboldt Foundation.

Abstract

We propose inference systems for binary relations with composition laws of the form S ∘ T ⊆ U in the context of resolution-type theorem proving. Particulary interesting examples include transitivity, partial orderings, equality and the combination of equality with other transitive relations. Our inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods. We establish their refutational completeness and also prove their compatibility with the usual simplification techniques used in rewrite-based theorem provers. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. We demonstrate that rewrite techniques considerably restrict variable chaining, though we also show that they cannot be completely avoided in general. If a binary relation under consideration satisfies additional properties, such as symmetry, further restrictions are possible. In particular, we discuss orderings and partial congruence relations.

Keywords

Automated Theorem Proving, First-Order Logic, Transitive Relations, Chaining, Orderings, Rewrite Techniques, Simplification

Contents

1 Introduction 2

2 Preliminaries 3

3 Transitive Relations 4 3.1 Commutation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Negative chaining . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

3.2.1 Admissible Clause Orderings . . . . . . . . . . . . . . . . . . . . 6 3.2.2 Inferences of Ordered Chaining . . . . . . . . . . . . . . . . . . . 7

3.3 Refutational Completeness for Horn Clauses . . . . . . . . . . . . . . . . 8 3.4 Variable chaining . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

4 General Binary Relations 11 4.1 Composition Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.2 Redundancy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.3 Ordered Chaining for General Composition Laws . . . . . . . . . . . . . 15 4.4 Refutational Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . 17

5 Partial Congruences 19 5.1 Replacement Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.2 The Many-Sorted Case . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.3 The Subterm Chaining Calculus . . . . . . . . . . . . . . . . . . . . . . 23 5.4 Lifting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 5.5 Refutational Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.6 Superposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 5.7 Monotonicity and Anti-Monotonicity . . . . . . . . . . . . . . . . . . . . 29

6 Total Orderings 30 6.1 Treating Irreflexivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6.2 Treating Totality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6.3 Ordered Chaining for Total Orderings . . . . . . . . . . . . . . . . . . . 34 6.4 A Refined Clause Ordering . . . . . . . . . . . . . . . . . . . . . . . . . 34 6.5 Non-strict Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 6.6 Variable Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

7 Conclusions 39

1 Introduction

Rewrite techniques, as exemplified by completion procedures, have been successfully applied to many problems in equational theorem proving. The theoretical foundation of completion is the use of rewrite rules, guided by well-founded syntactic orderings, in such a way that certain commutation properties are satisfied. Building ordered rewriting into an inference system, through the concept of rewrite proofs, forward reasoning (search) is effectively restricted and combined with don’t-care nondeterministic backward reasoning (simplification). The explicit generation of the congruence closure of a set of equations is usually avoided. This is one main advantage of rewrite techniques over methods based on resolution alone. From a practical point of view the simplification techniques afforded by rewriting are even more important. In the context of automated theorem proving, rewrite techniques have been typically applied to equivalence relations. In this paper we investigate their application to arbitrary (e.g., non-symmetric) transitive relations and design corresponding inference systems for first-order theories with transitive relations, using resolution as the underlying inference mechanism.

Resolution, in its different variants, forms the core of many current automated reasoning systems. (For a recent exposition of the theory of resolution see Bachmair and Ganzinger 1995b.) By and large such resolution refinements as hyper-resolution, ordered resolution, or the set-of-support strategy are quite useful in practice, but for logical theories with transitive relations, such as logics with equality or inequality relations, they are not very effective. Special techniques have been devised for such theories: chaining and variable elimination for inequalities, and paramodulation, which can be thought of as a form of subterm chaining, for equality. Chaining essentially encodes certain resolution steps with the transitivity axiom. For example, if S is a transitive relation, chaining allows one to derive uσ S vσ from u S s and t S v, where σ is a most general unifier of s and t. The completeness of this inference mechanism follows immediately from the completeness of resolution with selection (Bachmair and Ganzinger 1994b).

We propose the following refinement of chaining: first compare the term sσ (which is identical to tσ) to both uσ and vσ (using a given well-founded ordering on terms) and perform the chaining inference only if sσ is maximal. This form of “ordered chaining” can be viewed as an application of standard rewrite techniques. More precisely, we argue that it corresponds to a completion process, aimed at deriving enough rewrite rules so that the given transitive relation can be described by corresponding rewrite proofs. The completeness of ordered chaining is based on a suitable commutation property of the rewrite relations involved which is achieved through completion. In formalizing this approach we use standard methods from the theory of term rewriting. However, we wish to apply this approach not only to unit clauses, as is the case with standard completion procedures, but to general clauses, and therefore have to integrate the notion of rewriting in this more general context. This is relatively straightforward for Horn clauses, but more difficult in the case of disjunctions of positive literals, due to the additional degree of non-determinism in the rewrite relations and certain subtle dependencies between them. We will discuss the two cases separately.

The practicality of chaining methods crucially depends on the extent to which a particularly prolific form of chaining, called variable chaining (where s or t is a variable), can be restricted. Ordered chaining considerably cuts down the number of possible variable chainings, as the required maximality condition for terms can only be satisfied if the variable is unshielded, i.e., occurs only as an argument of the predicate S, but not as an argument of a function symbol or any other predicate symbol. However, we also show that some variable chainings are needed for transitive relations in general, though further restriction are possible if additional properties such as symmetry are satisfied. For instance, in the case of equivalence relations we obtain calculi in which chaining “into” a variable is not needed.

Transitivity is a particular instance of a composition law for binary relations of the form S ∘ T ⊆ U. The chaining techniques in this paper will be applicable to a large class of such composition laws. In order to introduce the main ideas in a way that does not require much technical detail, we will first, in Section 3, describe our methods for the particularly simple case of Horn clauses over one transitive relation. In Section 4 the methods will be extended to composition laws in general and to full firstorder clauses. Refutational completeness is established for an appropriately extended inference system and in the presence of a notion of redundancy that covers the usual simplification techniques used in rewrite-based theorem provers. Redundancy is the central concept when tailoring the general system to particulary interesting cases of binary relations. Each case will be investigated with the goal to further optimize the inference system and to avoid variable chaining as much as possible. In particular we consider (partial) equivalence and congruence relations in Section 5.1 and total orderings in Section 6; and conclude with a summary and suggestions for further research.

This paper combines results that we have annonced in (Bachmair and Ganzinger 1994a) and (Bachmair and Ganzinger 1994c) into a single framework with a uniform and complete presentation.

2 Preliminaries

We consider first-order languages with function symbols, predicate symbols, and variables. A term is an expression f(t_{1}, …, t_{n}) or x, where f is a function symbol of arity n, x is a variable, and t_{1}, …, t_{n} are terms. An atomic formula (or simply atom) is an expression P (t_{1}, …, t_{n}), where P is a predicate symbol of arity n and t_{1}, …, t_{n} are terms. A literal is an expression A (a positive literal) or ¬A (a negative literal), where A is an atomic formula. Atoms from binary predicate symbols S are often written in infix notation as u S v. A clause is a finite multiset of literals. We write a clause by listing its literals, ¬A_{1}, …, ¬A_{m}, B_{1}, …, B_{n}; or as a disjunction ¬A_{1} ∨ ⋯ ∨ ¬A_{m} ∨ B_{1} ⋯ ∨ B_{n}; or as a sequent A_{1}, …, A_{m} → B_{1}, …, B_{n}. An expression is said to be ground if it contains no variables.

By a (Herbrand) interpretation we mean a set I of ground atomic formulas. We say that an atom A is true (and ¬A, false) in I if A ∈ I; and that A is false (and ¬A, true) in I if A ∉ I. A ground clause is true in an interpretation I if at least one of its literals is true in I; and is false otherwise. In general, a clause is said to be true in I if all its ground instances are true. The empty clause is false in every interpretation. We say that I is a model of a set of clauses N (or that N is satisfied by I) if all elements of N are true in I. Occasionally, a model of N will also be called an N-interpretation. A set N is satisfiable if it has a model, and unsatisfiable otherwise. For instance, any set containing the empty clause is unsatisfiable.

3 Transitive Relations

In this section we will consider the satisfiability problem for sets of Horn clauses in languages with transitive relations, that is, predicates S that satisfy

x S y , y S z → x S z.

Such clauses present difficulties for resolution-based provers. A transitivity axiom can be resolved with itself to yield a new clause

x S y_{1} , y_{1} S y_{2} , y_{2} S z → x S z

that can again be resolved with the original clause, to yield

x S y_{1} , y_{1} S y_{2} , y_{2} S y_{3} , y_{3} S z → x S z

and so on. Certain refinements of resolution provide better control in this regard. For instance, the self-resolution that is problematic with transitivity, is automatically excluded by resolution with selection (Bachmair and Ganzinger 1994b): if we select the two negative literals in the transitivity axiom, the only kind of inference in which it can participate are inferences of the form

\frac{C , u S s D , t S v ¬(x S y), ¬(y S z), x S z}{Cσ , Dσ , uσ S vσ}

where σ is a most general unifier of s and t. The key here is that it is never necessary to resolve with the non-selected (i.e., positive) literal of the transitivity axiom (for details, see Bachmair and Ganzinger 1995b). Therefore we may encode transitivity as an inference rule:

Chaining:

\frac{C , u S s D , t S v}{Cσ , Dσ , uσ S vσ}

where σ is a most general unifier of s and t.

Unfortunately, the chaining rule, which was already proposed by Slagle (1972), is not completely satisfactory, as it explicitly generates the transitive closure of the binary relation described by S. For example, if a S b and b S c and c S d are given, chaining will generate the additional unit clauses a S c and b S d and a S d.

We will next outline how standard rewrite techniques can be used in this context to more effectively restrict the chaining rule. Rewrite systems provide for a more compact representation of transitive (closures of) relations and are one of the more efficient techniques for reasoning about chains of terms, such as a S b S c S d in the above example. Rewrite techniques have typically been applied to equivalence and congruence relations. We also discuss non-symmetric relations, developing an approach similar in spirit to what has been called bi-rewriting by Levy and Agustí (1993).

3.1 Commutation

If S is a binary relation, we denote by S^{−1} its inverse, by S^{+} its transitive closure, and by S^{∗} its reflexive-transitive closure. (A binary relation S is called reflexive if xSx for all x; irreflexive if xSx for no x; and non-reflexive if it is not reflexive.) The composition of two binary relations S and T is denoted by S ∘ T. (x, y) is in S ∘ T if and only if there exists a z such that (x, z) is in S and (z, y) is in T. Our objective is to represent transitive (closures of) relations by means of well-founded rewrite relations.^{1} Two relations S_{1} and S_{2} are employed for that purpose.

We say that S_{1} commutes with S_{2} if S_{2} ∘ S_{1} ⊆ (S_{1}^{+} ∘ S_{2}^{∗}) ∪ S_{2}^{+}.^{2}

Proposition 1 If S_{1} ∪ S_{2}^{−1} is a well-founded binary relation and S_{1} commutes with S_{2}, then the two relations (S_{1} ∪ S_{2})^{+} and (S_{1}^{+} ∘ S_{2}^{∗}) ∪ S_{2}^{+} are identical.

The proposition can be proved with standard methods from rewriting theory.^{3} It provides the starting point for our investigations.

Let ≻ be a (strict) ordering and ⪰ be its reflexive closure. We denote by ⇒_{S} the intersection of S with ≻; by ⇐_{S} the intersection of S with the inverse ≺ of the relation ≻; and by ⇔_{S} the reflexive part of S, that is, the intersection of S with the identity relation. If the ordering ≻ is total, then S = ⇔_{S} ∪ ⇒_{S} ∪ ⇐_{S}. We drop the subscript when the relation is known from the context. Slightly adapting Proposition 1, we obtain:

Proposition 2 Let S be a binary relation and ≻ be a well-founded ordering that is total on the given domain. If the relation ⇒_{S} ∪ ⇔_{S} commutes with ⇐_{S} ∪ ⇔_{S} then S^{+} = ⇔_{S} ∪ (⇒_{S}^{+} ∘ ⇐_{S}^{∗}) ∪ ⇐_{S}^{+}.

This result shows that under suitable commutation properties the non-reflexive part of a transitive relation can be described by a certain kind of rewrite proofs with ⇒ and ⇐.

In the logic context a relation is often represented by ground atoms in a Herbrand interpretation I. To simplify matters technically, for the remainder of this section we shall assume that S is the only predicate symbol, and that it denotes a transitive relation. If I satisfies the transitivity law T_{S} for S then I is called a transitivity interpretation. If I is a Herbrand interpretation, that is, a set of ground atoms (for S), and if ≻ is a wellfounded ordering on ground atoms, by analogy with the notation used before, we shall write ⇒_{I}, ⇐_{I}, and ⇔_{I}, respectively, to denote the intersection of S (as defined by I) with the relations ≻, ≺, and =. A rewrite proof of u S v in I is either of the form

u ⇔_{I} u,

provided u = v, or else is a non-empty sequence of rewrites

u = u_{0} ⇒_{I} ⋯ ⇒_{I} u_{m} = v_{n} ⇐_{I} ⋯ ⇐_{I} v_{0} = v,

where m + n ≥ 1. We write u ⇓_{I} v when there exists a rewrite proof for u S v in I. A sequence u ⇐_{I} t ⇒_{I} v, on the other hand, is called a peak. The peak is said to commute if u ⇓_{I} v. By a plateau we mean a sequence of rewrites t ⇔_{I} t ⇒_{I} v or u ⇐_{I} t ⇔_{I} t. Any plateau can be transformed into a rewrite proof by simply deleting the ⇔-step. A sequence of rewrites is a rewrite proof if and only if it contains no peak and no plateau as a subsequence.

By the rewrite closure of I we mean the set {u S v : u ⇓_{I} v}. As a consequence of Proposition 2 we obtain:

1The relations we talk about are abstract reduction systems in the sense of Klop (1992), but not necessarily rewrite relations in the sense of Dershowitz and Jouannaud (1990), in that they need not be closed under context application.

2The relation (S_{1}^{+} ∘ S_{2}^{∗}) ∪ S_{2}^{+} is identical to (S_{1}^{+} ∘ S_{2}^{∗}) ∪ (S_{1}^{∗} ∘ S_{2}^{+}).

3Commutation properties, with a view to their application to termination problems, have been discussed in Bachmair and Dershowitz 1986, Bellegarde and Lescanne 1987, Geser 1991.

Proposition 3 Let ≻ be well-founded and total on ground terms. The rewrite closure of I is a transitivity interpretation if and only if all peaks in I commute.

For example, if I contains the atoms a S b and b S c and c S d, and if a ≻ b ≻ c ≻ d, then a ⇒_{I} b and b ⇒_{I} c and c ⇒_{I} d. The relation ⇒_{I} evidently commutes with the (empty) relation ⇐_{I}. If we choose the ordering b ≻ c ≻ d ≻ a, the rewrite steps are a ⇐_{I} b and b ⇒_{I} c and c ⇒_{I} d, and there is a peak, a ⇐_{I} b ⇒_{I} c, that does not commute. If, through ordered chaining, we generate a S c, the corresponding rewrite step a ⇐ c makes the peak converge. Chaining with suitable ordering restrictions provides the basis for a completion process of which equational completion is a special case in which the two rewrite relations ⇒ and ⇐^{−1} are the same, cf., Section 5.1. Completion always succeeds for finite (ground) I. Equational completion procedures, such as ordered completion or conditional completion, have been described by inference rules, e.g., Bachmair, Dershowitz and Plaisted 1989, Ganzinger 1991, Dershowitz 1991. We will devise similar (refutationally complete) inference systems for transitive relations in general.

One important difference between a convergent rewrite system in the equational case and commutation of one rewrite system over another in the case of a non-symmetric relation S exists, though. A convergent system admits unique normal forms. Searching for a rewrite proof for a given pair of ground terms is don’t-care nondeterministic in that no backtracking is required. Commutation is weaker in this regard. In general one may have more than one “minimal” rewrite proof for any two given terms, and there may be no deterministic strategy of finding anyone of them.

3.2 Negative chaining

Having computed sufficiently many consequences by ordered chaining, for negative literals in clauses we need to enumerate their rewrite proofs. Take the above example and add another clause ¬(a S d) ∨ d S e. By transitivity we have a S d, which we may resolve with the additional clause to obtain d S e. However, with ordered chaining, we do not derive a S d directly, but only obtain enough inequalities for a suitable rewrite proof of a S d. We need an inference mechanism which solves negative inequalities and, as a side effect, generates enough inequalities for a rewrite proof of d S e. In the equational case, negative literals in clauses are solved by narrowing-like inferences which enumerate equational rewrite proofs. In the general case of a transitive relation, the corresponding inference mechanism will be called negative chaining.

3.2.1 Admissible Clause Orderings

We combine the chaining rules into an ordered resolution calculus, and for that purpose have to require an ordering on terms, literals and clauses. A well-founded and total ordering ≻ on ground terms and ground literals is called admissible if it is compatible with a certain complexity measure c_{L} on ground literals L. By compatibility we mean that whenever c_{L} ≻ c_{L′} then L ≻ L′, for any two ground literals L and L′. Throughout this paper we will use several such complexity measures, any of which will be a refinement of some previously defined measure. Results which are obtained for admissible orderings then also apply to orderings that are compatible with the refined measure.

For the purpose of this section, the following complexity measure will suffice: Suppose L is of the form u S v or ¬(u S v). Then c_{L} = (max_{L}, p_{L}, s_{L}), where (i) max_{L} denotes the maximal term of u and v with respect to ≻; (ii) p_{L} is 1, if L is negative, and 0 otherwise; and (iii) s_{L} is 1 if u ⪰ v, and 0 otherwise. We assume that the lexicographic combination of ≻ on terms with 1 > 0 is used to compare the complexity triples. For example, if s ≻ t, then the complexity of s S t is (s, 0, 1), whereas the complexity of ¬(t S s) is (s, 1, 0). The maximal term of a literal is the main criterion for any admissible literal ordering. Rewriting the maximal term into a smaller term will always yield a smaller literal. We observe that a negative literal is considered more complex than a positive literal with the same maximal term. Moreover we have stipulated that the argument terms of an atom be lexicographically compared.

An ordering on ground clauses is called admissible if it is the multiset extension of an admissible ordering ≻ on literals. We will also use ≻ to denote the clause ordering. We assume that orderings on ground expressions are extended to non-ground expressions as follows: E ≻ E′ if and only if Eσ ≻ E′σ, for all ground instances Eσ and E′σ. Thus, we have E ⪰̸ E′ if E′σ ≻ Eσ, for some ground instances Eσ and E′σ.^{4} We say that a literal L is maximal with respect to a clause C if L′ ≻ L, for no literal L′ in C; and that L is strictly maximal with respect to C if L′ ⪰ L, for no L′ in C. Given an admissible ordering on terms and literals, its extension to an admissible ordering on clauses is uniquely defined by the above stipulations.

A great variety of admissible literal and clause orderings exists for arbitrary signatures of function symbols.^{5} Selecting an appropriate such ordering is one of the most important ways in which one can take an influence on the search strategy of a prover that is based on rewriting methods. Defining selection strategies for negative literals is the second major high-level primitive for guiding search. In this paper we will not consider selection. It is not hard to see that the results about selection in the equational case (Bachmair and Ganzinger 1994b) can be extended to the framework that we consider in this paper. The calculi that we present here will not include selection so as to not further complicate matters technically.

3.2.2 Inferences of Ordered Chaining

We are now prepared for defining the inference rules of a chaining calculus.^{6} We assume ≻ to denote some admissible ordering on terms, literals and clauses.

Ordered Chaining:

\frac{C , u S s D , t S v}{Cσ , Dσ , uσ S vσ}

where (i) σ is the most general unifier of s and t, (ii) uσ S sσ is strictly maximal with respect to Cσ, (iii) tσ S vσ is strictly maximal with respect to Dσ, (iv) uσ ⪰̸ sσ, and (v) vσ ⪰̸ tσ.

Negative Chaining:

\frac{C , ¬(u S s) D , t S v}{Cσ , Dσ , ¬(vσ S σ)}

4Depending on the ordering, this extension to non-ground expressions may or may not be decidable.

In the latter case one will have to employ a safe and decidable approximation.

5For a survey on orderings see Dershowitz (1987).

6As usual we implicitly assume that the premises of an inference have no common variables. If necessary, the variables in one premise are renamed. Thus, it is also possible to use different variants of a clause as premises in one inference.

where (i) σ is the most general unifier of u and t, (ii) ¬(uσ S sσ) is maximal with respect to Cσ, (iii) tσ S vσ is strictly maximal with respect to Dσ, (iv) vσ ⪰̸ tσ, (v) sσ ⪰̸ uσ, and (vi) sσ ≠ vσ; and

\frac{C , ¬(u S s) D , t S v}{Cσ , Dσ , ¬(uσ S tσ)}

where (i) σ is the most general unifier of s and v, (ii) ¬(uσ S sσ) is maximal with respect to Cσ, (iii) tσ S vσ is strictly maximal with respect to Dσ, (iv) uσ ⊁ sσ,^{7} (v) tσ ⪰̸ vσ, and (vi) uσ ≠ tσ.

The resolution rule takes care of one-step rewrite proofs for negative literals:

Ordered Resolution:

\frac{C , A D , ¬B}{Cσ , Dσ}

where (i) σ is the most general unifier of A and B, (ii) Aσ is strictly maximal with respect to Cσ, and (iii) Bσ is maximal in Dσ.

The calculus of all these inference rules is denoted by B_{S}, or simply B (the Basic chaining calculus).

3.3 Refutational Completeness for Horn Clauses

Clauses with at most one positive literal are called Horn clauses. The calculi B_{S} are refutationally complete for such clauses. For the completeness proof we adapt the model construction approach of Bachmair and Ganzinger (1990) (see also Bachmair and Ganzinger 1994b).

Given a set N of ground clauses, we define a corresponding Herbrand interpretation I using induction on ≻. More precisely, we define for each clause C an interpretation I_{C}, intended to be a model for clauses smaller than C, and a set E_{C} that is designed to turn I_{C} into a model of C as well. Since ordered chaining is supposed to achieve that atoms can be proved by rewrite proofs, the partial interpretations I_{C}, as well as the final I, will be represented as the rewrite closures of suitable sets R_{C} and R.

Formally, for every clause C in N we define R_{C} to be the set ⋃_{C≻D} E_{D}. By I_{C} we denote the rewrite closure of R_{C}. Furthermore, if C is a clause C′ ∨ A, where A is a positive literal and A ≻ C′,^{8} and C is false in I_{C} then E_{C} = {A}. In that case, we also say that C is productive and that it produces A. In all other cases, E_{C} = ∅. Finally, let R be ⋃_{C} E_{C} and let I be the rewrite closure of R.

In what follows we shall also use the notation R^{C} for R_{C} ∪ E_{C} and I^{C} for the rewrite closure of R^{C}. Hence I_{C} is the partial interpretation defined by clauses smaller that C, whereas I^{C} additionally includes the effect of C in this construction. All these interpretations are rewrite closures of suitable rule sets so that an atom is true if and only if it has a rewrite proof in the corresponding rule set.

The following lemma expresses an important monotonicity property of our construction:

Lemma 1 If a ground clause C (which need not be in N) is true in some interpretation I_{D} or I^{D}, where D ⪰ C, then C is also true in I and in any interpretation I_{D′} and I^{D′} with D′ ≻ D. Furthermore, if a clause C is productive, then it is true in I^{C}.

7The case uσ = sσ needs to be dealt with by only one of the forms of negative chaining.

8In writing A ≻ C′ we view A to denote a positive unit clause.

Proof. The proof is straightforward and based on the following observations: Atoms which are true in some partial interpretation I_{D} or I^{D} remain true in any “later” interpretation I_{D′} or I^{D′} with D′ ≻ D, as the rule sets of which these rewrite closures are formed increase monotonically. Compatible orderings ≻ on literals are designed so that whenever a negative literal ¬A occurs in C and A is false in I_{D} or I^{D} with D ∈ N and D ⪰ C, then A remains false in I. If such an atom A is false in I_{D} or I^{D} then A has no rewrite proof in rules generated “up to D”. If D ⪰ C, rules that are generated into later interpretations I_{D′} have too large “left-hand sides” to be able to reduce A. □

This lemma will often be applied in its contrapositive form to infer that C is false in I_{C} and I^{C} whenever it is false in I_{D′} or I^{D′}, for some D′ ≻ C.

The next lemma states a continuity property of the model construction.

Lemma 2 Let D be a clause in N and let C be a ground clause (which need not be in N). If C is true in all interpretations I^{D′} with D ≻ D′, then C is also true in I_{D}.

Proof. If a ground atom A is true in I_{C} then has a rewrite proof over R_{C}, hence is true in I^{D′} where D′ ≺ C is the clause that produces the largest atom that occurs in the proof of A. Therefore, if the antecedent of C is true in I_{C}, it is already true in some such I^{D′}. In this case the succedent of C is true in I^{D′} and in I_{C}. □

The model construction given above is a rather general concept. It is parametrized by the notion of a rewrite closure (and hence of a rewrite proof). Although in this section we consider Horn clauses only, the construction is independent of that property. Later on we shall refine our inference systems and extend them to full clauses. In these contexts, the respective notions of a rewrite proof will be correspondingly refined, but the model construction per se will remain the same. It is important to note that the two basic properties of the construction as stated in the Lemmas 1 and 2 will hold for any of the notions of rewriting that we consider in this paper.

We say that a set of (possibly non-ground) clauses N is saturated (with respect to an inference system J) if it contains all conclusions of inferences (in J) from N.

Lemma 3 Let N be a set of ground Horn clauses that is saturated with respect to B and does not contain the empty clause, and let I be the interpretation constructed from N. Then for every clause C in N we have:

(1) If C is a productive clause C′ ∨ A, with A ≻ C′, then C′ is false in I.

(2) I^{C} as well as I_{C} are transitivity interpretations.

(3) C is true in I^{C}.

Proof. We use induction on ≻. Let C be a ground clause in N, such that (1)–(3) are satisfied for all smaller clauses in N.

(1) Suppose C is a productive clause of the form C′ ∨ A, with A ≻ C′. Since C is a Horn clause, C′ contains only negative literals. Furthermore, C is false in I_{C}. Thus, if ¬B is a literal in C′, then B ∈ I_{C} ⊆ I, from which we conclude that C′ is false in I.

(2) According to Proposition 3 we have to prove that all peaks u ⇐ v ⇒ t in I^{C} commute. By the induction hypothesis, peaks from any two rules in R_{C} commute, hence I_{C} is a transitivity interpretation. The assertion for I^{C} is thus trivially true if E_{C} is empty, or if E_{C} = {t S v} where v ⪰ t. (If v ≻ t, the bigger term occurs on the right side of the inequation. Clauses producing atoms of the form v S u in which the maximal term occurs on the left side cannot be smaller than C with respect to ≻.) Suppose C = C′ ∨ v S t produces v S t with v ≻ t. If there is another clause D = D′ ∨ u S v that produces uSv with v ≻ u, then there exists a peak u ⇐ v ⇒ t in I^{C}. Now consider ordered chaining by which the clause C′′ = C′ ∨ D′ ∨ u S t can be obtained from C and D. Since N is saturated and C ≻ C′′ we may apply the induction hypothesis for (3), to infer that C′′ is true in I^{C′′}. But C′ ∨ D′ is false in I and R^{C′′} ⊆ R_{C}, hence u ⇓_{R_{C}} t. This establishes the required commutation property.

(3) If C is false in I^{C}, then it cannot be productive, hence must violate the condition imposed on productive clauses, that is, the maximal literal in C is negative. Let us therefore assume C can be written as C′ ∨ ¬A, with a maximal atom ¬A that is false in I_{C}. Thus the atom A is true in I_{C}. If A is produced by some (smaller) clause D = D′ ∨ A, then the resolvent C′′ = D′ ∨ C′ of C and D is smaller than C (since ¬A ≻ D′), contained in N, and, as a consequence of (i), false in I_{C} and hence false in I^{C′′}—which contradicts the induction hypothesis. The only remaining possibility is that A is an atom u S v with u ⇓_{R_{C}} v. In that case there exists a suitable productive clause D ∨ u S v′ (where v′ ⇓_{R_{C}} v) or D ∨ u′ S v (where u ⇓_{R_{C}} u′) which, through negative chaining with C, produces a clause C′′ smaller than C that is contained in N and is false in I^{C′′}, which is again a contradiction. Thus, C must be true in I^{C}, which completes the proof. □

The lemma indicates that all interpretation I_{C} and I are transitivity interpretations. As an immediate corollary of the lemma we obtain:

Theorem 1 If a set of Horn clauses N is saturated with respect to B_{S}, then the set N ∪ T_{S} is unsatisfiable if and only if it contains the empty clause.

Proof. If N contains the empty clause, N ∪ T_{S} is unsatisfiable. Suppose N does not contain the empty clause. Let I be the Herbrand interpretation constructed from the set of all ground instances of N. It follows from standard results in resolution theory (usually called “lifting lemmas”) that if N is saturated with respect to B, then the set of its ground instances is also saturated. Therefore we may use the above lemma to infer that the relation ⇓_{R} is transitive and that I is a model of N ∪ T_{S}. □

We can use this theorem to check the unsatisfiability of sets of Horn clauses over languages with transitive relations: saturate the given set of clauses with respect to the inference system B by applying the inferences in B exhaustively; if the set if unsatisfiable, a contradiction in the form of the empty clause will eventually be generated. In the following section we generalize the ordered chaining calculus B to non-Horn clauses and to forms of composition laws for binary relations which are more general than transitivity. Before, though, we take a first look at the problem of variable chaining.

3.4 Variable chaining

In chaining we combine two inequalities (one of which may be negative) by unifying the first argument of one with the second argument of the other. If one of the two terms thus unified is a variable we speak of a variable chaining. More specifically, we speak of chaining into a variable if the inequality with the variable is not smaller (with respect to ≻) than the other inequality; and speak of chaining from a variable if the inequality with the variable is not bigger than the other inequality. Since the unification of a term with a variable not occurring in it always succeeds, variable chaining can be particularly prolific. Fortunately, the combination of certain redundancy criteria (to be defined and proved compatible with chaining below) and ordering constraints drastically cuts down on variable chaining.

Consider, for instance, an inference

\frac{C , u S x D , t S v}{Cσ , D , uσ S v}

where xσ = t. The constraints imposed on an ordered chaining inference require x to be a maximal term in the first premise, which implies that x does not occur in a negative literal and also is unshielded in the clause in the sense that it occurs only as an argument of S but not as an argument of any other predicate symbol or any function symbol. Moreover, the inference is redundant if the variable x is linear in the first premise, i.e., does not occur in C or u. For in that case the conclusion is C ∨ D ∨ u S v, and is either properly subsumed by C ∨ u S x or else is identical to C ∨ u S x up to renaming of variables. Similar arguments apply to inferences

\frac{C , u S s D , x S v}{C , Dσ , u S vσ}

where the variable occurs as the first argument of an S atom.

In sum, ordered chaining through a variable is only necessary if the variable is nonlinear, unshielded, and occurs only in positive literals. For Horn clauses these conditions cannot be satisfied simultaneously, so that ordered chaining through variables is not needed at all. But negative chaining into non-linear unshielded variables is still necessary, even for Horn clauses, as the following example shows. Take the set of clauses

→ a S a′
→ a′ S c
→ b S b′
→ b′ S c
a S x, b S x →

where c ≻ b′ ≻ b ≻ a′ ≻ a. This set of clauses is unsatisfiable. From the first two clauses we obtain a S c; from the third and fourth clause b S c. The two inequalities contradict the last clause. No ordered chaining is possible. We may resolve the third with the last clause, to get ¬(a S b′), from which we get ¬(a S b) by chaining with the third clause again. Any other inferences require chaining through a variable. In other words, no contradiction can be derived if we exclude variable chaining. If we use the fourth and fifth clause to chain through a variable, we get ¬(a S c) ∨ ¬(b S b′), from which a contradiction can be derived by one more chaining and two resolution steps.

In sections 5.4 and 6.6 we show that chaining into variables can be avoided if the given transitive relation is a partial congruence, or else if it is a dense, total ordering without endpoints.

4 General Binary Relations

We now generalize the results of the previous section to (i) full clauses, (ii) a more general form of composition laws for binary relations (to be defined in Section 4.1), and (iii) to a suitable concept of redundancy which will be defined in Section 4.2 and that will be compatible with chaining. The completeness results will be valid for a large class of variants of inference systems, differing in how they exploit additional logical properties of relations by specialized derived inferences that make other, less specialized inferences redundant.

4.1 Composition Laws

Transitivity is a special case of a composition law for binary relations. For a generalized chaining we assume a set Co of composition laws (or composition axioms) of the form

x S y , y T z → x U z

where S, T, and U are binary relations. We will also write S ∘ T ⊆ U in this case. We assume that composition of relations as defined by the laws in Co is associative, that is, whenever we have two laws S ∘ T ⊆ U and U ∘ V ⊆ W, then we must also have laws of the form T ∘ V ⊆ V′ and S ∘ V′ ⊆ W, and vice versa. In that case the consequences of Co, they have the form S_{1} ∘ S_{2} … ∘ S_{n} ⊆ S, do not depend on the order in which the basic laws are applied. To simplify the technical treatment we require in addition that in each law S ∘ T ⊆ U either U = S or U = T. A relation symbol that occurs in a composition law is called a special (binary) relation.

Example. The clauses

x < y , y < z → x < z
x ≈ y , y ≈ z → x ≈ z
x ≤ y , y ≤ z → x ≤ z
x ≈ y , y < z → x < z
x < y , y ≈ z → x < z
x ≈ y , y ≤ z → x ≤ z
x ≤ y , y ≈ z → x ≤ z
x < y , y ≤ z → x < z
x ≤ y , y < z → x < z

define the composition laws for a strict and non-strict ordering < and ≤, respectively, together with equality ≈. □

We assume again that ≻ denotes a given well-founded and total ordering on ground terms. Let I be a set of ground atoms and, for any binary relation S, let ⇒_{I}^{S}, and ⇐_{I}^{S}, and ⇔_{I}^{S}, respectively, denote the intersection of the binary relation S as represented by the set of S-atoms in I with ≻, ≺, and =. Generalizing the notions of Section 3.2, a proof of u S v in I is a sequence of the form

u = u_{0}S_{1}u_{1} S_{2} u_{2} … u_{n−1} S_{n} u_{n} = v

where n ≥ 1, the u_{i}S_{i}u_{I+1} are in I, and S_{1} ∘ S_{2} … ∘ S_{n} ⊆ S follows from Co. The proof is called a rewrite proof if it is of the form

u = u_{0} ⇒_{I}^{S_{1}} u_{1} … u_{k−1} ⇒_{I}^{S_{k}} u_{k} ⇐_{I}^{S_{k+1}} u_{k+1} … u_{n−1} ⇐_{I}^{S_{n}} u_{n} = v

or of the form

u=u_{0} ⇒_{I}^{S_{1}} u_{1} … u_{k−2} ⇒_{I}^{S_{k−1}} u_{k−1} ⇔_{I}^{S_{k}} u_{k} ⇐_{I}^{S_{k+1}} u_{k+1} … u_{n−1} ⇐_{I}^{S_{n}} u_{n} =v

with 1 ≤ k ≤ n. The existence of a rewrite proof for u S v in I will be indicated by the notation u ⇓_{I}^{S} v. The rewrite closure of I consists of I and the set of all atoms u S v that have a rewrite proof in I.

A proof u ⇐_{I}^{R} s ⇒_{I}^{S} t of u T t is called a peak. A proof u ⇐_{I}^{R} t ⇔_{I}^{S} t or u ⇔_{I}^{R} u ⇒_{I}^{S} t of u T t is called a plateau. The peak or plateau is said to be convergent, if there exists a rewrite proof of u T t in I. I is said to be complete if all peaks and plateaus in I converge. A straightforward generalization of Proposition 3 is the following completeness criterion:

Proposition 4 The following three properties are equivalent:

(i) I is complete.

(ii) Any ground atom which follows from I and Co has a rewrite proof in I.

(iii) The rewrite closure of I satisfies Co.

Proof. We prove that (i) implies (ii), the other implications being trivial. Proofs which are not rewrite proofs will be transformed into smaller proofs where the proof ordering is the multiset extension of ≻ applied to the terms that occur in the proof. The transformations will be of a local nature which is made possible by the associativity of the composition laws.

Let I commute and let u = u_{0} S_{1} u_{1} S_{2} u_{2} … u_{n−1} S_{n} u_{n} = v be a proof of u S v in I. If n = 1 the proof is a rewrite proof. If n > 1 and if the proof is not a rewrite proof then it contains a subproof of the form w U s V t, with s ⪰ w, s ⪰ t, and U ∘ V ⊆ T is in Co, with either T = U or T = V. If the subproof is a peak or plateau, we may replace it by a rewrite proof for w T t in I which, according to the assumption, exists. Otherwise s = t = w. In that case one of the two steps is of the form s T s, and we may simply delete the other. The new proof proves u S v and is smaller than the given proof. □

This proof entirely follows standard methods. We have given it in detail to indicate where we make use of the the fact that in composition laws the relation on the right side must be one of the operand relations of the left side. To relax that restriction one will have to treat the reflexive parts of relations more specifically.

From now on we also consider symmetry axioms

x R y → y R x

for special relations and in that case call R symmetric. Symmetry will be built into the notation in that we assume that an atomic expression s R t denotes both s R t and t R s. We require that if U is symmetric and S ∘T ⊆ U then both S and T are also symmetric. We use L to denote the union of the composition and symmetry laws.

Subsequently we restrict ourselves to the case where all predicate symbols are binary. Any other atom p(t_{1}, …, t_{n}) can be represented (in a many-sorted framework) by an equivalence p(t_{1}, …, t_{n}) ≡ ⊤ where ≡ is an equivalence relation (cf. section 5.1 for more details). Equivalence relations will be investigated more specifically in section 5.

4.2 Redundancy

We sketch the main ideas of an abstract notion of redundancy and refer to Bachmair and Ganzinger (1994b) for further details. Let N and S be sets of clauses and C be a ground clause (not necessarily a ground instance of N). Our intention is to specify when C is not needed for proving the potential inconsistency of N ∪ S. S will usually refer to clauses, such as the composition laws, which are built into the chaining inference system.

Redundancy is a notion which exploits certain properties of our model construction, hence depends on the given clause ordering. For the refined chaining calculus we need to refine the complexity measure c_{L} for literals L to become compatible with symmetry: If L is a ground literal A or ¬A, with A an atom of the form u S v, then c_{L} = (max_{L}, p_{L}, s_{L}) where (i) max_{L} is the maximal term among u and v; (ii) p_{L} is 1, if L is negative, and 0 otherwise; and (iii) s_{L} is 1 if S is not symmetric and if u ⪰ v, and s_{L} is 0, otherwise.

Again, an admissible ordering on ground clauses is the multiset extension of an admissible (with respect to the refined complexity measure) literal ordering, and we use ≻ to denote both the term and literal ordering as well as its multiset extension to an ordering on clauses.

From the proof of the Lemma 3 we observe that inferences were only required when they involve ground clauses C that are false in I_{C} and in situations where one could assume that all smaller clauses are true in I_{C}. The following definition of redundancy for clauses approximates these properties without making any explicit reference to the model construction. We call C S-redundant with respect to N if there exist ground instances C_{1}, …, C_{k} of N such that C is true in every S-model of C_{1}, …, C_{k} and C ≻ C_{j}, for all j with 1 ≤ j ≤ k. It can easily be seen that the clauses C_{1}, …, C_{k} can be assumed to be non-redundant. Clearly, if the C_{i} are true in I_{C}, C cannot be false in I_{C}, provided I_{C} satisfies S. A non-ground clause is called S-redundant if all its ground instances are.

Tautologies are S-redundant in this sense, for any S, and most cases of proper subsumption are also covered by this notion of redundancy. The axioms in S are all S-redundant by definition.

Further inspection of the proof of Lemma 3 reveals that, for binary inferences, the first premise is always a productive clause C. Its maximal literal A is strictly maximal, positive, and gets produced into I^{C}. While the ordering constraints for productivity are captured with the ordering constraints for the inferences, the fact that A is true in I^{C} will be reflected by the subsequent definition of redundancy for inferences. To that end, we call the maximal atom of the first premise of a binary inference the main atom of the inference. For other types of inferences, the main atom is defined to be ⊤. With these preliminaries, a ground inference with conclusion B, maximal premise C, and main atom A is called S-redundant with respect to N if either some premise is redundant, or else there exist ground instances C_{1}, …, C_{k} of N such that B is true in every S-model of A, C_{1}, …, C_{k}, and C ≻ C_{j}, for all j with 1 ≤ j ≤ k. A non-ground inference is called S-redundant if all its ground instances (that satisfy the associated restrictions) are redundant.

We say that a set of clauses N is saturated up to S-redundancy with respect to some inference system, if all inferences from N are S-redundant. For the remainder of this paper “redundancy” is meant to refer to L-redundancy whenever the concrete set of built-in axioms L is clear from the context.

For inference systems in which the first premise of a binary ground inference is smaller than the second, the the definition of redundancy given here is equivalent to notions of redundancy that we have proposed in previous work (Bachmair and Ganzinger 1990, Bachmair and Ganzinger 1994b). With the present definition we may admit larger classes of clause orderings.

For a refutationally complete inference system we expect that if N is saturated up to redundancy then N is unsatisfiable if and only if the empty clause is in N. That leaves us with the problem of how to effectively saturate a set of clauses. If the system is monotone in the sense that the conclusion of any ground inference is smaller than the maximal premise of the inference, then one way to render an inference redundant is to add its conclusion to N. Given a recursive and monotone inference system, for any recursively enumerable set of clauses an equivalent and saturated set can be recursively enumerated. The inference systems that we present below will usually not be monotone for arbitrarily chosen admissible clause orderings. However, in all cases it will not be difficult, when supplied with any admissible term ordering, to extend it to an admissible clause ordering for which the inferences are monotone.

4.3 Ordered Chaining for General Composition Laws

The inference system below represents a generalization of ordered chaining to general composition laws and to the case of general clauses. We assume an admissible ordering ≻ to be given.

Ordered Chaining:

\frac{C , u S s D , t T v}{Cσ , Dσ , uσ U vσ}

where (i) S ∘ T ⊆ U is in Co; (ii) σ is the most general unifier of s and t; (iii) uσ S sσ is strictly maximal with respect to Cσ; (iv) tσ T vσ is strictly maximal with respect to Dσ; (v) uσ ⪰̸ sσ, and uσ ≠ sσ if U = T; and (vi) vσ ⪰̸ tσ, and tσ ≠ vσ if U = S.

Negative Chaining:

\frac{C , ¬(u S s) D , t T v}{Cσ , Dσ , ¬(vσ U sσ)}

where (i) T ∘ U ⊆ S is in Co; (ii) σ is the most general unifier of u and t; (iii) ¬(uσ S sσ) is maximal with respect to Cσ; (iv) tσ T vσ is strictly maximal with respect to Dσ; (v) vσ ⪰̸ tσ, and (vi) sσ ⪰̸ uσ; and

\frac{C , ¬(u S s) D , t T v}{Cσ , Dσ , ¬(uσ U tσ)}

where (i) U ∘ T ⊆ S is in Co; (ii) σ is the most general unifier of s and v; (iii) ¬(uσ S sσ) is maximal with respect to Cσ; (iv) tσ T vσ is strictly maximal with respect to Dσ; (v) uσ ⊁ sσ, and (vi) tσ ⪰̸ vσ.

Ordered Resolution:

\frac{C , A D , ¬B}{Cσ , Dσ}

where (i) σ is the most general unifier of A and B; (ii) Aσ is strictly maximal with respect to Cσ; and (iii) Bσ is maximal with respect to Dσ.

Ordered Factoring:

\frac{C , A, B}{Cσ , Aσ}

where (i) σ is the most general unifier of A and B; and (ii) Aσ is maximal with respect to Cσ.

Unfortunately, it also turns out that for disjunctions of binary atoms with multiple occurrences of the maximal term of a clause the inference mechanism of negative and ordered chaining is insufficient. For example, take the set of clauses

\begin{aligned}(1) & & → & c ≤ b \\ (2) & & → & b ≤ c \\ (3) & & → & a ≤ b, a ≤ c \\ (4) & a ≤ b, a ≤ c & → \end{aligned}

where ≤ is transitive and a ≻ b ≻ c. This set of clauses is unsatisfiable. The third clause implies that a ≤ b or a ≤ c is true. But by the first two clauses, if one of the two inequalities is true, so is the other. This contradicts the last clause. From the first two clauses we obtain c ≤ c by chaining. From the last two clauses we obtain a≰ c ∨ a ≤ c by ordered resolution. This inference is redundant, as its conclusion is a tautology. Thus, by adding c ≤ c the set is saturated up to redundancy, but does not contain the empty clause.

The following inference rules restore refutational completeness and guarantee compatibility with redundancy.

Composition Resolution:

\frac{C , u V v , u′ U v′ D , s S t}{Dσ , ¬(tσ T v′σ), u′σ U v′σ}

where (i) S ∘ T ⊆ U is in Co; (ii) σ is the most general unifier of u, u′ and s; (iii) the literal uσ V vσ is strictly maximal with respect to Cσ ∨ u′σ U v′σ; (iv) the literal sσ S tσ is strictly maximal with respect to Dσ; and (v) vσ ⊁ uσ, v′σ ⊁ uσ, tσ ⪰̸ sσ, u′σ U v′σ ⪰̸ uσ V vσ and uσ V vσ ⊁ sσ S tσ.

\frac{C , u V v , u′ U v′ D , s S t}{Dσ , ¬(u′σ T sσ), u′σ U v′σ}

where (i) T ∘ S ⊆ U is in Co; (ii) σ is the most general unifier of v, v′ and t; (iii) the literal uσ V vσ is strictly maximal with respect to Cσ ∨ u′σ U v′σ; (iv) the literal sσ S tσ is strictly maximal with respect to Dσ; and (v) uσ ⊁ vσ, u′σ ⊁ vσ, sσ ⪰̸ tσ, u′σ U v′σ ⪰̸ uσ V vσ and uσ V vσ ⊁ sσ S tσ.

In the above example, the third clause resolves with itself by composition resolution yielding

(5)  b ≤ c → a ≤ c

Now the refutation proceeds by:

(6)  b ≤ c, c ≤ b, a ≤ c →  [neg. chaining of (5) into (3)]
(7) b ≤ c, b ≤ c, c ≤ b, c ≤ c →  [neg. chaining of (5) into (6)]
(8)  c ≤ c →  [resolution of (1) & (2) with (7)]
(9)  → c ≤ c  [chaining of (1) and (2)]
(10)  →  [resolution of (8) with (9)]

Composition resolution represents the controlled application of resolution with the composition laws. For instance, consider the case of a transitive relation S. The clause Dσ ∨ ¬(tσ S v′σ) ∨ sσ S v′σ is an instance of the conclusion of the resolution inference

\frac{Dσ , sσ S tσ ¬(x S y), ¬(y S z), xSz}{Dσ , ¬(tσ S z), sσ S z}

In other words, the conclusion of a composition resolution inference π is an instance of a resolvent between the second premise of π and a composition law in Co. The first premise of π (that is, the existence of a clause C , u S v , u′ S v′ with σ = mgu(s, u, u′) in the example) regulates which instances and resolvents are needed. We shall later see that in the presence of additional logical properties (eg., symmetry or totality) this inference can be drastically simplified.

The calculus of all these inference rules is denoted by C_{L}^{≻}, or simply C^{≻} or C. The soundness of the inferences can be checked easily.

It is not difficult to construct admissible clause orderings for which C^{≻} is monotone. Let ≻ be some total and well-founded ordering on ground terms. Suppose that we extend the complexity triples c_{L} for ground literals L to quadrupels c_{L} = (max_{L}, p_{L}, s_{L}, d_{L}) where the additional component d_{L} is 1 if the maximal term of L occurs twice in L, and 0, otherwise. Then any total, well-founded ordering ≻ on literals compatible with c_{L} and its multiset extension to clauses will do.

Lemma 4 Let ≻ be of the above form. Then C is monotone.

Proof. The lemma follows by straightforward inspection of the various cases. Consider, for instance, a ground instance of (the first variant of) composition resolution. It has the form

\frac{C , s V v , s U v′ D , s S t}{D , ¬(t T v′), s U v′}

where s V v is strictly maximal in C ∨ s S v′; the literal s S t is strictly maximal in D; and s ⪰ v, s ⪰ v′, s ≻ t, and (s S t) ⪰ (s V v) ≻ (s U v′). From the new component d_{L} in the literal ordering and as U is not symmetric we may infer that (s S t) ≻ (s U v′) is impossible if s = v′. Hence s ≻ v′ and therefore (s V v) ≻ ¬(t T v′). The conclusion is therefore smaller than the second premise. □

4.4 Refutational Completeness

Referring to the model construction of Section 3.3., we first state the main lemma.

Lemma 5 Let N be a set of clauses that is saturated up to redundancy with respect to C^{≻} and does not contain the empty clause. Furthermore, let I be the interpretation constructed from the ground instances of N according to ≻. Then for every ground instance C of a clause in N we have:

1. If C is productive then it is non-redundant.

2. If D is a clause D′ ∨ A which produces A and if D ⪯ C then D′ is false in I^{C}.

3. I_{C} as well as I^{C} satisfy L.

4. The clause C is true in I^{C}.

Proof. We use induction on ≻. Let C be a ground instance of N such that (1)–(4) are satisfied for all smaller ground instances of N.

(1) Let C be L-redundant in N. Then there exist ground instances C_{1}, …, C_{n} of N such that C logically follows from the C_{i}, that is, is true in every L-model of the C_{i}. Applying the induction hypothesis of (3) and (4) we infer that I_{C} is an L-model of the C_{i}. Therefore C is true in I_{C} and, hence, not productive.

(2) Suppose D is a productive clause of the form D′ ∨ A with A ≻ D′ and C ⪰ D. We prove, by means of induction, that D′ is false in I^{C′}, for any clause C ⪰ C′ ⪰ D. As induction hypothesis we may assume that D′ is false in I_{C′}. (This is easily confirmed for the base case C′ = D.) Suppose D′ is true in the rewrite closure of R^{C′}. Let s be the maximal term in D. If ¬B is a negative literal in D′ then B is true in I_{C′} and hence true in I^{C′}. If B is a positive literal in D′ then B is false in I_{C′}, and hence does not have a rewrite proof in R_{C′}. If s does not occur in B then C′ cannot produce an atom that would be applicable in a rewite proof of B, hence B is false in I^{C′}. There are two remaining cases to be considered. One is that C′ is of the form C′′ ∨ s S t and produces s S t with s ⪰ t; and moreover A is an atom s V v and D′ is of the form D′′ ∨ s U v′, such that s U v′ can be proved by a rewrite proof consisting of s S t, followed by a rewrite proof for some t T v′ in R_{C′}, with S ∘ T ⊆ U. Hence s ≻ t. As both C′ and D are productive, by (1) they are not redundant. Since N is saturated up to redundancy, the clause Ĉ = C′′ ∨ ¬(t T v′) ∨ s U v′ that is obtained by composition resolution from D and C′ follows from A and from instances of N which are smaller than C′. A, as well as, by induction hypothesis for (4), the C_{i}, are true in I_{C′}, and we may infer that Ĉ is true in I_{C′}. Also, since C′ is productive, C′′ is false in I_{C′}. Therefore, s U v′ must be true in I_{C′}. This contradicts our assumption that D′ is false in I_{C′}. The other, similar case that C′ is of the form C′′ ∨ s S t and produces s S t with t ≻ s, corresponds to the other version of composition resolution. Details are left to the reader.

(3) By Proposition 4 we have to show that both R_{C} and R^{C} are complete. By the induction hypothesis, peaks and plateaus that involve only R_{C} converge. The assertion for I^{C} is thus trivially true if E_{C} is empty, or if E_{C} = {t T v} where v ≻ t and T is not symmetric. Suppose C = C′ ∨ v T t (modulo the potential symmetry of T) produces v T t with v ≻ t. By the definition of E_{C}, the clause C′ is false in I_{C}. If there is another clause D = D′ ∨ u S v with C ≻ D that produces u S v with v ≻ u, and S ∘ T ⊆ U, then u ⇐^{S} v ⇒^{T} t is a peak in I^{C}. (If v = u and S = U then u ⇔^{S} v ⇒^{T} t is a plateau in I^{C}.) Since C ≻ D we may apply (2) to conclude that D′ is also false in I_{C}. Furthermore, C and D are by (1) non-redundant and produce C′′ = C′ ∨ D′ ∨ u U t by ordered chaining. Since N is saturated up to redundancy, the clause C′′ must logically follow from u S v and from clauses strictly smaller than C. That is, C′′ must be true in I_{C}, but C′ ∨ D′ is false in I_{C}. Therefore u U t is true in I_{C}, hence u ⇓_{I_{C}}^{U} t, which establishes the required commutation property. If C = C′ ∨ v T v produces v T v then there might be a plateau in I^{C} due to the existence of a clause D ≺ C producing an atom u S v [or v S u], with v ≻ u. That u U v [v U u] is true in I_{C} is proved in a similar way.

(4) We already know that all ground instances of N that are smaller than C are true in I_{C} and that I_{C} is a model L. If C is redundant, then it has to be true in I_{C} and in hence in I^{C}. If C is productive, it is by construction true in the rewrite closure of R^{C}. Let C be a non-redundant, non-productive clause.

(4.1) First suppose the maximal literal in C is negative and C can be written as C′ ∨ ¬A, with a maximal atom A that is true in I_{C}.

If A is produced by some (smaller) clause D = D′ ∨ A, then the resolvent C′′ = D′ ∨ C′ of C and D is smaller than C (since ¬A ≻ D′). Since N is saturated up to redundancy, C′′ must follow from clauses smaller than C, all of which are true in I_{C}. Therefore C′′ must be true in I_{C}. By (2), D′ is false in I_{C}. Therefore C′, and also C, is true in I_{C}.

If A is a binary atom u U v with a rewrite proof u ⇓_{R_{C}}^{U} v of length ≥ 2, then there exists a suitable productive clause D′ ∨ u S v′ (where v′ ⇓_{R_{C}}^{T} v) or D′ ∨ u′ T v (where u ⇓_{R_{C}}^{S} u′) and S ∘ T ⊆ U. By negative chaining we get either C′ ∨ D′ ∨ ¬(v′ T v) or C′ ∨ D′ ∨ ¬(u S u′). In either case we may use saturation up to redundancy to infer that C′, and hence C, is true in I_{C}.

(4.2) If C is of the form C′ ∨ A ∨ A, with multiple occurrences of the maximal literal A, then the smaller clause C′ ∨ A is obtained from C by ordered factoring. Using the induction hypothesis and saturation up to redundancy, we may infer that C′ ∨ A and C must be true in I_{C}.

Cases (4.1) and (4.2) cover all the possibilities for a non-redundant clause C to be non-productive. In each case we have shown C to be true in I_{C}, which completes this case. □

As an immediate corollary of the above lemma we obtain the following completeness theorem.

Theorem 2 If a set of clauses N is saturated up to redundancy with respect to C_{L}, then the set N ∪ L is unsatisfiable if and only if it contains the empty clause.

5 Partial Congruences

5.1 Replacement Axioms

In this section we look at replacement axioms of the form

x S y, P [x] → P [y]

which express that whenever x S y then P remains true if we replace the indicated occurrence of x in P by y. For example, if S is equality then this law is valid for arbitrary formulas P and occurrences x. Our intention is to represent this operational meaning in a chaining calculus in which chaining through subterms such as x in P [x] is performed in the presence of binary atoms such as x S y. The main problem with subterm chaining is that in general we cannot avoid chaining below variables. For example, if we have the axioms

x < y, y + z < u → x + z < u
x < y, z + y < u → z + x < u

expressing the monotonicity of an operation + in both arguments with respect to <, then, given inequations 3 < 5 and x+y < y+17, we would have to infer that x+(u+3) < (u + 5) + 17 where this inequation is obtained by chaining with 3 < 5 below the variable y in the second inequation, instantiating it by u + 5. This problem is discussed in more detail in Section 5.7. Chaining below variables is unfeasable in practice, and nothing is gained compared to a strategy by which monotonicity axioms are treated unspecifically just like any other clause. We will develop subterm chaining only for a class of binary relations for which variable overlaps are generally redundant. These relations will have to be symmetric, in particular. Orderings are not symmetric and hence the results of this paper will not allow to treat monotonicity laws for orderings by subterm chaining.

The relations that we will be able to handle are partial congruences. These are partial equivalences which in addition allow the replacement of equals by equals in arbitrary contexts. A partial equivalence ≡ is a binary relation which is symmetric, transitive and satisfies ≡ ∘ S ⊆ S and S ∘ ≡ ⊆ S, for any other binary relation S. A partial equivalence need not be reflexive. Reflexivity properties may, for instance, be inferred through the implication

x ∼ y → x ∼ x

which is a consequence of transitivity and symmetry. We call a term defined with respect to ∼ if t ∼ t can be derived, and the set of all defined ground terms is called the domain of the partial equivalence.

A partial congruence ∼ is a symmetric relation satisfying the replacement axiom

x ∼ y, A[x] → A[y]

for any atom A and any occurrence of x in A. Partial congruences are special cases of partial equivalences. A partial congruence need not satisfy any of the monotonicity laws

x ∼ y → f(… x …) ∼ f(… y …).

Monotonicity (together with symmetry and transitivity) implies replacement, but not vice versa.

Partial congruences are useful for axiomatizing partial functions. They occur in Scott’s logic of partial equality (Scott 1979) and also in type theory where t ≈_{T} t in a type T can be proven only if t is provably a member of T.

Example. A specification of natural numbers with a partial predecessor function might for instance be given as follows:

nat(x) ↔ x ∼ x
→ nat(0)
nat(x) ↔ nat(s(x))
0 ∼ s(x) →
nat(x) → p(s(x)) ∼ x
nat(p(x)) → s(p(x)) ∼ x

The undefinedness of p(0) is represented by the fact that ¬nat(p(0)) can be derived as a theorem. □

An example of a partial congruence for which the replacement axioms can be represented finitely (for finite signatures) is equality for strict partial functions:

Example.

x ∼ y → y ∼ x
x ∼ y , y ∼ z → x ∼ z
f(x_{1}, …, x_{n}) ∼ f(x_{1}, …, x_{n}) → x_{i} ∼ x_{i}, for any f and position i
x_{i} ∼ y_{i} , f(… x_{i} …) ∼ z → f(… y_{i} …) ∼ z, for any f and i

It is easy to see that these axioms in fact imply the replacement axioms. The third axiom (scheme) specifies strictness of all functions. □

Congruences ≈ are partial congruences which are reflexive. The replacement laws are then equivalent to the monotonicity laws

x ≈ y → f(… x …) ≈ f(… y …), for any function f.

together with reflexivity, symmetry and transitivity. Hence, if the signature is finite we again have a finite representation of the replacement laws. Note, however, that for the subsequent exposition of chaining finiteness of the representation of the replacement axioms is inessential.

Example. The clauses

x < y , y < z → x < z
x ≈ x
x ≈ y → y ≈ x
x ≈ y , y ≈ z → x ≈ z
x ≈ y → f(… x …) ≈ f(… y …), for any function f.
x ≤ y , y ≤ z → x ≤ z
x ≈ y , y < z → x < z
x < y , y ≈ z → x < z
x ≈ y , y ≤ z → x ≤ z
x ≤ y , y ≈ z → x ≤ z
x < y , y ≤ z → x < z
x ≤ y , y < z → x < z
x < x →

express the basic properties of equality and of and a strict and a non-strict inequality. The subterm chaining calculus to be presented below will be able to handle them implicitly. No explicit inferences from these axioms will be needed for refutational completeness. □

In a single-sorted framework any two partial congruences must be identical on the intersection of their domains. To simplify the technical presentation we will therefore assume that we have just one partial congruence ∼ in addition to equality ≈. ≈ is in particular the reflexive closure of ∼. We write ≡ to denote ∼ or ≈ and call atoms of the form s ≡ t equalites. We also write s ≢ t for negative equalities ¬ s ≡ t. We assume that the composition laws ≡ ∘ S ⊆ S and S ∘ ≡ ⊆ S, for any S, are contained in Co, and that Co does not contain any other composition laws involving ∼ and ≈. We also assume that the symmetry laws for ∼ and ≈ are in Sy. By L we again denote the set of all laws that we intend to built into the inference system, that is, the union of Co and Sy, together with the replacement axioms for ∼ and ≈ and the reflexivity axiom for ≈.

We extend our previous notion of a proof from Section 4.1. Let I be a set of ground atoms. Remember that symmetry is built into the notation. A proof in I is now a sequence of the form

u = u_{0} S^{0}|_{p_{0}} u_{1} S^{1}|_{p_{1}} u_{2} … u_{n−1} S^{n−1}|_{p_{n−1}} u_{n} = v

where n ≥ 0, and for each 0 ≤ i < n there exists v_{i}S_{i}v_{i+1} in I such that u_{i}|_{p_{i}} = v_{i}, u_{i+1} = u_{i}[v_{i+1}]_{p_{i}} and p_{i} is the root in u_{i} if S_{i} is different from ∼ and ≈. For each i, p_{i} denotes the term position at which the atom from I that is used in the i-th proof step is applied. Subsequently we will omit positions from the notation for proofs whenever they are irrelevant. The proof is said to prove u ≈ v if n = 0 (and u = v) or else if n > 0 and each S_{i} is either ∼ or ≈. The proof additionally proves u S v if S^{1} ∘ S^{2} ∘ … ∘ S^{n} ⊆ S follows from Co and if there exists at least one 0 ≤ i < n such that p_{i} is the root position in u_{i} and S_{i} is different from ≈. For example if a ∼ b and f(a) ≈ f(c) are in I then f(c) ≈ f(a) ∼ f(b) is a proof of f(c) ≈ f(b) but it is not a proof of f(c) ∼ f(b). On the other hand, if a ≈ b and f(a) ∼ f(c) are in I then f(c) ∼ f(a) ≈ f(b) is a proof of both f(c) ∼ f(b) and f(c) ≈ f(b).

Proposition 5 Let I be a set of ground atoms and let u and v be ground terms. Then u S v follows from I and L if and only if there exists a proof of u S v in I.

The characteristic properties of a rewrite proof (relative to a given well-founded ordering ≻ which is total on ground terms) are as before. More precisely, a proof of the above form is a rewrite proof if n = 0, or else if n = 1, u = v and S^{1} = ∼, or else if n ≥ 1 and

u = u_{0} ≻ … ≻ u_{k} ⪯ u_{k+1} ≺ … ≺ u_{n} = v.

Additionally we require for a rewrite proof that S^{k} be different from ≡ if n > 0 and u_{k} = u_{k+1}. then S^{k} is different from ≡. The rewrite closure of I consists of I and the set of all atoms u S v that have a rewrite proof in I. For an S-step in a rewrite proof over I we shall again use the notations s ⇒_{I}^{S} t, s ⇐_{I}^{S} t, or s ⇔_{I}^{S} t, depending on whether s ≻ t, s ≺ t or s = t, respectively. More refined notations such as u[s]_{p} ⇒_{I}^{≡} u[t]_{p} are used for denoting equality steps whenever the rewrite position needs to be explicitly indicated.

As before, a proof u ⇐_{I}^{R} s ⇒_{I}^{S} t of u T t is called a peak, and a proof u ⇐_{I}^{R} t ⇔_{I}^{S} t or u ⇔_{I}^{R} u ⇒_{I}^{S} t of u T t is called a plateau in I. The peak or plateau is said to be convergent, if there exists a rewrite proof of u T t in I. I is said to be complete if all peaks and plateaus in I converge.

Proposition 6 Then following three properties are equivalent:

(i) I is complete.

(ii) Any ground atom which follows from I and L has a rewrite proof in I.

(iii) The rewrite closure of I satisfies L.

For obtaining a workable inference system of ordered subterm chaining, we have to place additional restrictions on the term ordering. The ordering has to be stable under contexts, i.e., should be a rewrite relation. A rewrite relation is a binary relation ≻ on terms such that s ≻ t implies u[sσ] ≻ u[tσ], for all terms u and substitutions σ. A reduction ordering is a well-founded rewrite relation. From now on ≻ will always denote a complete reduction ordering, i.e., a reduction ordering that is total on ground terms.

A peak u[s]_{p} ⇐^{R} u[t]_{p} = u[s′]_{q} ⇒^{S} u[t′]_{q} is called critical if p or q is the root position. A plateau u[s]_{p} ⇔^{R} u[s]_{p} = u[s′]_{q} ⇒^{S} u[t′]_{q} or u[s]_{q} ⇐^{R} u[t]_{q} = u[s′]_{p} ⇔^{S} u[s′]_{p} is called a critial if p is the root position and if R is different from ≈.

Proposition 7 I is complete if and only if all critical peaks and plateaus commute.

5.2 The Many-Sorted Case

Throughout this paper we assume a single-sorted framework with at most one partial congruence (in addition to equality). The extension the case of many-sorted signatures and arbitrary families of partial congruences is a simple exercise that we leave to the reader. In practice a many-sorted framework is desirable. In that context one may want to have a (partial) congruence on each sort. The following example in particular justifies a posteriori why we can safely restrict ourselves to consider binary relations only. Non-binary atoms can be easily modelled in a two-sorted signature with sorts prop for (atomic) propositions for predicate symbols that are no special binary relations, and a sort o for objects. Function symbols are of type o^{n} → o and non-special predicate symbols are of type o^{n} → prop. ≈ denotes equality on o and ↔ denotes equality on prop. In the following clauses, x, y and z range over o, whereas p, q, r range over prop.

x ≈ x
x ≈ y → y ≈ x
x ≈ y , y ≈ z → x ≈ z
x ≈ y → F (… x …) ≈ F (… y …), for any function F
x ≈ y → P (… x …) ↔ P (… y …), for any predicate P
p ↔ p
p ↔ q → q ↔ p
p ↔ q , q ↔ r → p ↔ r

With these axioms in L a user may actually write clauses in which equivalences between propositions occur on literal position in clauses. An example of such an “extended” clause would be

P (x) ↔ Q(s(x)) → P (p(x)) ↔ Q(x).

In general, ordered chaining for ↔-atoms is ordered rewriting with equivalences. Orientable equivalences can be used for simplification of atoms by reduction in the same way as one uses orientable equations for the simplification of terms. A (minimal) constant ⊤ : prop can be introduced to express truth of an atom P (t_{1}, …, t_{n}) by writing an equivalence P (t_{1}, …, t_{n}) ↔ ⊤. Negative ordered chaining between to equivalences P ↔ ⊤ corresponds to ordered resolution while positive chaining yields tautologies of the form C ∨ (⊤ ↔ ⊤) which are redundant.

5.3 The Subterm Chaining Calculus

Let ≻ be a complete reduction ordering on terms. Once more we refine the complexity measure c_{L} for literals L, so as to accomodate for partial equivalences and congruences. If L is a ground literal A or ¬A, with A an atom of the form u S v, then c_{L} = (max_{L}, p_{L}, s_{L}), where (i) p_{L} is 1, if L is negative, and 0 otherwise; (ii) max_{L} is the maximal term of u and v; s_{L} is 0, if S is ∼ or ≈; otherwise, if S is different from ∼ and ≈, then s_{L} is 2, if u ⪰ v and S is not symmetric, and s_{L} is 1, otherwise. We observe that ≡-literals are made less complex than other literals with the same maximal term. That will have the effect that equalities are defined at an earlier stage in the model construction. An admissible ordering on ground clauses is the multiset extension of an admissible ordering on literals (based on the refined complexity measure), and the extensions to non-ground expressions is as above.

Ordered Subterm Chaining:

\frac{C , u S s D , t [ s′]_{p}T v}{Cσ , Dσ , t[u]_{p}σ U vσ}

where (i) σ is the most general unifier of s and s′; (ii) if p is the root in t then S ∘ T ⊆ U is in Co, and if p is not the root in t then S is ≡ and U = T; (iii) uσ S sσ is strictly maximal with respect to Cσ; (iv) tσ T vσ is strictly maximal with respect to Dσ; (v) uσ ⊁ sσ, and uσ ≠ sσ if U = T or S = ≡; (vi) vσ ⊁ tσ, and tσ ≠ vσ if U = S and p is the root position; and (vii) if S is ≡, then s′ is not a variable.

Negative Subterm Chaining:

\frac{C , t T v D , ¬(u[t′]_{p} S s)}{Cσ , Dσ , ¬(u[v]_{p}σ U sσ)}

where (i) σ is the most general unifier of t and t′; (ii) if p is the root in u, then T ∘U ⊆ S is in L, and if p is not the root in u, then U = S and T is ≡; (iii) ¬(uσ S sσ) is maximal with respect to Dσ; (iv) tσ T vσ is strictly maximal with respect to Cσ; (v) vσ ⪰̸ tσ and sσ ⪰̸ uσ; and (vi) if T is ≡ then t′ is not a variable;

and

\frac{C , t T v D , ¬(u S s[v′]_{p})}{Cσ , Dσ , ¬(uσ U s[t]_{p}σ)}

where (i) σ is the most general unifier of v and v′; (ii) if p is the root in s, then U ∘T ⊆ S is in L, and if p is not the root in s, then U = S and T is ≡; (iii) ¬(uσ S sσ) is maximal with respect to Dσ; (iv) tσ T vσ is strictly maximal with respect to Cσ; (v) uσ ⊁ sσ and tσ ⪰̸ vσ; and (vi) if T is ≡ then v′ is not a variable.

Ordered Resolution:

\frac{C , u′ S v D , ¬¬(u S v)}{Cσ , Dσ}

where (i) σ is the most general unifier of u, u′, v and v′; (ii) uσ S vσ is strictly maximal with respect to Cσ; and is maximal with respect to Dσ; and (iii) S is different from ≡.

Reflexivity Resolution:

\frac{C , u ≉ v}{Cσ}

where (i) σ is the most general unifier of u and v, and (ii) uσ ≉ vσ is maximal with respect to Cσ.

Ordered Factoring:

\frac{C , A, B}{Cσ , Aσ}

where (i) σ is the most general unifier of A and B; and (ii) Aσ is maximal with respect to Cσ.

Composition Resolution: This inference is the same as above, except that it is not required when U is ≡:

\frac{C , u V v , u′ U v′ D , s S t}{Dσ , ¬(tσ T v′σ), u′σ U v′σ}

where (i) S ∘ T ⊆ U is in Co and U is not ≡; (ii) σ is the most general unifier of u, u′ and s; (iii) the literal uσ V vσ is strictly maximal with respect to Cσ ∨ u′σ U v′σ; (iv) the literal sσ S tσ is strictly maximal with respect to Dσ; and (v) vσ ⊁ uσ, v′σ ⊁ uσ, tσ ⪰̸ sσ, u′σ U v′σ ⪰̸ uσ V vσ and uσ V vσ ⊁ sσ S tσ.

\frac{C , u V v , u′ U v′ D , s S t}{Dσ , ¬(u′σ T sσ), u′σ U v′σ}

where (i) T ∘ S ⊆ U is in Co and U is not ≡; (ii) σ is the most general unifier of v, v′ and t; (iii) the literal uσ V vσ is strictly maximal with respect to Cσ ∨ u′σ U v′σ; (iv) the literal sσ S tσ is strictly maximal with respect to Dσ; and (v) uσ ⊁ vσ, u′σ ⊁ vσ, sσ ⪰̸ tσ, u′σ U v′σ ⪰̸ uσ V vσ and uσ V vσ ⊁ sσ S tσ.

Note that if U is different from ≡ neither V nor S can be ≡ if the ordering restrictions are satisfied. That is, we do not require composition resolution for partial congruences. The latter are dealt with by a specialized form of composition resolution, called equality factoring.

Equality Factoring:

\frac{C , u ≡_{1} v , u′ ≡_{2} v′}{Cσ , vσ ≢_{3} v′σ , uσ ≡_{2} v′σ}

where (i) σ is the most general unifier of u and u′; (ii) either ≡_{2} = ≡_{3} = ≈ or else ≡_{2} is ∼ and exactly one of the ≡_{1} and ≡_{3} is ∼; (iii) vσ ⪰̸ uσ, v′σ ⪰̸ uσ, and v′σ ⪰̸ vσ; and (iv) uσ ≡ vσ is strictly maximal with respect to Cσ ∨ u′σ ≡ v′σ.

Equality factoring corresponds to composition resolution of a (suitable) clause with itself.

The subterm chaining calculus will be denoted by S^{≻}, or simply S.

Remarks. Let us point out the major differences between C and S which are mainly in the treatment of negative literals. A common case of negative chaining is

\frac{C , t S v D , ¬(u S s)}{Cσ , Dσ , vσ ≉ sσ}

with σ = mgu(t, u), as ≈ ∘S ⊆ S for any relation S. If vσ and sσ are unifiable (by τ), then from the latter we may infer Cστ ∨ Dστ by reflexivity resolution. While in the system C the last step of a rewrite proof for a negative literal is always built by a step of ordered resolution, in S it is usually a trivial proof of equality. Ordered resolution now only needs to take care of inequations of the form t S t with S different from ≡. Nontrivial proofs of equality are obtained by applying facts about congruences in negative subterm chaining inferences of the form

\frac{C , a ≡ b D , w[b′] ≉ c}{Cρ, Dρ, w[a]ρ ≉ cρ} .

Consider, for instance, the two clauses

→ a ∼ b
f(a) ≈ f(b) →

with a ≻ b. The refutation of this example proceeds as follows:

f(b) ≈ f(b) →
→

with a step of negative chaining of the first clause into the second clause, followed by an application of equality resolution. Note that f(b) ≁ f(b) cannot be inferred by negative chaining into the second clause.

More Restrictions. The inference system can be further optimized by adding more restrictions to the inference rules. Certain ground inferences appear as instances of more than one type of non-ground inference, and one may want to avoid that they are computed more than once. Moreover, chaining inferences of the form

\frac{C , s ∼ u D , s ≈ v}{C , D , u ≈ v}

which are a consequence of ∼ ∘ ≈ ⊆ ≈ are redundant given the fact that in this case

\frac{C , s ∼ u D , s ≈ v}{C , D , u ∼ v}

is another instance of ordered chaining from the same premises, and ∼ ⊆ ≈ holds for any partial equivalence ∼. A dual situation arises in negative chaining.

Monotonicity of Inferences. A clause ordering for which S^{≻} is monotone can be constructed as for C, cf. Section 4.3, by adding a component d_{L} to the complexity measure for literals L that is 1 if the maximal term of L occurs twice in L, and 0, otherwise.

5.4 Lifting

Chaining into or below variables is not needed for equality:

Lemma 6 Let

\frac{C , s ≡ t D[s]_{p}}{C , D[t]_{p}}

be a ground inference by ordered or negative subterm chaining. Moreover let D be the ground instance D′σ of a clause D′ in N such that p is a position at or below a variable in D′. Then the inference is L-redundant in N.

Proof. For the inference to be ordered we have s ≻ t. Suppose D′ = D′[x]_{q} with x a variable and q a position in D′ such that p = q.q′. Suppose that xσ = s′[s]_{q′}, and let t′ = s′[t]_{q′}. Define τ to be a substitution identical to σ except that x is mapped to t′. Then D′′ = D′τ is a ground instance of N for which D ≻ D′′. D′′ and s ≡ t, together with the laws for (partial) congruences, imply D[t] and, hence, C ∨ D[t]. (In fact this is the case as partial congruences are symmetric and allow replacement of equals by equals in any context in which x may occur in D′.) Therefore the inference is L-redundant in N. □

For sake of simplicity the lemma does not explicitly refer to those cases of variable chaining with an equality s ∼ t in which, in addition to the term replacement, a negative “∼” in the second premise becomes a “≈” or a positive “≈”, respectively, becomes a “∼” in the conclusion. Theses inferences are also redundant. The proof is similar and left to the reader.

A consequence of this lemma is that any non-redundant inference from ground instances of N can be obtained as ground instance of an inference from premises in N. In other words, any non-redundant ground inference can be lifted:

Theorem 3 Let N be a set of clauses that is saturated up to redundancy with respect to S. Then the set of ground instances of N is also saturated up to redundancy with respect to S.

5.5 Refutational Completeness

With these preliminaries we apply our model construction once more to obtain the following main lemma:

Lemma 7 Let N be a set of clauses that is saturated up to L-redundancy with respect to S and does not contain the empty clause, and let I be the interpretation constructed from all ground instances of N. Then for every ground instance C of a clause in N we have:

1. If C is productive then it is not L-redundant in N.

2. If C is a clause C′ ∨ u S v (or C′ ∨ v S u) that produces u S v (or v S u) with u ⪰ v, and D ≺ C is a clause D′ ∨ s ≡ t producing s ≡ t with s ≻ t then s is different from any subterm of u.

3. If D is a clause D′ ∨ A which produces A and if D ⪯ C then D′ is false in I^{C}.

4. I^{C} satisfies L.

5. C is true in I^{C}.

Proof. We use induction on ≻. By Theorem 3 we may assume that the set of ground instances of N is saturated up to redundancy. Let C be a ground clause in N, such that (1)–(5) are satisfied for all smaller clauses in N.

(1) Let C be L-redundant in N. Then there exist ground instances C_{1}, …, C_{n} of N such that C logically follows from the C_{i}, that is, is true in every L-model of the C_{i}. Applying the induction hypothesis of (4) and (5) we infer that I_{C} is an L-model of the C_{i}. Therefore C is true in I_{C} and, hence, not productive.

(2) Suppose that C = C′ ∨ u S v produces u S v with u ⪰ v, and D ≺ C is a clause D′ ∨ s ≡ t producing the equation s ≡ t with s ≻ t. Suppose that u = u[s]. The clause C′′ = D′ ∨ C′ ∨ u[t] S′ v (with either S′ = S or else S′ = ∼, in case ≡ is ∼ and S is ≈) can be obtained by ordered chaining from C and D. By (1) neither C nor D are redundant. The set of ground instances of N is saturated, hence D′ ∨ C′ ∨ u[t] S′ v logically follows from s ≡ t and from instances of N strictly smaller than C. By induction hypothesis (5) the latter are true in I_{C}, hence C′′ is true in I_{C}. By induction hypothesis for (3), D′ is false in I_{C}. C′ is also false in I_{C}, therefore, u[t] S′ v must be true in I_{C}. This implies that u S v is true in I_{C}, hence C cannot be productive.

(3) Suppose D is a productive clause of the form D′ ∨ A with A ≻ D′ and C ⪰ D. We prove, by means of induction, that D′ is false in I^{C′}, for any clause C ⪰ C′ ⪰ D. As induction hypothesis we may assume that D′ is false in I_{C′}. (This is easily confirmed for the base case C′ = D.) Suppose D′ is true in the rewrite closure of R^{C′}. There are essentially two cases. One is that C′ is of the form C′′ ∨ s ≡ t and produces an equation s ≡ t with s ⪰ t; and moreover A is of the form s V v and D′ is of the form D′′ ∨ s U v′ [or v′ U s], such that s U v′ [v′ U s] can be proved by a rewrite proof composed by a step of s ≡ t, and a rewrite proof for some t T v′ [or v′ T t] in R_{C′}. Hence s ≻ t, which implies that s ≻ v′ and that T, U, and V are ∼ or ≈. (Otherwise C′ ⪰ D would be impossible.) Then A has to be of the form s ≡′ u with s ≻ u. By (2) we may infer that C′ = D hence t = u, ≡ = ≡′ and if U = ∼ then T or V must be ∼. Consider the clause C′′ = D′′ ∨ ¬(u T v′) ∨ s U v′ which can be obtained by equality factoring from D. As N is saturated up to redundancy and D is non-redundant, C′′ follows from instances of N strictly smaller than D, hence C′′ must be true in I_{D}. D′′ and ¬(u T v′) are, however, false in I_{D}, hence s U v′ is true in I_{D} so that D cannot be productive.

The other case in which C′ produces an inequation s S t is proved by applying composition resolution as in the proof of the corresponding statement (2) in Lemma 7. In that case, s S t cannot participate in a rewrite proof for an equation s U v′ in D′, hence composition resolution can be restriced to inequations as stated. Details are left to the reader.

(4) and (5) are proved similar to the corresponding statements in Lemma 7. □

As an immediate corollary of the above lemma we obtain the following completeness theorem.

Theorem 4 If a set of clauses N is saturated up to redundancy with respect to S_{L}, then the set N ∪ L is unsatisfiable if and only if it contains the empty clause.

5.6 Superposition

When restricted to equality ≈ as the only binary relation, the subterm chaining calculus specializes to the superposition calculus which is a restricted form of paramodulation. Ordered subterm chaining combines superposition with similar chaining inferences for other binary relations. Paramodulation was introduced by Robinson and Wos (1969), but all early completeness proofs assumed the presence of “functional-reflexive axioms” and required paramodulation into variables (i.e., chaining into variables). Brand (1975) was the first to prove that the functional-reflexive axioms are not needed, and his proof requires only a very limited form of paramodulation into a variable. The first proof that paramodulation into a variable is not needed at all was given by Peterson (1983), while Hsiang and Rusinowitch (1991) were the first to explicitly put some ordering restrictions on paramodulation. The more restrictive superposition calculus described in (Zhang and Kapur 1988, Zhang 1988) turned out to be incomplete; for a counterexample see Bachmair and Ganzinger (1990). The superposition calculus with equality factoring was introduced by Bachmair and Ganzinger (1990). There are also alternatives to equality factoring: Rusinowitch (1991) weakens some ordering constraints, while merging paramodulation is proposed in (Bachmair and Ganzinger 1990), see also (Pais and Peterson 1991). More recently new paramodulation and superposition calculi have been proposed by Bachmair, Ganzinger, Lynch and Snyder (1995b) and by Nieuwenhuis and Rubio (1992). Superposition has also been extended to support associativity and commutativity of functions symbols by Bachmair and Ganzinger (1995a), Nieuwenhuis and Rubio (1994), and Vigneron (1994).

5.7 Monotonicity and Anti-Monotonicity

The completeness results for the subterm chaining calculus are based on an application of standard rewriting techniques for treating replacement axioms in an ordered fashion. They apply to partial congruences. In practice, however, one often encounters theories with non-symmetric relations that satisfy monotonicity properties. For example, to define ordered ring structures we need axioms such as

x < y → x + z < y + z
x < y → −y < −x

that express monotonicity and anti-monotonicity, respectively, of certain functions with the (non-symmetric) ordering relation. Naturally, (subterm) chaining methods for general clauses (Manna and Waldinger 1986, Manna and Waldinger 1992) and completionlike procedures for unit clauses (Levy and Agustí 1993) have been proposed for such relations, but for completeness chaining into some of the variables of the functionalreflexive axioms (cf. the “variable instance pairs” in Bachmair, Dershowitz and Hsiang 1986) is required, which is impractical in general.

For example, given two inequalities x < x ∗ x and a < b, and a syntactic ordering in which a ≻ b and x ∗ x ≻ x, we need the “variable subterm chaining” (or “variable overlap”) a < a ∗ a < a ∗ b to derive a < a ∗ b.^{9} If < were symmetric, we would also have a rewrite proof

a ⇒^{<} b ⇐^{<} b ∗ b ⇐^{<} a ∗ b

for a < a ∗ b, and the chaining would be unnecessary. This example, which is typical of the problems variable overlaps may cause for completion procedures, depends on the syntactic ordering ≻ and on the non-linearity of the variable x.

In the case of non-unit clauses, proper handling of negative literals poses further difficulties. Take the set of two clauses

→ a < b
f(x) < f(f(y)) →

(and the monotonicity axiom x < y → f(x) < f(y)). This set of clauses is unsatisfiable: from the first clause and the monotonicity axiom we get f(f(a)) < f(f(b)), which contradicts the second clause. However, we cannot get a contradiction from the first two clauses by chaining even at variable subterms (regardless of how the ordering is defined). In this example we can get a contradiction by an inference that combines chaining into a variable with a subsequent unification of terms. Thus, we get f(x) < f(f(a)) by chaining, and the empty clause, because f(x) and f(f(a)) are unifiable. This is a limited form of resolution, which may be called context resolution, in which a context is put around one of the literals before the actual resolution takes place. In the example above, the context is determined by the chaining and the subsequent unification. Unfortunately, in the presence of non-linear variables, the context may have to be guessed. Take the clauses a < b and f(g(b), x, x) ≮ f(y, y, g(a)). Assuming suitable monotonicity axioms, the first clause implies f(g(b), g(a), g(a)) < f(g(b), g(b), g(a)), which indicates the appropriate context for a < b, so that resolution with the second clauses yields a contradiction.

9At this point the reader should not be confusing the ordering < on the object level with the term orderings ≻ on the meta-level that is used to restrict the search space for theorems about <.

It appears as if the problem cannot be solved satisfactorily in general. Monotonicity axioms cannot be implemented by subterm chaining without avoiding chaining below variables. The alternative which we can propose on the basis of our results is to make monotonicity axioms for general transitive relations subject to standard ordered (head) chaining, but at the same time apply a more refined analysis of redundancy to especially prolific kinds of inferences. For instance, ordered chaining inferences in B of the form

\frac{x < y → f(x) < f(y) y < z → f(y) < f(z)}{x < y , y < z → f(x) < f(z)}

with < transitive, are redundant in any N that contains x < y → f(x) < f(y). For the inference to be ordered, one must have y ≻ x and y ≻ z. To show redundancy we have to find a proof of the conclusion that uses only instances of N which are smaller than the maximal premise y < z → f(y) < f(z). In addition the proof may use arbitrary instances of the transitivity axiom for <. Clearly, x < y∧y < z implies x < z by transitivity and any instance of x < z → f(x) < f(z) is smaller than the corresponding instance of y < z → f(y) < f(z) whenever y ≻ x.^{10}

In the future one should develop special versions of subterm chaining for particular algebraic structures such as ordered groups and fields or lattices. The presence of additional algebraic structure seems to simpifiy the problem considerably. On the other hand the technical treatment gets much more involved. The present treatment has to be generalized to rewriting modulo AC, and specific forms of simplification that are afforded by the algebraic structure have to be integrated. A detailed analysis of redundancy is required for inferences between theory clauses and “user clauses”. A specialized version of AC-superposition for commutative rings, but without orderings, has been described by Bachmair, Ganzinger and Stuber (1995a).

6 Total Orderings

In this section we shall refine the subterm chaining calculus S in the presence of total orderings. We assume that L specifies < as a transitive relation. Atoms of the form s < t are called inequalities. Negative inequalities ¬(s < t) will also be written as s ≮ t. We assume that < is intended to denote a total ordering, that is, consider saturation of sets N of clauses which contain the irreflexivity axiom

x ≮ x

subsequently also denoted by Ir, and the totality axiom

x < y ∨ y < x ∨ x ≈ y ,

subsequently also denoted by T_{x,y} or, in short, by T. We will show that saturation can be organized such that no explicit inferences with totality are required and such that inferences with clauses in which the maximal term occurs more than once, in particular composition resolution inferences with inequations, can be drastically simplified. Finally we will again address the problem of variable chaining and present simplification techniques that eliminate the need for many, if not all, variable chainings.

10This reasoning requires compatibilty of ≻ with contexts. Hence even if one does not implement monotonicity axioms by subterm chaining, ≻ should be a reduction ordering so as to allow for redundancy arguments of the indicated kind.

In order to not complicate the presentation technically we assume that we have just one total ordering < and that < engages in no composition laws other than transitivity of < and compatibility with congruences. We assume moreover that ∼ and equality ≈ are the same and the only congruence relation.

6.1 Treating Irreflexivity

It is useful to treat the irreflexivity of < explicitly by an inference we call irreflexivity resolution:

Irreflexivity Resolution:

\frac{C , u < v}{Cσ}

where (i) σ is the most general unifier of u and v; and (ii) uσ < vσ is strictly maximal with respect to Cσ.

In the presence of irreflexivity resolution negative chaining into x ≮ x is redundant:

Proposition 8 Let N be such that all inferences by irreflexivity resolution from N are redundant in N. Then any inference by negative chaining into the irreflexivity clase x ≮ x is redundant in N ∪ Ir.

Proof. Suppose that

\frac{C , s < t s ≮ s}{C , t ≮ s}

is a ground inference by negative chaining into the irreflexivity clause such that s ≻ t. Let N′ denote the instances of N ∪Ir smaller than s ≮ s. We have to prove that C ∨ t ≮ s is implied by s < t, L and N′. Suppose that C is false and t < s is true in some model J of L, s < t, and N′. Then t < t is true in J. But t ≮ t is in N′ which is a contradiction. Hence s ≮ t is true in J. The other type of inference by negative chaining into the irreflexivity clause has the form

\frac{C , s < t s ≮ s}{C , t ≉ s}.

where s ⪰ t. If s ≻ t, its redundancy is proved in a similar way. For s = t we may obtain C by irreflexivity resolution, and this inference was assumed to be redundant. □

6.2 Treating Totality

At first we show that chaining inferences with totality are not needed.

Proposition 9 Any chaining inference from N ∪ T_{x,y} of the form

\frac{C , s < t x < y , y < x, x ≈ y}{C , s < y , y < t, t ≈ y}

is redundant in N ∪ T_{x,y}.

Proof. We have to show that any ground instance of the conclusion C′ = C , s < y , y < t, t ≈ y follows from s < t and from instances in N ∪ T_{x,y} strictly smaller than T_{t,y}, assuming the axioms in L to be satisfied. From the ordering restrictions of the inference we infer that t ≻ s and t ≻ y for the ground instance under investigation. Suppose that C is false. We perform a case analysis on s < y, hence apply T_{s,y} which is smaller than T_{t,y}. If s < y is true then C′ is true. If y < s or y ≈ s is true, by transitivity of < and by compatibility with ≈, y < t is true, hence C′ is true, also in this case. This completes the redundancy proof. □

Chaining inferences of the form

\frac{C , s ≈ t x < y , y < x, x ≈ y}{C , s < y , y < t, t ≈ y}

into a variable x are excluded anyway in S. Hence if the only composition laws in which < is involved are transitivity and compatibility with ≈, no chaining inferences which involve totality are needed.

Lemma 8 For any set of clauses N, all inferences from N ∪T by ordered subterm chaining, ordered factoring and irreflexivity resolution in which at least one of the premises is T are redundant in N ∪ T.

Proof. The chaining cases have been considered above. For the other inferences an easy inspection reveals that from T they produce tautologies. □

Next we look at negative chaining into inequations. These can be avoided by transforming clauses of the form C ∨ s ≮ t into C ∨ t < s ∨ t ≈ s which, in the presence of totality, is logically equivalent.

Proposition 10 C ∨ s ≮ t is not an instance of the irreflexivity clause then it is redundant in N ∪ Ir ∪ { C ∨ t < s ∨ t ≈ s }.

Proof. For the proof we may assume that C ∨ s ≮ t is ground, and otherwise apply the proof to all ground instances of C ∨ s ≮ t. If s = t then C is not the empty clause and hence is properly subsumed by the irreflexivity clause. Otherwise, suppose that s ≻ t (the case t ≻ s is proved in a similar way). Let N′ be the set of ground instances of N ∪ Ir ∪ { C ∨ t < s ∨ t ≈ s } smaller than C ∨ s ≮ t. C′ = C ∨ t < s ∨ t ≈ s is in N′. Let J be a L-model of N′. Suppose that C is false and s < t is true in J. As C′ is true in J, t < s or t ≈ s is true in J. According to L, < is transitive and compatible with ≈. Therefore we conclude in both cases that t < t is true in J which contradicts the fact that t ≮ t is in N′. Hence s ≮ t is true in J. □

Note that through applying one step of negative chaining with T, followed by reflexivity resolution, from C ∨ s ≮ t we may deduce C ∨ t < s ∨ t ≈ s, if s or t is a maximal term. The significance of the proposition rests in the fact that once we have the latter clause, any inference from the former is redundant. Therefore we need not chain into negative inequations of any clause provided we make totality resolution mandatory:

Totality resolution:

\frac{C , u ≮ v}{C , v < u, v ≈ u}

where u ≮ v is maximal in C.

Inference rules in which the conclusion renders one of its premises redundant are called simplification rules. They can be used to replace the redundant premise by the conclusion.

The following proposition provides us with further possibilities for optimization.

Proposition 11 Let C be a ground clause C′ ∨ s < t ∨ s < u with s the maximal term in C and s ≻ t ≻ u. Then C is redundant in

N ∪ T ∪ { C′ ∨ s < u ∨ u < t ∨ u ≈ t, C′ ∨ s < t ∨ t < u }.

Symmetrically, if C is of the form C′ ∨ t < s ∨ u < s with maximal term s and s ≻ t ≻ u. Then C is redundant in

N ∪ T ∪ { C′ ∨ u < s ∨ t < u ∨ t ≈ u, C′ ∨ t < s ∨ u < t }.

Proof. C′ ∨ s < u ∨ u < t ∨ u ≈ t and C′ ∨ s < t ∨ t < u are both smaller than C and, in the presence of T_{u,t} (which is also smaller than C), imply C in any L-model. The symmetric case is essentially the same. □

The proposition motivates the following inferences.

Inequality factoring:

\frac{C , s < t, s′ < u}{Cσ , sσ < uσ , uσ < tσ , uσ ≈ tσ}

and

\frac{C , s < t, s′ < u}{Cσ , sσ < tσ , tσ < uσ}

where σ is the most general unfier of s and s′, tσ ⪰̸ sσ, and sσ < tσ is strictly maximal in Cσ ∨ sσ < uσ;

and

\frac{C , t < s, u < s′}{Cσ , uσ < sσ , tσ < uσ , tσ ≈ uσ}

and

\frac{C , t < s, u < s′}{Cσ , tσ < sσ , uσ < tσ}

where σ is the most general unfier of s and s′, tσ ⪰̸ sσ, and tσ < sσ is strictly maximal in Cσ ∨ uσ < sσ.

6.3 Ordered Chaining for Total Orderings

We are now in a position to define an optimized chaining inference system O_{L}^{≻} for total orderings.

The calculus O_{L}^{≻} consists of the inferences in S_{L} with

(i) the exception of negative chaining or ordered resolution inferences with negative inequations s ≮ t;

(ii) the additional restriction sσ ≠ s′σ for inferences with a most general unifier σ for which one of the premises takes the form C = C′ ∨ s < t ∨ s′ < u [or C′ ∨ t < s ∨ u < s], with sσ the maximal term in C; and

(iii) the addition of inferences by irreflexivity resolution, totality resolution and inequality factoring.

As an immediate consequence of the above investigations we obtain the following completeness theorem.

Theorem 5 If a set of clauses N is saturated up to redundancy with respect to O_{L}^{≻}, then the set N ∪ L ∪ Ir ∪ T is unsatisfiable if and only if it contains the empty clause.

Proof. We show that if N is saturated up to redundancy by O then N ∪Ir∪T is saturated by S. The inferences of type (i) of S that are excluded from C are redundant. In case they involve the irreflexivity clause this can be seen by applying the Proposition 8. Otherwise if C is a clause C′ ∨ s ≮ t then, as N is saturated by totality resolution, any ground instance Cσ of C is redundant, or else the ground instance C′′σ of C′′ = C′ ∨ t < s ∨ t ≈ s follows from instances of N smaller than Cσ. In the latter case we may apply Proposition 10 to infer that Cσ follows from instances in N ∪ { C′′ } smaller than Cσ. Hence Cσ is redundant in N.

For inferences of type (ii), let Cσ be a ground instance of C = C′ ∨ s < t ∨ s′ < u [or C′ ∨ t < s ∨ u < s] such that tσ ⪰̸ sσ, sσ = s′σ, and sσ < tσ [tσ < sσ] is strictly maximal in C. As N is saturated under inequality factoring, applying Proposition 11, we infer in a similar way that Cσ is redundant in N.

Finally, from Lemma 8 we conclude that (the remaining) inferences in O that involve the totality axiom are redundant, too. □

6.4 A Refined Clause Ordering

In O_{L}^{≻} composition resolution inferences involving < are still possible. They might, for instance, take the form

\frac{C , u V v , u′ < v′ D , s < t}{Dσ , tσ ≮ v′σ , sσ < v′σ}

for a relation V different from <. Such inferences can be avoided if the ordering on atoms is stratified such that uσ V vσ cannot lie in between two inequations involving the maximal term uσ = sσ = u′σ.

For this reason the complexity measure c_{L} for literals L will now be refined. The resulting class of clause orderings ≻ will also make O^{≻} monotone. Another consequence of the refinement is that most cases of variable elimination for dense total orderings become simplifications, cf. Section 6.6. To that end certain properties of the non-ground clause from which a ground clause is obtained as an instance will be essential. Let L be a ground literal A or ¬A in a ground instance Cσ of a clause C. Let n_{C} be the number of different variables occuring as arguments of an equality or an inequality in C. For example, if C is the clause x < f(y) ∨ z ≤ f(z), then n_{C} = 2, as both x and z (but not y) qualify. Then c_{L} = (max_{L}, p_{L}, s_{L}, r_{L}, n_{L}, d_{L}) where the first three components are defined as in Section 5.3; r_{L} is 1 if A is an inequation, r_{L} is 0 if A is an equation, and r_{L} is 2, otherwise; d_{L} is 1 if the maximal term occurs twice in L, and 0, otherwise; and n_{L} is 0 if A is not an inequation; n_{L} is −1 if C is the totality axiom, and n_{L} is n_{C}, otherwise. Clearly, literal orderings (or more precisely, orderings on occurrences of literals in ground instances of clauses) which are compatible with the new definition of c_{L} are admissible literal orderings in the sense of section 5.3, thus the completeness results about S and C apply. From now an ordering ≻ is called admissible if it is compatible with the preceding complexity measure.

Under this class of orderings, any composition resolution involving < must be of the form

\frac{C , u < v , u′ < v′ D , s < t}{Dσ , tσ ≮ v′σ , sσ < v′σ}

where σ is the most general unifier of u, u′ and s, tσ ⪰̸ sσ, vσ ⪰̸ uσ, v′σ ⪰̸ u′σ, and the literal uσ < vσ is strictly maximal in Cσ ∨ u′σ < v′σ. (The inference might also be of the dual form with maximal terms on the right sides of inequations.) Inferences of this form are excluded from O^{<} as their first premise is rendered redundant by inequality factoring.

Lemma 9 For the class of admissible orderings ≻, O^{≻} is monotone.

Proof. Composition resolution inferences do not involve < in their main atom, hence the new component n_{L} is irrelevant there, and the proof is similar to Lemma 4. Non-trivial cases of inferences are those in which n_{C} may be bigger for the conclusion than for any of its premises. An easy inspection reveals that this is possible only for chaining inferences through an equality or inequality. As n_{C} only affects the complexity of inequalities, we need to look at ground inferences of the form

\frac{C , u ≈ v D , s[u] < t}{C , D , s[v] < t}

or

\frac{C , v < s D , s < t}{C , D , v < t} .

According to the ordering restrictions in O, in particular (ii) above, neither C nor D contains an inequation of the form s < w. Therefore, if L is a literal in C or D, it is smaller than s < t already according to one of the first four components in c_{L}. (If the complexity measures do not differ with respect to max_{L}, p_{L} and s_{L}, then L cannot be an inequation, hence, r_{L} ist 0, while it is 1 for s < t.) We may conclude that the conclusion is smaller than the second premise, regardless of the number of unshielded variables in it. □

6.5 Non-strict Orderings

Totality resolution converts s ≮ t into a disjunction t < s ∨ t ≈ s, by which the terms s and t are duplicated. In general clauses may get twice as big and chaining produces even longer clauses containing many repeated occurrences of terms. This is a severe efficiency problem in practice. As a solution we propose to deal with <, ≈ and the reflexive closure ≤ of < simultaneously. We restrict ourselves to positive occurrences of strict and non-strict inequations.

Formally we introduce ≤ on the meta-level by considering an atom s ≤ t just as a more concise notation for the disjunction s < t ∨ s ≈ t. Note that in this disjunction the equation cannot be maximal so that inferences with ≤ result from inferences with the strict inequation. We propose the following changes to inferences involving < and ≤ which considerably reduce term duplication.

The original chaining inference from the expanded versions of clauses C ∨ s < t and D ∨ t ≤ u yields C ∨ D ∨ s < u ∨ t ≈ u. We should instead infer C ∨ D ∨ s < u which is logically sound in the presence of L and which subsumes the former. From C ∨ s ≤ t and D ∨ t ≤ u, instead of inferring C ∨ D ∨ s < u ∨ t ≈ u ∨ s ≈ t, we may deduce C ∨ D ∨ s < u ∨ t ≈ u which again is sound and subsumes the former. Given C ∨ s ≈ t and D ∨ t ≤ u, S^{≻} requires to infer C ∨ D ∨ s < u ∨ t ≈ u. We may instead infer C ∨ D ∨ s ≤ u, which stands for C ∨ D ∨ s < u ∨ s ≈ u. In interpretations in which s ≈ t both clauses are equivalent but the latter is smaller than the former whenever s ≺ t. Hence the old inference becomes redundant whenever the new inference is redundant. Inequality factoring can be changed in a similar way to avoid duplication of terms. An example for the new inferences is

\frac{C , s < t, s ≤ u}{C , t ≤ u, s < t}

together with

\frac{C , s < t, s ≤ u}{C , u < t, s ≤ u} .

6.6 Variable Elimination

From now on we use the symbol ⊲ to denote strict and non-strict inequalities < and ≤. ⊴ will denote ⊲ or ≈. When we speak of the priority of a relation symbol among <, ≤, and ≈, we take < to have highest and ≈ the lowst priority.

A variable chaining is a chaining from C ∨ s ⊲_{1} t and D ∨ u ⊲_{2} v through tσ = uσ in which one of the terms t or u is a variable. As we have already observed in section 3.4, the ordering constraints considerably cut down on the number of variable chainings. More specifically, the ordering constraints can only be satisfied if each term t or u is either a non-variable or an unshielded variable; that is, a variable that does not occur in a subterm f(…, x, …) nor in an atom that is neither an equation nor an inequation. For example, the variable x is unshielded in a < x ∨ x < b, if a and b are constants. x and y are both shielded in x ≤ y ∨ s(y) < s(x). Certain unshielded variables can be eliminated in any total ordering. More occurrences of unshielded variables can be eliminated in total orderings without endpoints. If the ordering is also dense all unshielded variables can be eliminated.

The following inference eliminates all unshielded occurences of a variable x from a clause if all occurrences of x are in inequations s ⊲ t.

Variable Elimination:

\frac{C , u_{1} ⊲_{1} x, …, u_{m} ⊲_{m} x, x ⊲′_{1} v_{1}, …, x ⊲′_{n} v_{n}}{C , ⋁_{1 ≤ i ≤ m,1 ≤ j ≤ n} u_{i} ⊲_{i,j} v_{j}}

with n, m ≥ 0, where x is an unshielded variable not occurring in C, u_{i} and v_{i}, and where ⊲_{i,j} is the lowest-priority symbol of ⊲_{i} and ⊲′_{j}.

This inference rule is sound for total dense orderings without endpoints. It has been used by Bledsoe, Kunen and Shostak (1985) in their chaining calculus. Their calculus does not admit predicates other than ⊲. (But even then equality s ≈ t is implicitly present in the conjunction of two nonstrict inequalities s ≤ t and t ≤ s. To assure completeness they have to explicitly compute inferences with congruence axioms as specified by the set of clauses

⋁_{1 ≤ i ≤ n} x_{i} < y_{i} ∨ ⋁_{1 ≤ i ≤ n} y_{i} < x_{i} ∨ f(x_{1}, …, x_{n}) ≤ f(y_{1}, …, y_{n})

where f ranges over all function symbols.)

Weaker variable elimination rules can be applied to non-dense orderings. For example, in any total ordering a < b is equivalent to a < x ∨ x < b. In an ordering without left endpoint a disjunction C ∨ ⋁_{i} x ≈ u_{i} ∨ ⋁_{j} t_{j} < x, where x does not occur in C or any term t_{i}, is equivalent to C. In a total, “discrete” ordering, in which s(x) denotes the “successor” of x, the disjunction a ≤ x ∨ x ≤ b is equivalent to a ≤ b ∨ a ≈ s(b). This can also be generalized to a variable elimination rule. Hines (1994) proposes related elimination rules for a certain fragment of the first-order theory of integers.

Lemma 10 (i) A clause C ∨ s ≈ s is redundant with respect to any set of clauses.

(ii) A clause C′ of the form C ∨ ⋁_{i} x ⊴_{i} u_{i} (or C ∨ ⋁_{i} u_{i} ⊴_{i} x) in which i ranges over a non-empty set of indices and x is an unshielded variable that does not occur in C is L-redundant with respect to any set of clauses that contains C.

(iii) Let C′ be a clause C ∨ ⋁_{i} u_{i} ⊲_{i} x ∨ ⋁_{j} x ⊲_{j} v_{j} with an unshielded variable x not occurring in C, u_{i}, v_{i}, and let C′′ be C ∨ ⋁_{i,j} u_{i} ⊲_{i,j} v_{j}, where ⊲_{i,j} is the lowest-priority symbol of ⊲_{i} and ⊲′_{j}. Then C′ is either a totality axiom or else C′ is L-redundant with respect to any set N that contains C′′ and the totality axioms.

Proof. (i) C is a tautology and hence redundant.

(ii) C implies C′ and is smaller.

(iii) We sketch the main ideas. Let C′ be not a variant of the totality axiom. Take ground instances D′ = D ∨ ⋁_{i} a_{i} ⊲_{i} c ∨ ⋁_{j} c ⊲_{j} b_{j} and D′′ = D ∨ ⋁_{i,j} a_{i} ⊲_{i,j} b_{j} of C′ and C′′, respectively. Since C′′ does not contain the unshielded variable x, but otherwise contains the same terms as C′, we have n_{L′} > n_{L′′} for any pair of literals L′ in D′ and L′′ in D′′, respectively. Consider the maximal literal L′′ in D′′. Then there is an inequality L′ in D′ with the same or bigger maximal term occurring in the same argument position. Hence, the complexity tuple associated with L′ is bigger than the tuple associated with L′′ in one of the first five components. In short, we have D′ ≻ D′′.

Let T_{a} be the set of all disjunctions c < a_{i} ∨ a_{i} ≤ c and let T_{b} be the set of all disjunctions c < b_{j} ∨ b_{j} ≤ c. These are ground instances of the totality axiom. It can be shown that D′ is true in every L-model of T_{a} ∪ {D′′} and in every L-model of T_{b} ∪ {D′′}. Also, if none of the terms a_{i} or c is maximal in D′, then clearly all clauses in T_{a} are smaller than D′. On the other hand, if some term a_{i} or c is maximal in D′, then that term occurs as the first argument of an inequality in D′, which we may use to infer that all clauses in T_{b} are smaller than D′. (Note that the n_{L}-count for T_{b}-literals is −1 which is essential in case c is maximal.) In sum, D′ is L-redundant with respect to T ∪ {D′′}. □ The lemma not only indicates that variable elimination for clauses of type (i)–(iii) is simplifying, but that in the presence of the totality axioms the premise in any of the elimination rules is rendered redundant by its conclusion. Like totality resolution, the variable elimination rules are simplification rules: their premises can be replaced by the respective conclusion. In other words, if variable elimination is made mandatory, then no other inference rule needs to be applied to a clause with an unshielded variable, which also means that variable chainings are not needed. The compatibility of eager variable elimination with other chaining systems has been shown by Richter (1984) and Hines (1992).

Variable elimination in the presence of arbitrary equations is somewhat more complicated. The cases (i) and (ii) of Lemma 10 are already applicable to clauses with equations. To eliminate an unshielded variable x from a clause D in the remaining cases we translate all (positive and negative) equalities with x into inequalities, and then apply the above variable elimination rule. More precisely, a clause

D = C ∨ ⋁_{1≤i≤m} x ≉ u_{i} ∨ ⋁_{1≤j≤n} x ≈ v_{j}

where x is an unshielded variable, is transformed to the formula

C ∨ ⋁_{1≤i≤m}(x < u_{i} ∨ u_{i} < x) ∨ ⋁_{1≤j≤n}(x ≤ v_{j} ∧ v_{j} ≤ x)

in which x does not occur in an equality. (We assume that either the disjunction of the negative equations x ≉ u_{i} in D is non-empty or else there are occurrences of x in inequalities of the form x ⊲ s and t ⊲ x in C. (If this is not the case then one of the cases (i) or (ii) of Lemma 10 applies.) The formula can be translated into 2^{n} clauses, to which the variable elimination rule can be applied. Let us denote by Ve_{D} the set of all these clauses, with x eliminated. Unfortunately, some ground instances of clauses in Ve_{D} may be larger than the corresponding ground instance of Dσ with respect to our clause ordering. Consequently, clauses are not necessarily rendered L-redundant by variable elimination. However, those ground instances of D, in which x is instantiated to the maximal term in the clause, are L-redundant.

Lemma 11 Let D be a clause with an unshielded variable x of the above form and σ be a substitution such that xσ is a maximal term in Dσ. Then Dσ is redundant with respect to any set N that contains the clauses in Ve_{D} and the totality axioms.

To sum up these considerations, a clause with an unshielded variable x is in many but not all cases redundant. In any case inferences involving this variable (chaining through x, superposition from x, [in]equality factoring applied to [in]equalities with x as maximal term) are redundant. (The ordering constraints for such inferences require x to be instantiated with the maximal term, in which case the corresponding instances of the C are redundant, as indicated by the lemma.) The lemma thus indicates that variable chaining is not needed if all variable elimination inferences are sound and are made mandatory. This is the case for dense total orderings without endpoints.

Let Do(d, l, r) denote the set of all clauses

x < d(x, y), y ≤ x
d(x, y) < y , y ≤ x

l(x) < x x < r(x) which encodes the properties of a dense ordering without endpoints. Let CV^{≻} denote the calculus consisting of the variable elimination inferences and of the inferences in O^{≻} excluding chaining inferences through variables as well as any other inference in which an unshielded variable denotes, according to the ordering restrictions of the inference, the maximal term. CV^{≻} is refutationally complete (and sound in the presence of Do(d, l, r)). Explicit inferences with the clauses in Do(d, l, r) are not required.

Theorem 6 Let N be a set of clauses that is saturated up to L-redundancy with respect to CV^{≻}. Then N ∪ Ir ∪ T ∪ Do(d, l, r) is also saturated up to L-redundancy, where d, l and r are function symbols not in N.

Proof. The only possible inferences between clauses in N ∪ T and Do(d, l, r) would be variable chainings, of which there are none in CV. The only other inference from Do(d, l, r) which is the chaining of the two axioms for d produces a tautology and is therefore redundant too. Since N is assumed to be saturated, inferences from N ∪ T are also redundant in N and hence in N ∪ T ∪ Do(d, l, r). In short, N ∪ T ∪ Do(d, l, r) is saturated. □

7 Conclusions

We have shown how to extend standard term rewriting techniques in saturation-based theorem proving to binary relations other than equality. Ordered paramodulation has been generalized to ordered (subterm) chaining. By ordered chaining we may implement a large class of composition laws for binary, in general non-symmetric relations. In the paper we have in particular investigated transitive relations (system B), families of general composition laws (system C), composition laws for binary relations in the presence of partial congruences (system S), and total orderings (systems O and CV).

The main advances over previous work on chaining-based inference systems are the following. We have justified the ordering restrictions for chaining inferences by the concept of commutation for rewrite systems. Our calculi can treat more than one special binary relation at the same time Our completeness results apply to arbitrary signatures of non-logical symbols. We have provided for an integrated treatment of equality and other transitive relations whereby known results about superposition are obtained as special cases. The completeness results for the various inference systems have been obtained in the presence of a general notion of redundancy. The compatibility of simplification and deletion techniques can be justified by simply showing that deleted clauses or ignored inferences are redundant. In particular we have given a justification of variable elimination rules for total orderings by showing the redundancy of clauses with unshielded variables. We have also analysed the problem of chaining at or below variables to some extent.

In this paper we have not described any details about how saturation of a clause set up to redundancy might be done in practice. We refer the reader to our papers Bachmair and Ganzinger (1994b) and Bachmair and Ganzinger (1995b) for a detailed exposition of fairness issues and techniques for simplification and redundancy detection which readily carry over to the framework of the present paper.

The theory described here has been implemented in the Saturate system (Ganzinger 1994) and very promising experimental results have been obtained. Exploiting the structure of a background theory does help to find theorems faster. Our prover will do better for theories of transitive relations that satisfy additional logical properties such as symmetry or totality. By contrast automated theorem provers based on traditional approaches in automated theorem proving usually become tied up in exploring large uninteresting parts of the search space when one adds syntactically cumbersome axioms such as transitivity or totality axioms for a relation.

Search should be replaced as much as possible by don’t-care non-deterministic simplification, and the latter is intrisically theory-specific. The principle of replacing search by simplification and the problem of integrating mathematical decision procedures has been fundamental in the design of heuristic theorem provers such as the Boyer-More theorem prover or the PVS-System (Owre, Rushby and Shankar 1992). (In particular Boyer and Moore (1988) provide an interesting discussion about how to integrate mathematical theories into a heuristic prover.) The approach taken here, and as exemplified for the case of quantifier elimination (variable elimination) for dense total orderings, sets out for an integration that guarantees refutational completeness in the presence of arbitrary additional vocabulary. The decidable subcases are decided while in the general case search is to a large extent replaced by simplification. Many of the more prolific inferences can shown to be redundant.

With the methods developed in this paper only a first and small step has been taken towards making saturation-based theorem provers know about mathematics. Much work remains to be done. The next steps should be to investigate theorem proving for theories in which transitive relations, in particular orderings, interact with algebraic structure, that is, consider specializations of the calculi of the present papers in the presence of the axioms of an ordered group of field, or of fragments of lattice theory.

References

L. Bachmair and N. Dershowitz, 1986. Commutation, transformation, and termination. In J. H. Siekmann (ed.), Proc. 8th Int. Conf. on Automated Deduction, Lecture Notes in Computer Science 230, pp. 5–20. Springer-Verlag, Berlin.

L. Bachmair and H. Ganzinger, 1990. On restrictions of ordered paramodulation with simplification. In M. Stickel (ed.), Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lecture Notes in Computer Science 449, pp. 427–441. Springer-Verlag, Berlin.

L. Bachmair and H. Ganzinger, 1994a. Ordered chaining for total orderings. Proc. 12th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 814, pp. 435–450. Springer-Verlag, Berlin.

L. Bachmair and H. Ganzinger, 1994b. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3): 217–247. Revised version of Technical Report MPI-I-91-208, 1991.

L. Bachmair and H. Ganzinger, 1994c. Rewrite techniques for transitive relations. Proc. 9th IEEE Symposium on Logic in Computer Science, pp. 384–393. IEEE Computer Society Press.

L. Bachmair and H. Ganzinger, 1995a. Associative-commutative superposition. In N. Dershowitz (ed.), Proc. 3rd Int’l Workshop on Conditional and Typed Rewriting, Jerusalem, Lecture Notes in Computer Science 968, pp. 1–14. Springer-Verlag, Berlin. Revised version of TR MPI-I-93-267, 1993.

L. Bachmair and H. Ganzinger, 1995b. The theory of resolution. In preparation.

L. Bachmair, N. Dershowitz and J. Hsiang, 1986. Orderings for equational proofs. Proc. Symp. Logic in Computer Science, pp. 346–357. Boston, Massachusetts.

L. Bachmair, N. Dershowitz and D. Plaisted, 1989. Completion without failure. In H. Ait-Kaci and M. Nivat (eds), Resolution of Equations in Algebraic Structures, vol. 2, pp. 1– 30. Academic Press.

L. Bachmair, H. Ganzinger and J. Stuber, 1995a. Combining algebra and universal algebra in first-order theorem proving: The case of commutative rings. In E. Astesiano, G. Reggio and A. Tarlecki (eds), Recent Trends in Data Type Specification, Lecture Notes in Computer Science 906, pp. 1–29. Springer-Verlag, Berlin.

L. Bachmair, H. Ganzinger, C. Lynch and W. Snyder, 1995b. Basic paramodulation. Information and Computation 121(2): 172–192. Revised version of TR MPI-I-93-236, 1993.

F. Bellegarde and P. Lescanne, 1987. Transformation ordering. In H. Ehrig, R. Kowalski, G. Levi and U. Montanari (eds), TAPSOFT’87, Vol. 249, pp. 69–80.

W. Bledsoe, K. Kunen and R. Shostak, 1985. Completeness results for inequality provers. Artificial Intelligence 27: 255–288.

R. S. Boyer and J. S. Moore, 1988. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In J. E. Hayes, D. Michie and J. Richards (eds), Machine Intelligence 11, chapter 5, pp. 83–124. Clarendon Press, Oxford.

D. Brand, 1975. Proving theorems with the modification method. SIAM Journal of Computing 4: 412–430.

N. Dershowitz and J.-P. Jouannaud, 1990. Rewrite systems. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pp. 243–309. North-Holland, Amsterdam.

N. Dershowitz, 1987. Termination of rewriting. Journal of Symbolic Computation 3: 69–116.

N. Dershowitz, 1991. A maximal-literal unit strategy for horn clauses. Proc. 2nd Int. Workshop on Conditional and Typed Rewriting Systems, Lecture Notes in Computer Science 516, pp. 14–25. Springer-Verlag, Berlin.

H. Ganzinger, 1991. A completion procedure for conditional equations. Journal of Symbolic Computation 11: 51–81.

H. Ganzinger, 1994. The Saturate system. Available on the world-wide web under URL http://www.mpi-sb.mpg.de/SATURATE/Saturate.html.

A. Geser, 1991. Relative Termination. Ulmer Informatik–Berichte 91-03, Universiät Ulm, Fakultät für Informatik, Ulm, FRG.

L. M. Hines, 1992. Completeness of a prover for dense linear logics. Journal of Automated Reasoning 8: 45–75.

L. M. Hines, 1994. Str ˙+ve and integers. In A. Bundy (ed.), Twelfth International Conference on Automated Deduction, LNAI 814, pp. 416–430. Springer-Verlag, Nancy, France.

J. Hsiang and M. Rusinowitch, 1991. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Journal of the ACM 38(3): 559–587.

J. W. Klop, 1992. Term Rewriting Systems, Vol. 2, pp. 2–116. Clarendon Press, Oxford.

J. Levy and J. Agustí, 1993. Bi-rewriting, a term rewriting technique for monotonic order relations. In C. Kirchner (ed.), Rewriting Techniques and Applications, Lecture Notes in Computer Science 690, pp. 17–31. Springer, Berlin.

Z. Manna and R. Waldinger, 1986. Special relations in automated deduction. Journal of the ACM 33: 1–60.

Z. Manna and R. Waldinger, 1992. The special-relation rules are incomplete. In D. Kapur (ed.), 11th International Conference on Automated Deduction, pp. 492–506. Springer LNAI 607, Saratoga Springs, NY.

R. Nieuwenhuis and A. Rubio, 1992. Basic superposition is complete. ESOP’92, Lecture Notes in Computer Science 582, pp. 371–389. Springer-Verlag, Berlin.

R. Nieuwenhuis and A. Rubio, 1994. AC-superposition with constraints: No AC-unifiers needed. Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science 814, pp. 545–559. Springer-Verlag, Berlin.

S. Owre, J. M. Rushby and N. Shankar, 1992. PVS: A prototype verification system. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNCS 607, pp. 748–752. Springer.

J. Pais and G. Peterson, 1991. Using forcing to prove completeness of resolution and paramodulation. Journal of Symbolic Computation 11: 3–19.

G. E. Peterson, 1983. A technique for establishing completeness results in theorem proving with equality. SIAM J. on Computing 12(1): 82–100.

M. Richter, 1984. Some reordering properties for inequality proof trees. Lecture Notes in Computer Science 171, pp. 183–197. Springer-Verlag.

G. Robinson and L. T. Wos, 1969. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie (eds), Machine Intelligence 4, pp. 133–150. American Elsevier, New York.

M. Rusinowitch, 1991. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix completion procedure as a complete set of inference rules. J. Symbolic Computation 11: 21–49.

D. S. Scott, 1979. Identity and existence in intuitionistic logic. Applications of Sheaves, Proc. Durham, Lecture Notes in Mathematics 753, pp. 660–695.

J. R. Slagle, 1972. Automatic theorem proving for theories with built-in theories including equality, partial orderings, and sets. Journal of the ACM 19: 120–135.

L. Vigneron, 1994. Associative-commutative dedution with constraints. Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science 814, pp. 530–544. Springer-Verlag, Berlin.

H. Zhang and D. Kapur, 1988. First-order theorem proving using conditional rewrite rules. In E. Lusk and R. Overbeek (eds), Proc. 9th Int. Conf. on Automated Deduction, Lecture Notes in Computer Science 310, pp. 1–20. Springer-Verlag, Berlin.

H. Zhang, 1988. Reduction, superposition and induction: Automated reasoning in an equational logic, PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York.