MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Ordered Chaining for Total Orderings

Leo Bachmair Harald Ganzinger

MPI–I–93–250 December 1993

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

Im Stadtwald D 66123 Saarbrücken

Germany Addresses

Leo Bachmair, Department of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794,

U.S.A, leo@sbcs.sunysb.edu

Harald Ganzinger, Max-Planck-Institut für Informatik, Im Stadtwald, D-66123 Saarbrücken, Ger-

many, hg@mpi-sb.mpg.de

Acknowledgements

The research described in this paper 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 design new inference systems for total orderings by applying rewrite techniques to chaining calculi. Equality relations may either be specified axiomatically or built into the deductive calculus via paramodulation or superposition. We demonstrate that our inference systems are compatible with a concept of (global) redundancy for clauses and inferences that covers such widely used simplification techniques as tautology deletion, subsumption, and demodulation. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. Syntactic ordering restrictions on terms and the rewrite techniques which account for their completeness considerably restrict variable chaining. We show that variable elimination is an admissible simplification techniques within our redundancy framework, and that consequently for dense total orderings without endpoints no variable chaining is needed at all.

Keywords

Automated Theorem Proving, First-Order Logic, Total Orderings, Chaining, Variable Elimination, Term Rewriting

Contents

1 Introduction 1 1.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

2 Preliminaries 3 2.1 Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Predicate logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Chaining . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.4 Simplification orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.5 Rewrite systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Maximal chaining 6 3.1 Inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 Redundancy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Refutational completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.4 Variable elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.5 Saturation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

4 Chaining with superposition 14

5 Summary 19

1 Introduction

The axioms of the theories of partial and total orderings are extremely prolific in the context of resolution-based theorem proving. Many theorem provers build in transitivity by so-called chaining rules, which allow one to derive (C ∨ D ∨ u < v)σ from premises C∨u < s and D∨t < v after unifying s and t by σ. Even though chaining is a considerable improvement over naive resolution, in this general form it still generates a huge search space. First, chaining inferences are always possible if s or t is a variable. For instance, the totality axiom x < y ∨ y ≤ x can always be applied in four different ways, leading to the derivation of many equivalent variants of each clause. The situation is even worse for total orderings with additional structure, and in particular dense orderings with no endpoints. The clauses which express density and the absence of endpoints can also be chained with any other clause. For example, the clause x < rx expressing the nonexistence of a right endpoint, generates infinitely many inequalities x < r^{n}x just by chaining with itself. Secondly, the same clause C ∨ u < s can be used as the first or as the second premise of a chaining inference, so that one needs to chain with both terms, u and s. Third, and related to the first two points, chaining is designed to generate the full (possibly infinite) transitive closure of a given set of inequalities, even though for any particular refutation a finite subset will be sufficient. This lack of goal-orientedness forms another obstacle to any efficient proof search. These problems apply to transitive relations in general; solutions have been proposed for certain theories.

Bledsoe and Hines (1980) have investigated dense total orderings without endpoints and have developed techniques for eliminating certain occurrences of variables from formulas. In their inference system, no chaining through variables is performed and no explicit inferences with transitivity, density, totality and the “no endpoints” axioms are computed. Completeness results for particular such systems of restricted chaining are proved by Bledsoe, Kunen and Shostak (1985) and Hines (1992). Theorem provers developed from these theoretical investigations have performed successfully in proving theorems such as the continuity of the sum of two continuous functions or the intermediate value theorem; see Bledsoe and Hines (1980), Hines (1988) or Hines (1990).

Ordered paramodulation (Hsiang and Rusinowitch 1991) and superposition (Bachmair and Ganzinger 1990) are chaining-based inference systems for equality relations (the congruence properties of which also require chaining through subterms). Paramodulation into or below variables was first shown to be unnecessary by Brand (1975). Various syntactic restrictions avoid that equalities are always applied in both directions. In many cases even an infinite transitive closure of a given set of equalities can be represented by a finite convergent rewrite system. Only that system, and not the complete transitive closure of the given set of equalities (or clauses), is computed by the ordered variants of paramodulation and superposition.

Our aim is to combine the two approaches, keeping their best features, but avoiding their drawbacks. For that purpose we adapt the term rewriting techniques for arbitrary transitive relations described in Bachmair and Ganzinger (1993) to total orderings.

1.1 Results

We present refutationally complete inference systems for total orderings, in which chaining is restricted by syntactic ordering constraints in much the same way as we know it from superposition calculi. That is, chaining inferences as above are performed only if the term sσ is maximal in both (instances by σ of the) parent clauses. These ordering constraints immediately rule out many forms of chaining through variables. For instance, a term xσ cannot be maximal if the variable x is shielded in a clause, that is, occurs as an argument of a function symbol. We also go beyond simple chaining in that we eliminate all occurrences of the maximal term in one single inference that combines several chaining steps. The effect is similar to hyper-resolution, in that the results of intermediate chaining steps need not be explicitly generated. Explicit inferences with transitivity and totality are shown to be redundant. This inference system applies to arbitrary total orderings and avoids most, though not all, variable chainings. The ordering constraints, like in the equational case, derive from a presentation of the full transitive closure of the given binary relation by an appropriate rewrite closure.

We prove refutational completeness of our inference systems in the presence of a general notion of redundancy for clauses and inferences by which most of the commonly applied simplification and elimination techniques (e.g., tautology elimination or subsumption) can be justified. For total orderings in particular we show that variable elimination, as proposed by Bledsoe and Hines (1980), is a simplification rule in our sense: a clause becomes redundant once variable elimination has been applied to it. In other words, variable elimination can be made mandatory. Ordering constraints for inferences and mandatory elimination of unshielded variables together achieve that chaining through variables can be completely avoided for dense total orderings with no endpoints. Variable elimination is also excluded in the inference systems proposed by Bledsoe, Kunen and Shostak (1985) and Hines (1992), though these calculi, unlike ours, are not compatible with tautology deletion. Our proofs are comparatively simple and in particular profit from our ability of treating simplification techniques such as variable elimination as a separate issue.

The first of the two calculi which we present in this paper lacks an efficient treatment of equality. Like in previous approaches (Bledsoe and Hines 1980, Bledsoe, Kunen and Shostak 1985, Hines 1992) an equality s ≈ t is represented by two inequalities s ≤ t and t ≤ s. The disadvantage of this approach is that the implicitly specified equality relation requires additional congruence axioms for each function symbol, while such powerful simplification mechanisms as demodulation cannot be used. Therefore we describe another system, in which we combine chaining with superposition (Bachmair and Ganzinger 1990). Equality is thus built into the inference rules; explicit inferences with congruence axioms or functional reflexive axioms and superposition into or below variables are not needed. The extended inference system also considerably improves earlier chaining systems with paramodulation (Slagle 1972), and for dense orderings without endpoints superposition from variables is not needed either. In addition, when superposing into inequalities only the maximal term of the inequality needs to be replaced. As before, the completeness result allows to discard redundant clauses and inferences and admits simplifications such as demodulation or condensement.

We have implemented most the techniques investigated here as an extension of the Saturate system (Nivela and Nieuwenhuis 1993), and have obtained promising experimental results.

2 Preliminaries

2.1 Orderings

A (strict) partial ordering is a transitive and irreflexive binary relation; a quasi-ordering a reflexive and transitive binary relation. The reflexive closure of a strict ordering is a quasi-ordering. On the other hand, if ≤ is a quasi-ordering, then its strict part <, defined by: x < y if and only if x ≤ y but not y ≤ x, is a strict ordering. An ordering < is said to be total if x < y or y < x, whenever x and y are distinct. The ordering is dense if for all x and y with x < y, there exists an element z, such that x < z and z < y. An ordering < has no left (resp. right) endpoint if for every x there exists a y such that y < x (resp. x < y). By an ordering without endpoints we mean one that has neither a left nor a right endpoint. For instance, the usual less-than relation on the natural numbers is a total ordering with a left, but no right, endpoint. The less-than relation on the real numbers is a dense total ordering without endpoints.

2.2 Predicate logic

We consider first-order predicate logic with equality; more specifically, first-order languages with function symbols, variables, and (interpreted) predicate symbols <, ≤, and ≈.^{1} 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 s ≈ t, called an equality, or an expression s < t or s ≤ t, called a strict or non-strict inequality, respectively, where s and t are terms. A literal is an expression A (a positive literal) or ¬A (a negative literal), where A is an atomic formula. We also write s ≉ t instead of ¬(s ≈ t) and use a similar notation for inequalities. When we speak of the priority of a predicate symbol, we take < to have the highest and ≈ the lowest priority. The symbol ⊲ is used to denote (strict or non-strict) inequalities; the symbol ⊴ to denote equalities and inequalities. 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.

We intend ≈ to be interpreted as an equality relation^{2} and < as a strict ordering. Also, x ≤ y is meant to be interpreted as x < y∨x ≈ y. (From a logical point of view, the symbol ≤ is therefore superfluous. But for theorem proving purposes shorter formulas are generally preferable, and it is better to avoid replacing a non-strict inequality by a disjunction.) The most problematic properties of these relations—for an automated theorem prover—are the transitivity properties. By a transitivity interpretation we mean a model of the set T R of all transitivity axioms

1Uninterpreted predicate symbols can be encoded in a many-sorted language with function symbols and equality, by representing a formula P (t_{1}, …, t_{n}) as an equality f_{P} (t_{1}, …, t_{n}) ≈ true_{P}.

2An equality relation is a congruence on ground terms.

x ⊴_{1} y, y ⊴_{2} z → x ⊴ z

where ⊴ is the highest-priority symbol of ⊴_{1} and ⊴_{2}. For example, x ≮ y ∨y ≉ z ∨x < z is a transitivity axiom. The set P O consisting of the axioms in T R and the axioms

x < y → x ≤ y
→ x ≤ x
x < x →

encodes that < is a strict ordering and ≤ a quasi-ordering (with < contained in its strict part). Interpretations satisfying P O are called partial orderings for short. If in addition the totality axiom

x < y ∨ y ≤ x

is satisfied, the interpretation is called a total ordering. In that case, < coincides with the strict part of ≤.

2.3 Chaining

Many theorem provers build in transitivity by so-called chaining rules,

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

where σ is a most general unifier of s and t; see Slagle (1972). For instance, with chaining we may deduce s < t from s < u and u < t. Specific variants of this inference rule can be found in calculi for dense total orderings (Bledsoe and Hines 1980, Bledsoe, Kunen and Shostak 1985) and in paramodulation calculi for equality (Robinson and Wos 1969). In its full generality, the chaining rule is not practical, as the search space spanned by the inferences may be huge. Variable chainings, that is, chainings with a premise C ∨ u < x or D ∨ y < v, are particularly prolific. Fortunately, they can be completely excluded in the case of dense total orderings without endpoints (Bledsoe, Kunen and Shostak 1985) and considerably restrained in the case of paramodulation (Brand 1975 was the first to prove that paramodulation into a variable is unnecessary).

Chaining essentially generates the transitive closure of a given binary relation. For example, from a < b and b < c and c < d we may deduce a < c and b < d and a < d. In other words, whenever there is a (finite) chain of equalities and/or inequalities

x_{1} ⊴_{1} x_{2} ⊴_{2} ⋯ ⊴_{n−1} x_{n}

the equality or inequality x_{1} ⊴ x_{n} can be deduced, where ⊴ is the highest-priority predicate among all ⊴_{i}. The basic idea of the term rewriting approach is to consider not arbitrary chains, but only those in which the intermediate terms x_{2}, …, x_{n−1} are in a certain sense simpler than the endpoints x_{1} and x_{n}. Moreover, the equality or inequality x_{1} ⊴ x_{n} is not necessarily deduced, but instead the corresponding chain may be implicitly represented by a rewrite system. We employ these ideas for the design of refutationally complete chaining systems in which various constraints are imposed on inference rules. Two concepts are of importance in this context: rewrite systems and simplification orderings.

2.4 Simplification orderings

An ordering ≻ is well-founded if there is no infinite sequence t_{1} ≻ t_{2} ≻ · · ·. An ordering on ground terms is called a reduction ordering if it is well-founded and satisfies the following property: whenever s ≻ t then u[s] ≻ u[t], for all terms u, s, and t. A reduction ordering is called a simplification ordering if it also satisfies the subterm property: A[s] ≻ s, for all expressions A and proper subexpressions s of A. A reduction ordering is complete if it is total on ground terms. (Complete reduction orderings are simplification orderings.)

Later on, we shall extend the term ordering ≻ to an ordering on literals. Also, any ordering ≻ on a set S can be extended to an ordering on finite multisets over S (which for simplicity we also denote by ≻) as follows: M ≻ N if (i) M ≠ N and (ii) whenever N(x) > M(x) then M(y) > N(y), for some y such that y ≻ x. An ordering on literals can thus be extended to an ordering on clauses. If ≻ is a total (resp. well-founded) ordering, so is its multiset extension.

Finally, we extend an ordering ≻ to non-ground expressions by defining: 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′σ. We say that a literal L is maximal in a clause C if L′ ≻ L, for no literal L′ in C; and that L is strictly maximal in C if L′ ⪰ L, for no L′ in C.^{3}

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

2.5 Rewrite systems

Let I be a set of ground atomic formulas and ≻ be a simplification ordering. We use the equalities and inequalities in I as rewrite rules. More precisely, we write u ⊲_{I} v if u ⊲ v is an inequality in I and write u ≈_{I} v if u = w[s] and v = w[t], for some term w and equality s ≈ t or t ≈ s in I. Furthermore, we write u ⊴_{I}^{L} v, if u ≻ v, and u ⊴_{I}^{R} v, if v ≻ u. The subscripts are dropped if I is clear from the context.

By a proof (in I) we mean a finite sequence u_{0} ⊴_{1} u_{1} ⊴_{2} u_{2} … u_{n−1} ⊴_{n} u_{n} (in I), where n ≥ 0. More specifically, we speak of a proof of u_{0} ≤ u_{n}. We speak of a proof of u_{0} < u_{n} if in addition at least one of the symbols ⊴_{i} is < (and hence n ≥ 1); and of a proof of u_{0} ≈ u_{n} if all symbols ⊴_{i} are ≈. (If n = 0, we have a proof of u_{0} ≈ u_{0}.) By the transitive closure of I we mean the set of all atoms u ⊴ v provable in I. A rewrite proof is a sequence

u_{0} < u_{1}

or

u_{0} ⊴_{1}^{L} ⋯ ⊴_{m−1}^{L} u_{m} ⊴_{m}^{R} ⋯ ⊴_{n}^{R} u_{n}.

By the rewrite closure of I we mean the set of all atoms u ⊴ v that are provable by a rewrite proof in I.

In proving the completeness of chaining systems we construct Herbrand models for certain clause sets, describing interpretations by rewrite closures. A key question is under which circumstances the rewrite closure of a set I is a transitivity interpretation; a question, it turns out, that is related to commutation properties of the rewrite relations ⊴_{I}.

3Depending on the ordering on ground terms, 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.

If a sequence u_{0} ⊴_{1} ⋯ ⊴_{n} u_{n} is not a rewrite proof then either (i) there is a subsequence u_{i−1} ⊴_{i}^{R} u_{i} ⊴_{i+1}^{L} u_{i+1}, or (ii) u_{i−1} and u_{i} are identical or incomparable (i.e., u_{i−1} ⊁ u_{i} and u_{i} ⊁ u_{i−1}), for some i. A subsequence u ⊴_{1}^{R} t ⊴_{2}^{L} v, called a peak, is said to commute if u ⊴ v is provable by a rewrite proof, where ⊴ is the highest-priority symbol of ⊴_{1} and ⊴_{2}. Commutation allows us to deal with case (i). If ≻ is a complete simplification ordering, then case (ii) applies only if u_{i−1} = u_{i}.

For example, if I contains the atoms a < b and b < c and c < d, and if a ≻ b ≻ c ≻ d, then a <^{L} b and b <^{L} c and c <^{L} d. The relation <^{L} evidently commutes with the (empty) relation <^{R}. If we choose the ordering differently, b ≻ c ≻ d ≻ a, there is a peak, a <^{R} b <^{L} c, that does not commute. There are rewrite proofs of a < b and b < c, but not of a < c.

The following lemma relates commutation and transitivity.

Lemma 1 Let ≻ be a complete simplification ordering and I be a Herbrand interpretation that contains no strict inequality t < t. The rewrite closure of I is a transitivity interpretation if and only if all peaks in I commute.

Proof. Suppose that all peaks in I commute. It is sufficient to show that whenever u ⊴ v is provable in I, then there also exists a rewrite proof. If a sequence u = u_{0} ⊴_{1} ⋯ ⊴_{k} u_{k} = v contains peak, then by commutation the peak can be replaced by a rewrite proof. Moreover, any proof step u_{i} ≈ u_{i+1} or u_{i} ≤ u_{i+1}, where u_{i} = u_{i+1}, can be eliminated from a proof. (Strict inequalities t < t cannot always be eliminated, which is the reason why we have to exclude them.) The multiset of terms {u′_{0}, …, u′_{n}} used in the resulting new proof u = u′_{0} ⊴_{1} ⋯ ⊴_{n} u′_{n} = v is smaller than the multiset {u_{0}, …, u_{k}} with respect to the (multiset extension of the) simplification ordering ≻. Since the ordering ≻ is well-founded, we may conclude that every sequence of rewrites can be transformed to a rewrite proof.

For the converse observe that by transitivity of the rewrite closure of I any peak must have a rewrite proof. □

The lemma provides the starting point for our investigation of chaining techniques for total orderings, as peaks can be made to commute by applying suitable chaining inferences. (In the above example the peak a <^{R} b <^{L} c commutes once the inequality a < c has been deduced from a < b and b < c by chaining.) Similar, so-called “critical pair lemmas” form the basis of all completion procedures; Levy and Agustí (1993) appear to have been the first to apply these techniques to non-symmetric rewrite relations. We go beyond usual completion procedures in that we consider general clauses, and thus have to deal with negative literals and disjunctions of literals. Particular emphasis will be given to the question of (the necessity of) variable chainings. For a discussion of the general aspects of these questions we refer to our work on rewrite techniques for transitive relations (Bachmair and Ganzinger 1993). In this paper we look at total orderings, primarily dense total orderings without endpoints.

3 Maximal chaining

3.1 Inference rules

The predicate ≤ for non-strict inequality can be defined in terms of strict inequality and equality. It is also possible, though, to express equality in terms of inequality, representing u ≈ v by (the conjunction of) two inequalities u ≤ v and v ≤ u. This, indeed, is the framework in which previous chaining inference systems have been formalized, the advantage being that no specific inference mechanisms for equality are needed. The necessary properties of the implicit equality relation are specified by the set EE_{F} 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 in F; see Bledsoe, Kunen and Shostak (1985). The necessity of including these axioms is a disadvantage. Later on, we will build equality into the inference mechanism via paramodulation, thereby obviating any explicit equality axioms. (Another advantage of equational inference systems is that further simplification techniques such as demodulation become available, which are indispensable in actual implementations.)

In this section all atomic formulas are assumed to be (strict or non-strict) inequalities. Totality can be expressed as a clause x < y ∨ y ≤ x or x ≤ y ∨ y ≤ x. By T A we denote the set of these two clauses. They can be used to transform negative inequalities into positive ones: replace x ≮ y by y ≤ x and x ≰ y by y < x. Thus, we only need to consider disjunctions of positive inequalities.

We build the irreflexivity and transitivity properties directly into the inference mechanism.

Irreflexivity Resolution:

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

where σ is the most general unifier of s and t and sσ < tσ is maximal in Cσ.

Maximal Chaining:

\frac{C , u_{1}⊲_{1}s_{1}, …, u_{m}⊲_{m}s_{m} D , t_{1}⊲′_{1}v_{1}, …, t_{n}⊲′_{n}v_{n}}{Cσ , Dσ , ⋁_{1≤i≤m,1≤j≤n} u_{i}σ ⊲_{i,j} v_{j}σ}

where (i) σ is the most general unifier of s_{1}, …, s_{m}, t_{1}, …, t_{n} and ⊲_{i,j} is the highestpriority symbol of ⊲_{i} and ⊲′_{j}, (ii) u_{i}σ ⪰̸ s_{1}σ, for all 1 ≤ i ≤ m, and uσ ⪰̸ s_{1}σ, for all terms u in C, and (iii) v_{i}σ ⪰̸ t_{1}σ, for all 1 ≤ i ≤ n, and vσ ⊁ t_{1}σ, for all terms v in D, and t_{1}σ occurs in Dσ only in inequalities v ⊲ t_{1}σ.

For example, from x < f(a) ∨ b < f(x) and f(y) < c ∨ f(a) < d we may deduce a < c ∨ a < d ∨ b < c ∨ b < d (assuming f(a) is the maximal term in the clause).

The conclusion of a maximal chaining inference can also be obtained by a sequence of m × n ordinary chaining inferences, interspersed with factoring inferences; but an important difference is that with maximal chaining the intermediate clauses need not be deduced. In this regard, the effect of maximal chaining is similar to that of hyperresolution. Chaining inferences are restricted to the maximal terms in a clause; maximal chaining is designed to eliminate these terms.

The inference system MC^{≻} consisting of irreflexivity resolution and maximal chaining represents our basic inference mechanism for total orderings. (We also assume that the premises of an inference have no variables in common; if necessary, the variables in one premise are renamed.) Below we shall outline further improvements to the calculus for richer structures, such as dense total orderings without endpoints. These improvements ultimately derive from the concept of redundancy (of clauses and inferences) discussed in the next section.

3.2 Redundancy

Simplification and deletion techniques, such as subsumption, tautology deletion, condensement, demodulation, contextual rewriting, etc., have proved to be indispensable for actual implementations of theorem provers. We have developed a framework, based on the notion of redundancy, for formalizing and reasoning about such techniques (Bachmair and Ganzinger 1994). The main ideas are sketched below.

Let ≻ be a well-founded ordering on clauses and N and S be sets of clauses. We say that a ground instance Cσ of some clause C (which need not be an element of N) is S-redundant with respect to N if there exist ground instances C_{1}σ_{1}, …, C_{k}σ_{k} of N such that Cσ is true in every S-model of C_{1}σ_{1}, …, C_{k}σ_{k} and Cσ ≻ C_{j}σ_{j}, for all j with 1 ≤ j ≤ k. The clause C is S-redundant if all its ground instances are.

Tautologies are S-redundant in this sense, for any set S, and most cases of proper subsumption are also covered by this notion of redundancy.^{4} According to the definition, the axioms in S are all S-redundant. We are interested in P O-redundancy. (Since these axioms are built into the chaining mechanism, we expect them to be redundant.)

If an inference system is in a certain sense compatible with this notion of redundancy, then redundant formulas can be ignored by inferences. A ground inference (i.e., an inference in which the premises and the conclusion are ground clauses) is called simplifying (with respect to ≻) if its conclusion is smaller than its maximal premise. A non-ground inference is simplifying if all its ground instances are. We next define a suitable well-founded ordering on ground (instances of) clauses, with respect to which irreflexivity resolution and maximal chaining are simplifying. It is not difficult to find such an ordering; the reason we present one that is relatively complicated is that we apply the same ordering to variable elimination and superposition inferences.^{5}

The clause ordering is based on an ordering on literals. Let L be a literal u ⊴ v or ¬(u ⊴ v) in a ground instance Cσ of a clause C. We have to distinguish between positive and negative literals; let s_{L} be 1 if L is a negative literal, and 0 otherwise. We shall compare literals primarily by looking at their terms; let max_{L} be the maximal term, and min_{L} the minimal term of u and v. The argument position of the maximal term is also of importance; let p_{L} be 1 if L is an (strict or non-strict) inequality with max_{L} = u, and 0 otherwise. We need to distinguish between the different predicates; let r_{L} be 2 if L is a strict inequality, 1 if L is a non-strict inequality, and 0 otherwise. Finally, certain characteristics of the clause C are crucial for dealing with variable elimination. Let n_{C} be the number of different variables occurring as an argument of an equality or 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. We define n_{L} = −1, if C is the totality axiom; n_{L} = 0, if ⊴ is ≈; and n_{L} = n_{C}, otherwise.^{6}

Now, with each literal L we associate the tuple (max_{L}, s_{L}, p_{L}, n_{L}, r_{L}, min_{L}), and compare such tuples using the ordering ≻ in the first and last component, and the usual ordering on natural numbers in the other components. The corresponding ordering on literals is also denoted by the symbol ≻. Its multiset extension is an ordering on ground (instances of) clauses.

For example, if s ≻ t, we associate with an occurrence of a literal s < t in a ground instance of C the tuple (s, 0, 1, n_{C}, 2, t); with t ≮ s the tuple (s, 1, 0, n_{C}, 2, t); and with s ≤ s the tuple (s, 0, 1, n_{C}, 1, s).

4The definition of redundancy does not, for instance, cover cases where two clauses subsume each other.

5This ordering is the key to our refutational completeness proofs.

6We shall see that the number n_{C} decreases under variable elimination. The totality axiom is needed to justify variable elimination; its special role is reflected in the ordering.

It can easily be checked that irreflexivity resolution or maximal chaining inferences are simplifying with respect to this clause ordering. (In the case of irreflexivity resolution, one literal is removed and the number n_{C} can only decrease. In the case of maximal chaining, the maximal term occurs as the first argument of an inequality in the maximal premise, whereas in the conclusion it may occur only as the second argument of an inequality, if at all.)

A ground inference with conclusion B and maximal premise C is called S-redundant with respect to N if either some premise is S-redundant, or else there exist ground instances C_{1}, …, C_{k} of N such that B is true in every S-model of C_{1}, …, C_{k} and C ≻^{c} C_{j}, for all j with 1 ≤ j ≤ k. A non-ground inference is called S-redundant if all its ground instances are S-redundant.

We say that a set of clauses N is saturated up to S-redundancy if all inferences from N are S-redundant. Since the inferences in MC^{≻} are simplifying, they can be rendered redundant by adding the conclusion to the given set of clauses. Thus, computing the closure of a clause set under these inferences yields a saturated set.

3.3 Refutational completeness

We claim that if a set N is saturated up to P O-redundancy under MC^{≻}, then it either contains the empty clause or has a total ordering as model. Our approach for proving this claim is straightforward. We define a (transfinite) sequence of “partial” interpretations, one for each ground instance of a clause in N, beginning with the “empty” interpretation and considering clauses in increasing order according to the given well-founded ordering ≻. Whenever a clause C is false in the current partial interpretation I_{C}, we extend I_{C} by adding an inequality of C that extends the ordering described by I_{C} in a least restrictive way. The clause C is satisfied in the extended interpretation.

Let us first formally define which inequality is chosen from C to extend an interpretation I. Let C be a ground clause with maximal term s and I be an interpretation. By P_{I}(C) we denote some inequality s ⊲ t or t ⊲ s in C, such that (i) P_{I}(C) is an inequality s ⊲ t, if C contains any inequality s ⊲′ t′ at all; (ii) if P_{I}(C) is an inequality s ⊲ t, there is no inequality s ⊲′ t′ in C, such that either t < t′ is true in I or else t ≤ t′ is true in I and ⊲′ has lower priority than ⊲; (iii) if P_{I}(C) is an inequality t ⊲ s, there is no inequality t′ ⊲′ s in C, such that either t′ < t is true in I or else t′ ≤ t is true in I and ⊲′ has lower priority than ⊲.

For example, suppose a ≻ b ≻ c and let C be the clause a < b ∨ a < c. If b < c is true in I, then P_{I}(C) is a < c. Extending I by a < b yields a non-minimal extension of I to a model of C, as a < c follows from a < b and b < c by transitivity.

Now, for every ground instance C of a clause in N, let R_{C} be the set ⋃_{C≻D} E_{D} and I_{C} the rewrite closure of R_{C}. If C is false in I_{C} and does not contain s < s, where s is the maximal term in C, then E_{C} = {P_{I_{C}}(C)}. In all other cases, E_{C} = ∅. We say that C produces P_{I_{C}}(C), and call C productive, if E_{C} = {P_{I_{C}}(C)}. By I^{C} we denote the rewrite closure of R_{C} ∪ E_{C}. Finally, by R we denote the set ⋃_{C} E_{C} and by I the rewrite closure of R.

Evidently, a productive clause C is false in I_{C}, but true in I^{C}. The key properties of the interpretations I_{C} are summarized in the following lemma.

Lemma 2 Let N be a set of clauses that is saturated up to P O-redundancy but does not contain the empty clause. Let I be the interpretation constructed from all ground instances of N ∪ T A. Then for every ground instance C of a clause in N ∪ T A we have:

(1) if C is productive it is non-redundant;

(2) I^{C} satisfies P O; and

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

Proof. We use induction on ≻. Let C be a ground instance of a clause in N, such that the assertion holds for all smaller ground instances of N.

(1) The induction hypothesis may be used to show that I_{C} is a partial ordering and all ground instances of N and the totality axioms that are smaller than C are true in I_{C}. Therefore, if C were P O-redundant it would have to be true in I_{C}. But as a productive clause C is false in I_{C}.

(2) To prove that I^{C} is a transitivity interpretation, it suffices, by Lemma 1, to show that all peaks in I^{C} commute. By the induction hypothesis, peaks in I_{C} commute. Suppose there is a peak u_{1} ⊲′_{1} s ⊲_{1} v_{1} in I^{C} that is not also a peak in I_{C}. Then s ⊲_{1} v_{1} must be produced by C, so that C can be written as C′ ∨ s ⊲_{1} v_{1} ∨ ⋯ ∨ s ⊲_{n} v_{n}, where C′ contains no inequality s ⊲′ v and v_{j} ≤ v_{i} is true in I_{C}, for all i and j with i < j. The inequality u_{1} ⊲′_{1} s on the other hand must be produced by some smaller clause D of the form D′ ∨ u_{1} ⊲′_{1} s ∨ ⋯ ∨ u_{m} ⊲′_{m} s, where the maximal term s does not occur in D′ and u_{i} ≤ u_{j} is true in I_{C}, whenever i < j. We have to show that there is a rewrite proof of u_{1} ⊲ v_{1} in I^{C}, where ⊲ is the highest-priority symbol of ⊲′_{1} and ⊲_{1}.

Let us first assume that C is a ground instance v_{1} ≤ s ∨ s < v_{1} or v_{1} < s ∨ s ≤ v_{1} of a totality axiom. We consider the first case, the second is similar. Take the smaller ground instance v_{1} ≤ u_{1} ∨ u_{1} < v_{1} of the totality axiom, which by the induction hypothesis is true in I_{C}. We know that u_{1} ≤ s is true in I^{D}, and hence in I_{C}. If v_{1} ≤ u_{1} were true in I_{C}, then v_{1} ≤ s would also have to be true in (the partial ordering) I_{C}, which contradicts the assumption that C, as a productive clause, is false in I_{C}. In short, we may infer that u_{1} < v_{1} is true in I_{C}.

Let us therefore assume that C is not an instance of T A. Since D cannot be an instance of T A either, the clause

C′′ = C′ ∨ D′ ∨ ⋁_{1≤i≤m,1≤j≤n} u_{i} ⊲_{i,j} v_{j},

where ⊲_{i,j} is the highest-priority symbol of ⊲′_{i} and ⊲_{j}, is the conclusion of a maximal chaining from ground instances of N. By saturation up to redundancy and part (1), C′′ must follow from P O and ground instances of N smaller than C. By the induction hypothesis, all of these clauses, and hence C′′, are true in I_{C}. On the other hand, C is productive, so that C and C′ are false in I_{C}. Similarly, D′ is false in I_{D} and remains false in I_{C}. (Inequalities produced by a clause D̃ ≻ D have a maximal term s̃ ⪰ s and therefore cannot contribute to any rewrite proof of an inequality in D′.) We may thus infer that some disjunct u_{i} ⊲_{i,j} v_{j} is true in I_{C}. Moreover, both u_{1} ≤ u_{i} and v_{j} ≤ v_{1} are true in I. Thus, if ⊲ is ≤ or if ⊲_{i,j} is <, we are done. Suppose ⊲ is < (so that either ⊲_{1} or ⊲′_{1} is <) and ⊲_{i,j} is ≤ (so that both ⊲′_{i} and ⊲_{j} are ≤). We distinguish two subcases.

If u_{1} < s is true in I_{C}, then we may use (part (iii) of) the definition of P_{I_{C}}(C) to infer that u_{i} ≤ u_{1} is false in I_{C}. By the induction hypothesis, the ground instance u_{1} < u_{i} ∨ u_{i} ≤ u_{1} of T A is true in I_{C}, which implies that u_{1} < u_{i}, and hence u_{1} < v_{1}, is true in I_{C}.

If s < v_{1} is true in I_{C}, then we may use (part (ii) of) the definition of P_{I_{C}}(C) to infer that s ≤ v_{j} is false in I_{C}. The ground instance v_{j} < s ∨ s ≤ v_{j} of T A is smaller than C,^{7} so that by the induction hypothesis we may infer that v_{j} < s is true in I_{C}. Again this implies that u_{1} < v_{1} is true in I_{C}.

To show irreflexivity of < let us assume that u is the smallest term for which u < u is true in I^{C}. Since u < u cannot be produced by any clause, there must exist a rewrite proof u ⊲^{L} ⋯ ⊲^{L} v ⊲^{R} ⋯ ⊲^{R} u in I^{C}. We may use transitivity to infer that v < v is also true in I^{C}, but as u ≻ v this contradicts the assumption that u is the smallest term with this property.

The remaining axioms of P O are satisfied for any rewrite closure.

(3) If C is redundant, it follows from P O and smaller ground instances of N. By the induction hypothesis, all these clauses are true in I_{C}, hence C is true in I_{C} (and I^{C}). If C is productive, it is evidently true in I^{C}, as E_{C} ⊆ I^{C}. If C is not productive, it is either true in I_{C}, or else is of the form C′ ∨ s < s, where s is the maximal term in C. Since N is saturated up to redundancy, the irreflexivity resolution inference

\frac{C′ , s < s}{C′}

is redundant. In other words, C′ follows from P O and clauses smaller than C. We may use the induction hypothesis to infer that C′ is true in I_{C}. □

We now obtain the following refutational completeness result.

Theorem 1 Let N be a set of clauses with subset EE_{F}, where F is the given set of function symbols. If N is saturated up to P O-redundancy with respect to MC, then it has a total ordering as model if and only if it does not contain the empty clause.

Proof. If N contains the empty clause, it has no model. Suppose N does not contain the empty clause. Let I be the interpretation constructed from all ground instances of N ∪ T A. We may use Lemma 2 to show that I is a model of N ∪ P O ∪ T A, and hence satisfies all clauses specifying a total ordering. □

This theorem applies to arbitrary total orderings. The chaining mechanism can be improved for more specific theories, such as dense total orderings without endpoints.

3.4 Variable elimination

A variable chaining is a maximal chaining in which one of the terms s_{i} or t_{j} is a variable. Variable chaining can be quite prolific, as the unification of terms required for an inference always succeeds if the terms are variables. Fortunately, the ordering constraints in conditions (ii) and (iii) considerably cut down on the number of variable chainings. More specifically, the ordering constraints can only be satisfied if each term s_{i} or t_{j} is either a non-variable or an unshielded variable; that is, a variable that does not occur in a subterm f(…, x, …). For example, the variable x is unshielded in a < x ∨ x < b. 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.

7The fourth component n_{L} in the tuples associated with literals is crucial at this point.

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}}

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. 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} t_{i} < 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. (The equation a ≈ s(b) can be translated into a conjunction of inequations or, alternatively, one may use the equational inference systems described in the next section.)

Lemma 3 (i) A clause C ∨ x ≤ x is P O-redundant with respect to any set of clauses.

(ii) A clause C ∨ x < x is P O-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 is P O-redundant with respect to any set N that contains C′′ and the totality axioms.

Proof. (i) A clause C ∨ x ≤ x is satisfied in any partial ordering and hence is P Oredundant.

(ii) Observe that C ∨ x < x is true in any model of C and that C is smaller than C ∨ x < x.

(iii) We sketch the main ideas. 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_{C′} > n_{C′′}. 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, so that the tuple associated with L′ is bigger than the tuple associated with L′′ in one of the first four components. In short, we have D′ ≻ D′′.

Let T_{a} be the set of all disjunctions c < a_{i} ∨ a_{i} ≤ c and a_{i} < c ∨ c ≤ a_{i}; and let T_{b} be the set of all disjunctions c < b_{j} ∨ b_{j} ≤ c and b_{j} < c ∨ c ≤ b_{j}. All of these disjunctions are ground instances of the totality axioms. It can be shown that D′ is true in every model of T R ∪ A ∪ {D′′} and in every model of T R ∪ 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′. In sum, D′ is T R-redundant with respect to T A ∪ {D′′}. □

The lemma not only indicates that variable elimination 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. The variable elimination rules may therefore be called simplification rules: their premises can be replaced by the respective conclusion. In other words, variable elimination can be made mandatory, in that 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 variable elimination with other chaining systems has been shown by Richter (1984) and Hines (1992).

By CV^{≻} we denote the calculus consisting of irreflexivity resolution and maximal chaining plus variable elimination. Also, let DO(d, l, r) denote the set P O plus all clauses

x < y → x < d(x, y)
x < y → d(x, y) < y
→ l(x) < x
→ x < r(x)

which encodes the properties of a dense ordering without endpoints.

Lemma 4 Let N be a set of clauses that is saturated up to P O-redundancy with respect to MC and contains EE_{F} as a subset, where F is the given set of function symbols. If N contains no unshielded variables, then N ∪ DO(d, l, r) is also saturated up to P Oredundancy, where d, l and r are function symbols not in F.^{8}

Proof. The only possible inferences between clauses in N and DO(d, l, r) would be variable chainings, of which there are none, as there are no clauses with unshielded variables. Inferences from P O are trivially P O-redundant. 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 are also redundant in N and hence in N ∪ DO(d, l, r). In short, N ∪ DO(d, l, r) is saturated. □

The significance of this lemma rests on the fact that with variable elimination it is possible to eliminate clauses with unshielded variables. Clauses C ∨x ≤ x are redundant, whereas a clause C ∨ x < x with unshielded variable x becomes redundant once C has been deduced by irreflexivity resolution. (This is the only situation in which irreflexivity resolution needs to be applied to a clause C ∨ s < t, where s or t is a variable.) All other unshielded variables can be eliminated by variable elimination. In the next section we briefly discuss the main aspects of the saturation process; for further details see (Bachmair and Ganzinger 1994).

3.5 Saturation

Theorem proving may be viewed as a process of saturating a given set of clauses. A theorem proving derivation is a (possibly infinite) sequence S_{0}, S_{1}, … of clause sets, such that each set S_{i+1} is obtained from its predecessor S_{i} either by deleting some redundant clauses, or by adding (one or more) conclusions of inferences, the premises of which are in S_{i}. The limit S_{∞} of such a derivation is the set ⋃_{i} ⋂_{j≥i} S_{j} of all persisting clauses.

A theorem proving derivation is said to be fair if the every conclusion of an inference, the premises of which are in S_{∞}, is contained in some set S_{i}. A fair derivation can be constructed by systematically applying inferences to persisting formulas.

8The function symbols d, l, and r are Skolem symbols for which no equality axioms are needed (Bledsoe, Kunen and Shostak 1985).

Note that fairness imposes no restriction on deletion of redundant formulas. If variable elimination is applied exhaustively, no clause with an unshielded variable persists. In other words, the limit of such a derivation contains no clauses with unshielded variables.

We have the following theorem, cf. (Bachmair and Ganzinger 1994).

Theorem 2 The limit of a fair theorem proving derivation is saturated up to redundancy.

In sum, any theorem prover based on maximal chaining is refutationally complete, provided the inference rules are applied in a fair way, as defined above.

4 Chaining with superposition

The chaining calculus described above requires explicit equality axioms. Equality can also be built in via paramodulation (originally introduced by Robinson and Wos 1969), which in fact may be seen as a form of “subterm chaining” (as discussed in Bachmair and Ganzinger 1993). We now allow all three symbols ≈, < and ≤ to occur in clauses. This is logically redundant as ≤ can be expressed as a disjunction in ≈ and <, but from a practical point of view, and as was confirmed by our experimentation with the Saturate system, it is more appropriate to handle the three relations simultaneously and specifically so as to avoid duplication of terms as much as possible.^{9} For the same reason we allow negative equalities s ≉ t that would otherwise have to be transformed into disjunctions s < t∨t < s. Thus, clauses may contain positive and negative equalities in addition to positive inequalities.

Totality can be expressed as a clause T E

x < y ∨ y < x ∨ x ≈ y

and the anti-symmetry axiom AS

x ≤ y , y ≤ x → x ≈ y

specifies the relationship between equality and inequality.

The calculus CS consists of three parts: a chaining calculus for inequalities, a superposition calculus for equalities, and further chaining rules that connect equalities with inequalities. Superposition is a form of paramodulation in which ordering constraints are imposed on the inference rules. We use the superposition calculus of Bachmair and Ganzinger (1994). Symmetry of equality is built in as an inference rule

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

where u or v is a maximal term in the premise. (In practice, equations are usually considered as unordered pairs to avoid unnecessary duplication of formulas.)

9Testing the solvability of ordering constraints for the lexicographic path ordering is NP-complete in the number of terms that are involved in an inference (Nieuwenhuis 1993) and may easily become a bottleneck in practice.

Reflexivity Resolution:

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

where σ is a most general unifier of u and v and uσ ≉ vσ is a maximal literal in Cσ.

Superposition:

\frac{C , t ≈ s D , L′[s′]}{Cσ , Dσ , L[t]σ}

where (i) σ is a most general unifier of s and s′; (ii) tσ ≈ sσ is strictly maximal in Cσ and tσ ⪰̸ sσ; (iii) L′ is either an equality u[s] ≈ v or v ≈ u[s], or the negation thereof, such that vσ ⪰̸ uσ and L′σ is strictly maximal in Dσ, if it is a positive equality, and just maximal in Dσ if it is negative; and (v) s′ is not a variable.

Equality Factoring:

\frac{C , t ≈ s , t′ ≈ s′}{Cσ , tσ ≉ t′σ , t′σ ≈ s′σ}

where (i) σ is a most general unifier of s and s′, (ii) tσ ⪰̸ sσ, and (iii) sσ ≈ tσ is maximal in (C ∨ s ≈ t ∨ s′ ≈ t′)σ.

Superposition is a restricted form of subterm chaining applied to equations. We need a similar form of “maximal subterm chaining” with equations into inequations. These inference rules are designed to reduce maximal terms.

Equality Chaining Left:

\frac{C , u ≈ s D , t_{1}[s_{1}]_{p}⊲_{1}v_{1}, …, t_{n}[s_{n}]_{p}⊲_{n}v_{n}}{Cσ , Dσ , t_{1}[u]_{p}⊲_{1}v_{1}, …, t_{n}[u]_{p}⊲_{n}v_{n}}

where (i) σ = ρτ with ρ the most general unifier of s, s_{1}, …, s_{n}, and τ the most general unifier of t_{1}[s_{1}]ρ, …, t_{n}[s_{n}]ρ, (ii) uσ ⪰̸ sσ, and uσ ≈ sσ is strictly maximal in Cσ, (iii) v_{i}σ ⪰̸ t_{1}σ, for all 1 ≤ i ≤ n, and vσ ⊁ t_{1}σ, for all terms v in D, and t_{1}σ occurs in Dσ only in equalities or inequalities v ⊴ t_{1}σ, and (iv) none of the s_{i} is a variable.

Equality Chaining Right:

\frac{C , u ≈ s D , v_{1}⊲_{1}t_{1}[s_{1}]_{p}, …, v_{n}⊲_{n}t_{n}[s_{n}]_{p}}{Cσ , Dσ , v_{1}⊲_{1}t_{1}[u]_{p}, …, v_{n}⊲_{n}t_{n}[u]_{p}}

where (i) σ = ρτ with ρ is the most general unifier of s, s_{1}, …, s_{n}, τ the most general unifier of t_{1}[s_{1}]ρ, …, t_{n}[s_{n}]ρ, (ii) uσ ⪰̸ sσ, and uσ ≈ sσ is strictly maximal in Cσ, (iii) v_{i}σ ⪰̸ t_{1}σ, for all 1 ≤ i ≤ n, and vσ ⊁ t_{1}σ, for all terms v in D, and t_{1}σ occurs in Dσ only in equalities, and (iv) none of the s_{i} is a variable.

Finally, we also need to be able to deduce equalities implicitly specified by inequalities, so that the anti-symmetry axiom is satisfied. For that purpose we modify the maximal chaining rule as follows.

Inequality Chaining:

\frac{C , u_{1}⊲_{1}s_{1}, …, u_{m}⊲_{m}s_{m} D , t_{1}⊲′_{1}v_{1}, …, t_{n}⊲′_{n}v_{n}}{Cσ , Dσ , ⋁_{1≤i≤m,1≤j≤n} ineq(i, j)}

where (i) σ is the most general unifier of s_{1}, …, s_{m}, t_{1}, …, t_{n}, (ii) ineq(i, j) is the strict inequality u_{i}σ < v_{j}σ if ⊲_{i} or ⊲′_{j} is <, and the disjunction u_{i}σ < v_{j}σ ∨ u_{i}σ ≈ t_{1}σ otherwise,^{10} (iii) u_{i}σ ⪰̸ s_{1}σ, for all 1 ≤ i ≤ m, and uσ ⪰̸ s_{1}σ, for all terms u in C, and (iv) v_{i}σ ⪰̸ t_{1}σ, for all 1 ≤ i ≤ n, and vσ ⊁ t_{1}σ, for all terms v in D, and t_{1}σ occurs in Dσ only in inequalities v ⊲ t_{1}σ.

For example, from a ≤ f(x) and f(a) ≤ b ∨ f(y) < c we may deduce a < b ∨ f(a) ≈ a ∨ a < c (assuming f(a) is the maximal term in the clause). Inequality chaining is like maximal chaining, except that when two non-strict inequalities are chained we split the resulting non-strict inequality into a strict inequality and an equality.

The calculus CS consists of the above inference rules plus irreflexivity resolution. (Maximal chaining is replaced by inequality chaining.) It can easily be shown that all inference rules in CS are simplifying. To prove the refutational completeness proof of CS we use the same approach as for MC, but have to modify the definition of the interpretations I_{C} and I. Let I be an interpretation. A ground term t is said to be reducible with respect to I if we have t ≈_{I}^{L} s (or equivalently s ≈_{I}^{R} t), for some term s. Terms that are not reducible are said to be irreducible.

Let C be a ground clause with maximal term s and I be an interpretation. Let P_{I}(C) be an inequality s < t if C contains s ⊲ t and t < t′ is false in I, for any inequality s ⊲ t′ in C; and let P_{I}(C) be t < s if C contains t ⊲ s, but no inequality s ⊲ u, and t′ < t is false in I, for any inequality t′ ⊲ s in C.

Let N be a set of ground clauses and C be a clause in N with maximal term s. As before, let R_{C} be the set ⋃_{C≻D} E_{D} and I_{C} the rewrite closure of R_{C}. The set E_{C} is defined as follows:

• If s occurs in a negative literal in C or else is reducible with respect to I_{C}, then E_{C} = ∅. (For the remaining cases, we assume that s is irreducible and occurs only in positive literals.)

• If C is false in I_{C} and contains some inequality s ⊲ t or t ⊲ s, but not s < s, then E_{C} = {P_{I_{C}}(C)}.

• If C is false in I_{C} and can be written as C′∨s ≈ t, where s ≈ t is a strictly maximal literal and C′ is false in the rewrite closure of R_{C} ∪ {s ≈ t}, then E_{C} = {s ≈ t}.

• Otherwise, E_{C} = ∅.

Again, we call C productive if E_{C} ≠ ∅. By I^{C} we denote the rewrite closure of R_{C} ∪ E_{C}. Finally, by R we denote the set ⋃_{C} E_{C} and by I the rewrite closure of R.

The key properties of the interpretation I are summarized in the following lemma.

Lemma 5 Let N be a set of clauses that is saturated up to P O-redundancy under CS and contains EE as a subset, but does not contain the empty clause. Let I be the interpretation constructed from all ground instances of N ∪ T E. Then for every ground instance C of a clause in N we have:

10Multiple copies of an equation u_{i}σ ≈ t_{1}σ resulting from different inequalities t_{j} < v_{j} and t_{k} < v_{k} can of course be merged into one.

(1) if C is productive it is non-redundant;

(2) I^{C} satisfies P O;

(3) C is true in I^{C}. Furthermore, I is a model of the anti-symmetry axiom.

Proof. We use induction on ≻. Let C be a ground instance of a clause in N, such that the assertion is satisfied for all smaller ground instances of N.

(1) This part is the same as for Lemma 2.

(2) This part is similar to Lemma 2, except that we have to use inequality chaining instead of maximal chaining. We outline the differences between the two cases.

Transitivity, as we have seen, reduces to a commutation property. Let C be a clause C′ ∨ s ⊲_{1} v_{1} ∨ ⋯ ∨ s ⊲_{n} v_{n}, where C′ contains no inequality s ⊲′ v and v_{j} ≤ v_{i} is true in I_{C}, for all i and j with i < j; and let D be a clause D′ ∨ u_{1} ⊲′_{1} s ∨ ⋯ ∨ u_{m} ⊲′_{m} s, where D′ contains no inequality s ⊲ u or u ⊲ s and u_{i} ≤ u_{j} is true in I_{C}, whenever i < j. We assume that C produces s < v_{1} and D produces u_{i} < s, and have to show that there is a rewrite proof of u_{1} ⊲ v_{1} in I^{C}, where ⊲ is < if ⊲′_{1} or ⊲_{1} is <, and ≤ otherwise. Note that the term s must be irreducible with respect to I_{C} (for otherwise C cannot be productive).

We know that D is not an instance of T E. Let us first assume that C is not an instance of T E either. Then the clause

C′′ = C′ ∨ D′ ∨ ⋁_{1≤i≤m,1≤j≤n} u_{i} < v_{j} ∨ ⋁_{k∈K} u_{k} ≈ s

is the conclusion of an inequality chaining inference from ground instances of N. (Here K = ∅, if all symbols ⊲′_{i} are <, and K is the set of all indices k for which ⊲_{k} is ≤, otherwise.) The equations u_{k} ≈ s are all false in I_{C}, as s is irreducible and s ≻ u_{k}, for all k. Since C′ and D′ are also false in I_{C}, some strict inequation u_{i} < v_{j} is true in I_{C}, which implies that u_{1} < v_{1} is true in I_{C}.

Suppose C is a ground instance v_{1} < s ∨ s < v_{1} ∨ s ≈ v_{1} of a totality axiom in T E. By the induction hypothesis, the smaller ground instance v_{1} < u_{1} ∨ u_{1} < v_{1} ∨ u_{1} ≈ v_{1} is true in I_{C}. Since u_{1} < s is true, and v_{1} < s false in I_{C}, we may infer that both v_{1} < u_{1} and u_{1} ≈ v_{1} are false in I_{C}. Consequently, u_{1} < v_{1} must be true in I_{C}.

The remaining axioms in P O can be shown to be true in I_{C} in the same way as in the proof of Lemma 2.

(3) If C is productive, it is evidently true in I^{C}. Suppose C is non-productive. If C is false in I_{C}, then it must violate some other condition imposed on productive clauses. We distinguish according subcases.

(3.1) Suppose C is an instance Ĉσ of a clause Ĉ in N, such that xσ is reducible with respect to I_{C}, for some variable x in Ĉ. Let t be a ground term, such that xσ ≈_{I_{C}}^{L} t, and let τ be the same substitution as σ, except that xτ = t. Since Ĉσ ≻ Ĉτ, we may use the induction hypothesis to infer that C′ = Ĉτ is true in I_{C′}, and hence in I_{C}. But since xσ ≈ t is also true in I_{C}, and C′ differs from C only in that some occurrences of xσ are replaced by t, the clause C is also true in I_{C}.

For the remaining subcases we assume that C is a reduced ground instance Ĉσ of a clause in N in the sense that xσ is irreducible for all variables x in Ĉ.^{11}

(3.2) If C is of the form C′ ∨ s < s, the same arguments as in Lemma 2 apply.

11This assumption is needed for lifting subterm chaining inferences.

(3.3) If C is of the form C′ ∨ s ≉ s, we may adapt case (3.2) by using reflexivity resolution instead of irreflexivity resolution.

(3.4) If s is reducible with respect to I_{C}, we may apply superposition or equality chaining. We discuss one representative case.

Suppose C is of the form C′ ∨ s ≉ t, where s ≉ t is a maximal literal in C, s ≻ t, and s contains a subterm u, for some equation u ≈ v, with u ≻ v, produced by a clause D = D′ ∨ u ≈ v (smaller than C). By superposition we obtain C′′ = C′ ∨ D′ ∨ s[v] ≉ t from C and D. Since C and D are reduced ground instances of clauses Ĉ and D̂, respectively, the clause C′′ is a ground instance of the conclusion of a superposition inference from Ĉ and D̂. By saturation up to P O-redundancy, C′′ must logically follow from P O and ground instances of N smaller than C. Since all of these clauses are true in I_{C}, we may infer that C′′ is true in I_{C}, which implies that C is true in I_{C}.

(3.5) The only remaining case not yet covered is of a clause C = C′′ ∨ s ≈ t′ ∨ s ≈ t, where s is irreducible by R_{C} and t ≈ t′ is true in I_{C}. By equality factoring we obtain the clause C′′ ∨ t ≉ t′ ∨ s ≈ t′, which by saturation up to P O-redundancy is true in I_{C}. Consequently, C is also true in I_{C}, which completes the proof of part (3).

Finally, it is straightforward to show that all ground instances u ≤ v∨v ≤ u → u ≈ v are true in I. Suppose u ≤ v and v ≤ u are true in I, hence provable by rewrite proofs. Since R contains only equations or strict inequalities, each rewrite proof is either a proof of an equation or of a strict inequality. Since u < v is false (for otherwise irreflexivity is violated), we may conclude that there is a proof of u ≈ v. □

Using this lemma, we obtain the following completeness result.

Theorem 3 Let N be a set of clauses that is saturated up to P O-redundancy (with respect to CS). Then N has a total ordering with equality as a model if and only if it does not contain the empty clause.

The variable elimination rule applies as previously, but the presence of equality complicates matters somewhat. The elimination of literals x < x, x ≤ x, x ≈ x, and x ≉ x is obvious. To eliminate an unshielded variable x from a clause D we translate all (positive and negative) equalities with x into inequalities, and then apply the usual 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. The formula can be translated into 2^{n} clauses, to which the usual variable elimination rule can be applied. Let us denote by V E_{D} the set of all these clauses, with x eliminated. Unfortunately, some ground instances of clauses in V E_{D} may be larger than the corresponding ground instance of Dσ with respect to our clause ordering. Consequently, clauses are not necessarily rendered P Oredundant by variable elimination. However, those ground instances of D, in which x is instantiated to the maximal term in the clause, are P O-redundant.

Lemma 6 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 V E_{D} and the totality axioms.

To sum up these considerations, a clause with an unshielded variable x is not necessarily redundant, but inferences involving this variable (chaining through x, superposition from x, [ir]reflexivity resolution applied to [in]equalities with x) 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.

5 Summary

We have presented chaining-based inference systems for total orderings that extend previous work in several respects: we impose ordering constraints on chaining inferences; we build equality directly into the inference mechanism; and we establish refutational completeness in the presence of a notion of redundancy that covers such important simplification techniques as tautology deletion, subsumption, condensement, and demodulation. The completeness proofs of our results are conceptually simple. We deal with variable elimination as a simplification rule, separately from the chaining rules; an approach that better clarifies the connection between these essential components of chaining systems.

The improvements are not only of theoretical significance, as experimental evidence indicates that equational inference mechanisms, such as superposition and demodulation, are preferable to explicit axiomatizations of equality. Some form of equational reasoning appears to be used in the provers described by Bledsoe and Hines (1980), Hines (1988) and Hines (1990), and inference systems with equational reasoning capabilities may provide a better approximation to actual implementation practice than other chaining systems.

The superposition calculus, as described above, contains an explicit factoring rule for equalities, whereas maximal chaining implicitly encodes factoring for inequalities. An alternative to maximal chaining would be ordered chaining (as in Bachmair and Ganzinger 1993) with inequality factoring.

In algebraic structures such as ordered rings one may have axioms

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

that express monotonicity or anti-monotonicity properties of an ordering with respect to certain functions. The techniques we have discussed should be extended to such cases. An important question in this context is to what extent chaining through or below variables is necessary. Our techniques may also be useful in the context of chaining and variable elimination for set theory, an application that has been studied by Hines (1990).

References

L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In M. Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lecture Notes in Computer Science, vol. 449, pp. 427–441, Berlin, Springer-Verlag.

L. Bachmair and H. Ganzinger, 1993. Rewrite Techniques for Transitive Relations. Technical Report MPI-I-93-249, Max-Planck-Institut für Informatik, Saarbrücken.

L. Bachmair and H. Ganzinger, 1994. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, Vol. 4, No. 3, pp. 1–31. Revised Version of MPI-I-91-208, to appear.

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

W. W. Bledsoe and L. M. Hines, 1980. Variable Elimination and Chaining in a Resolutionbased Prover for Inequalities. In Wolfgang Bibel, Robert Kowalski, editors, 5th Conference on Automated Deduction, LNCS 87, pp. 70–87, Les Arcs, France, Springer-Verlag.

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

N. Dershowitz, 1987. Termination of Rewriting. Journal of Symbolic Computation, Vol. 3, pp. 69–116.

L. M. Hines, 1988. Hyper-chaining and knowledge-based theorem proving. In Proc. 9th Int. Conf. on Automated Deduction, Lecture Notes in Computer Science, pp. 469–486, Berlin, Springer-Verlag.

L. Hines, 1990. Str+^{.}ve⊆: The Str+^{.}ve-based Subset Prover. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, LNAI 449, pp. 193–206, Kaiserslautern, FRG, Springer-Verlag.

L. M. Hines, 1992. Completeness of a Prover for Dense Linear Logics. Journal of Automated Reasoning, Vol. 8, pp. 45–75.

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

J. Levy and J. Agustí, 1993. Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. In C. Kirchner, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 17–31, Berlin, Springer.

Robert Nieuwenhuis, 1993. Simple LPO constraint solving methods. Information Processing Letters, Vol. 47, pp. 65–69.

P. Nivela and R. Nieuwenhuis, 1993. Saturation of first-order (constrained) clauses with the Saturate system. In Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 436–440, Berlin, Springer-Verlag.

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

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

J. R. Slagle, 1972. Automatic theorem proving for theories with Built-in Theories Including Equality, Partial Orderings, and Sets. Journal of the ACM, Vol. 19, pp. 120–135.