Rewrite Techniques for Transitive Relations

Leo Bachmair^{∗} and Harald Ganzinger^{†}

Abstract

We propose inference systems for dealing with transitive relations in the context of resolution-type theorem proving. These 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 for transitive relations in general. If the given relation satisfies additional properties, such as symmetry, further restrictions are possible. In particular, we discuss (partial) equivalence relations and congruence relations.

1 Introduction

Transitive relations are indispensable for reasoning about programs; partial orderings and equality relations being representative examples widely used in computational logic. Although transitive relations can naturally be represented by term rewriting systems surprisingly little work has been devoted to the use of rewrite techniques for transitive relations in the context of resolution-based automated theorem provers. The techniques that have been developed apply to specific transitive relations, such as equality relations, and typically depend on additional properties. The concept of a convergent rewrite system, for instance, is of little interest for non-symmetric relations.

In this paper, we show that in the absence of symmetry the more general concept of commutation of two rewrite systems is of the same fundamental importance for reasoning about general transitive relations as is confluence for the particular case of equality.

Confluence admits equalities to be proved via normalization by rewriting. Commutation provides us with a similar notion of rewrite proofs for inequalities. In the case of equality, the concept of rewrite proofs leads to ordering restrictions by which paramodulation inferences (which essentially encode the transitivity and congruence properties of equality) can be effectively controlled. Having a notion of rewrite proofs for general transitive relations will allow us to attach similar ordering restrictions to chaining inferences that just encode transitivity alone. If < is a transitive relation, chaining allows one to derive uσ < vσ from u < s and t < v, where σ is a most general unifier of s and t. In “ordered chaining” we first compare the term sσ (which is identical to tσ) to both uσ and vσ (using a given simplification ordering on terms) and perform the chaining inference only if sσ is maximal. The systematic application of ordered chaining to a set of inequations corresponds to a completion process, aimed at obtaining a description of the given transitive relation as a “rewrite closure.”

The results of the present paper may be summarized as follows. We propose to represent sets of inequations by rewrite systems and show that commutation properties lead to the existence of rewrite proofs for derivable inequalities. We present an inference system for first-order clauses based on ordered chaining that is refutationally complete in the presence of a general notion of global redundancy by which the usual simplification techniques (tautology deletion, subsumption, etc) can be justified. The gain in efficiency with an ordered system over the unordered variants of chaining that have been proposed in the literature are comparable to the improvements achieved by superposition over unrestricted paramodulation.

In practical applications an especially prolific form of chaining, called variable chaining (where s or t is a variable x), needs to be avoided as much as possible. We present several results in this direction. First of all, ordered chaining considerably cuts down the number of possible variable chainings right away, 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 <, but not as an argument of a function symbol or any other predicate symbol). Unfortunately, some variable chainings are needed for transitive relations in general. Some positive results that we have obtained are based on syntactic properties of clauses, such as the linearity of x, but additional logical properties can have a greater effect in this respect. Thus, we show that in the presence of symmetry almost all forms of variable chainings are redundant. This generalizes known results for equality to arbitrary partial (not necessarily reflexive) equivalence relations. (Properties other than symmetry can have a similar effect, though for different reasons. An important example we have investigated with the techniques presented here are total orderings; see Bachmair and Ganzinger 1993a.)

∗Department of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794, U.S.A, leo@cs.sunysb.edu

†Max-Planck-Institut für Informatik, Im Stadtwald, D-66123 Saarbrücken, Germany, hg@mpi-sb.mpg.de

We also consider (partial) congruence relations and obtain a refutationally complete inference system based on ordered subterm chaining which specializes to known superposition calculi for equality. Finally, we present examples of non-symmetric and monotone transitive relations for which ordered subterm chaining is incomplete if chaining below variables is not admitted. How to avoid chaining below variables for particularly interesting theories of this kind (e.g., fragments of set theory or ordered fields) appears to be an important problem for future research.

In summary, our results cover a wide spectrum of binary relations spanned by arbitrary combinations of transitivity with reflexivity, irreflexivity, symmetry and monotonicity properties, and provide refutationally complete chaining inference systems for the various cases together with a theoretical foundation based on term rewriting.

2 Transitive Relations

The main question we consider in this paper is the satisfiability of sets of clauses^{1} in first-order languages with transitive relations, that is, predicates < that satisfy

x < y, y < z → x < z.

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

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

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

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

and so on. Certain refinements of resolution provide better control and exclude such problematic selfresolutions. For instance, if we select the two negative literals in the transitivity axiom, we get inferences

\frac{C , u < s D , t < v x ≮ y , y ≮ z , x < z}{Cσ , Dσ , uσ < 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 (1994). Thus we may encode transitivity as an inference rule:

Chaining:

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

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

This chaining rule (originally proposed by Slagle 1972) is not completely satisfactory, though, as it explicitly generates the transitive closure of the binary relation described by >. For example, from just a single clause x < s(x) chaining generates infinitely many clauses x < s^{n}(x). In refutational theorem provers only finitely many of these clauses are needed for any possible refutation.

For example, suppose < denotes a strict partial ordering, specified by a set of unit clauses u < v plus the transitivity axiom and the irreflexivity axiom x ≮ x. Such a clause set is contradictory if, and only if, there exists a sequence, more specifically a cycle, of ground terms u_{1} < ⋯ < u_{n} = u_{1}. The existence of a cycle u_{1} < u_{1} can be easily checked by inspecting the given clauses, while longer cycles can be shortened by chaining; that is, from u_{i−1} < u_{i} and u_{i} < u_{i+1} we obtain u_{i−1} < u_{i+1} and a shorter cylce. However, there are n − 2 different chaining inferences to shorten a cycle of length n, any single one of which would achieve the same purpose. To eliminate such redundancies in the chaining process, we use a measure of the syntactic complexity of a term and select only those chainings in which the term u_{i} is more complex than u_{i−1} and u_{i+1}. This refinement of chaining can be conveniently formalized in terms of rewrite techniques, which we describe next.

3 Rewrite Techniques

An (Herbrand) interpretation is a set I of ground atomic formulas. We say that a ground 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. (The empty clause is false in every interpretation.) A non-ground clause is true in I if all its ground instances are true. 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. We speak of a transitivity interpretation if the transitivity axiom is satisfied.

1A clause is a finite multiset of literals; a literal being either an atomic formula A (a positive literal) or the negation ¬A thereof (a negative literal).

Let < be a binary predicate that is assumed to denote a transitive relation. Literals u < v and u ≮ v are called inequations. We are interested in certain extensions of a Herbrand interpretation I to a transitivity interpretation. We say that u < v is provable if there exists a sequence u = u_{0} < u_{1} … u_{n−1} < u_{n} = v, where n ≥ 1 and u_{i−1} < u_{i} is in I, for all i. The transitive closure of I is the set of all atoms u < v provable in I.

Let now ≻ be a simplification ordering on ground terms.^{2} Inequations can often be oriented into rewrite rules. If u < v is an inequation in I we write u <^{L} v if u ≻ v, and u <^{R} v if v ≻ u. A rewrite proof is a sequence

u_{0} < u_{1}

or u_{0} <^{L} ⋯ <^{L} u_{m} <^{R} ⋯ <^{R} u_{n}.

By the rewrite closure of I we mean the set I plus all atoms u < v that are provable by a rewrite proof in I. Under certain circumstances, related to commutation properties of the rewrite relations <^{L} and <^{R}, the rewrite closure of a set I is a transitivity interpretation.

If a sequence u_{0} < ⋯ < u_{n} is not a rewrite proof then either (i) there is a subsequence u_{i−1} <^{R} u_{i} <^{L} u_{i+1}, or (ii) some terms u_{i−1} and u_{i} are incomparable or identical (i.e., u_{i−1} ⊁ u_{i} and u_{i} ⊁ u_{i−1}), for some i. A subsequence u <^{R} t <^{L} v, called a peak, is said to commute if u < v is provable by a rewrite proof. Commutation allows us to deal with case (i). If the simplification ordering ≻ is total on ground terms, then case (ii) applies to ground proofs only if u_{i−1} = u_{i}, for some i, in which case the sequence can be shortened by deleting 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, we get a <^{R} b and b <^{L} c and c <^{L} d, and 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 simplification ordering that is total on ground terms and I be a Herbrand interpretation. 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 it is provable by a rewrite proof. Consider a sequence u = u_{0} < ⋯ < u_{k} = v. If the sequence contains peak, then by commutation the peak can be replaced by a rewrite proof. Moreover, whenever u_{i−1} and u_{i} are identical and n > 1, then u_{i−1} < u_{i} can be eliminated from the sequence. The multiset of terms {u′_{0}, …, u′_{n}} used in the resulting new sequence u = u′_{0} < ⋯ < u′_{n} = v is smaller than the multiset {u_{0}, …, u_{k}} with respect to the (multiset extension of the) simplification ordering ≻. In other words, for any sequence that is not a rewrite proof we can obtain a simpler sequence. 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 transitive relations, 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.) Similar socalled “critical pair lemmas” form the basis of completion procedures; Levy and Agustí (1993) appear to have been the first to apply these techniques to nonsymmetric 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.

4 Ordered Chaining

4.1 Inference rules

Let ≻ be a simplification ordering that is total on ground terms. We combine the chaining rules for inequalities with an ordered resolution calculus, and for that purpose need to extend the ordering ≻ to literals. We assume that ≻ is well-founded, satisfies the subterm property (i.e., A[s] ≻ s, for all expressions A and proper subexpressions s of A), and is total on ground terms and ground atoms. We extend ≻ to a well-founded ordering on ground literals by associating with each such literal L a complexity measure (max_{L}, p_{L}, s_{L}, min_{L}) defined as follows. Let L be a literal A or ¬A. The second component p_{L} is ⊤, if L is negative, and ⊥ otherwise. If A is not an inequality, then max_{L} is A, and s_{L} and min_{L} are both ⊥. If A is an inequality u < v, then max_{L} denotes the maximal, and min_{L} the minimal, term of u and v; and s_{L} is ⊤ if the maximal term occurs as first argument and ⊥ otherwise. (We assume that ⊤ and ⊥ are new elements with ⊤ ≻ t ≻ ⊥, for all t.)

2A simplification ordering (on ground terms) is a wellfounded ordering with the following two properties: (i) t[u] ≻ t[v] whenever u ≻ v and (ii) t[s] ⪰ s, for all terms t, u, v, and s.

For example, if s ≻ t, then the complexity of s < t is (s, ⊥, ⊤, t), whereas the complexity of t ≮ s is (s, ⊤, ⊥, t). The complexity of s < s is (s, ⊥, ⊤, s). The resulting ordering is total on ground literals. Its extension to (finite) multisets, which we also denote by the same symbol, is well-founded and total on ground clauses.

We extend this ordering 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′σ. 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.

Our inference rules are parametrized with respect to the simplification ordering. The chaining rules are designed to establish commutation.

Ordered Chaining:

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

where σ is the most general unifier of s and t, uσ < sσ is strictly maximal in Cσ, tσ < vσ is strictly maximal in Dσ, uσ ⪰̸ sσ, and vσ ⪰̸ tσ.

Negative Chaining:

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

where σ is the most general unifier of u and t, uσ ≮ sσ is maximal in Cσ, tσ < vσ is strictly maximal in Dσ, vσ ⪰̸ tσ, sσ ⪰̸ uσ, and sσ ≠ vσ; and

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

where σ is the most general unifier of s and v, uσ ≮ sσ is maximal in Cσ, tσ < vσ is strictly maximal in Dσ, uσ ⪰̸ sσ, tσ ⪰̸ vσ, and uσ ≠ tσ.^{3}

The resolution rule applies to arbitrary literals.

Ordered Resolution:

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

where σ is the most general unifier of A and B, Aσ is strictly maximal in Cσ, and ¬Bσ is maximal in Dσ.

The calculus of all these inference rules,^{4} denoted by B_{<} (or B), is refutationally complete for Horn clauses.^{5} For the completeness proof we adapt the model construction approach of Bachmair and Ganzinger (1994).

Given a set N of ground clauses, we define a Herbrand interpretation I via induction on ≻. More precisely, we define for each ground clause C an interpretation I_{C}, intended to be a model for ground clauses smaller than C, and sets R_{C} and E_{C} that are designed to turn I_{C} into a model of C (in certain cases). Formally, for every clause C in N let R_{C} be the set ⋃_{C≻D} E_{D}, and I_{C} be the rewrite closure of R_{C}. Furthermore, if C is a clause C′ ∨ A, where A is a positive literal and A ≻ C′, 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. Otherwise, E_{C} = ∅. Finally, let R be ⋃_{C} E_{C} and I be the rewrite closure of R.

A set of (possibly non-ground) clauses N is saturated if it contains all conclusions of inferences from N. The interpretation I constructed for the set of all ground instances of N can be shown to be a transitivity interpretation and a model of N, whenever N is saturated.

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.

Lemma 2 If a ground Horn 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}.

Proof. The proof is straightforward, once one has observed that the ordering ≻ is 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. □

3The case sσ = vσ is covered by ordered resolution.

4We assume that the premises of an inference have no common variables. If necessary, the variables in one premise are renamed.

5A Horn clause is a clause with at most one positive literal.

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.

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) Both I^{C} and 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 ∈ C′, then B ∈ I_{C} ⊆ I, from which we conclude that C′ is false in I.

(2) By Lemma 1 it suffices to show that all peaks commute. Peaks that involve only R_{C} commute by the induction hypothesis, hence I_{C} is a transitivity interpretation. The assertion for I^{C} is trivially true if E_{C} contains no inequation, or if E_{C} = {t < v} where v ⪰ t. (For the latter case observe that, by definition of the ordering ≻, I_{C} cannot contain an inequation v < u.) Suppose C = C′ ∨ v < t produces v < t with v ≻ t. If there is another clause D = D′ ∨ u < v that produces u < v with v ≻ u, then there exists a peak u <^{R} v <^{L} t. But by ordered chaining we obtain from C and D the clause C′′ = C′ ∨ D′ ∨ u < t. Since N is saturated and C ≻ C′′ we may apply the induction hypothesis to infer that C′′ is true in I^{C′′}. But C′ ∨ D′ is false in I, so that u < t is true in I^{C′′}, and hence true in I^{C}, which 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 literal ¬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 false in I_{C} and hence false in I^{C′′}—which contradicts the induction hypothesis. The only remaining possibility is that A is true in the rewrite closure I_{C}. In other words, u < v is provable by a rewrite proof of length ≥ 2. In that case there exists a suitable productive clause D ∨ u < v′ (where v′ < v is true in I_{C}) or D ∨ u′ < v (where u < u′ is true in I_{C}), 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 interpretations I_{C} and I are transitivity interpretations. Let us denote by T_{<} the transitivity axiom for the predicate <. As an immediate corollary of the lemma we obtain:

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

Proof. If N contains the empty clause, N ∪ T_{<} 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 rewrite closure of R is a transitivity interpretation and that I is a model of N ∪ T_{<}. □

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; 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 arbitrary clauses. First, though, we describe a suitable concept of redundancy that is compatible with chaining.

4.2 Redundancy

We sketch the main ideas of an abstract notion of redundancy and refer to Bachmair and Ganzinger (1994) for further details.

Let N and E be sets of clauses and C be a ground clause (not necessarily a ground instance of N). We call C E-redundant with respect to N if there exist ground instances C_{1}, …, C_{k} of N such that C is true in every E-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. A non-ground clause is called E-redundant if all its ground instances are.

Tautologies are E-redundant in this sense, for any E, and most cases of proper subsumption are also covered by this notion of redundancy. The axioms in E are all E-redundant by definition (presumably they are built into the inference mechanism).

A ground inference with conclusion B and maximal premise C is called E-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 E-model of C_{1}, …, C_{k} and C ≻^{c} C_{j}, for all j with 1 ≤ j ≤ k. A non-ground inference is called Eredundant if all its ground instances are.

We say that a set of clauses N is saturated up to Eredundancy if all inferences from N are E-redundant.

For the remaining part of this section, redundancy is meant to refer to T_{<}-redundancy. One way to render an inference in B redundant is to add its conclusion to the set N. Theorem 1 can be generalized as follows.

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

4.3 Ordered chaining for general clauses

The following inference rules need to be added to obtain a refutationally complete inference system for general clauses.

Ordered Factoring:

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

where σ is the most general unifier of A and B, and Aσ is maximal in Cσ.

Unfortunately, it also turns out that for disjunctions of positive inequalities 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

→ c < b
→ b < c
→ a < b, a < c
a < b, a < c →

where 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 b ≮ b ∨ a ≮ c ∨ a < c by negative chaining. 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.

Transitivity Resolution:

\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; the inequality uσ < vσ is strictly maximal in Cσ ∨ u′σ < v′σ; the inequality sσ < tσ is strictly maximal in Dσ; and vσ ⪰̸ uσ, v′σ ⪰̸ uσ, v′σ ⪰̸ vσ, tσ ⪰̸ sσ, and vσ ⊁ tσ.

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

where σ is the most general unifier of v, v′ and t; the inequality uσ < vσ is strictly maximal in Cσ ∨ u′σ < v′σ; the inequality sσ < tσ is strictly maximal in Dσ; and uσ ⪰̸ vσ, u′σ ⪰̸ vσ, u′σ ⪰̸ uσ, sσ ⪰̸ tσ, and uσ ⊁ sσ.

This inference rule represents the controlled application of resolution with the transitivity axiom. For instance, the clause Dσ ∨ tσ ≮ v′σ ∨ sσ < v′σ is an instance of the conclusion of the resolution inference

\frac{Dσ , sσ < tσ x ≮ y , y ≮ z , x < z}{Dσ , tσ ≮ z , sσ < z}

In other words, the conclusion of a transitivity resolution inference π is an instance of a resolvent between the second premise of π and the transitivity axiom. The first premise of π regulates which instances and resolvents are needed. A similar inference is needed for resolving with the second literal of the transitivity axiom.

The calculus consisting of B_{<} plus ordered factoring and transitivity resolution is denoted by C_{<} (or C). These calculi are refutationally complete for arbitrary clause sets with a transitivity axiom. In the presence of n > 1 transitive relations <_{i}, the union ⋃_{i} C_{<i} forms a refutationally complete inference system. For the completeness proof the model construction has to be slightly modified (cf. Bachmair and Ganzinger 1993b).

We obtain the following completeness theorem.

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

We shall see below that only a very limited form of transitivity resolution is needed for transitive relations that are also symmetric. For total orderings, transitivity resolution can be completely avoided if the chaining rule that we have presented here is extended to so-called maximal chaining (Bachmair and Ganzinger 1993a).

5 Variable Chaining

In chaining we put together two inequalities (one of which may be negative) by unifying corresponding terms. If one of the two terms thus unified is a variable we speak of a variable chaining. This form of chaining is particularly prolific, as the unification of a term with a variable not occurring in it always succeeds. Fortunately, the constraints imposed by ordered chaining drastically cut down the number of possible variable chainings.

Consider an ordered chaining inference

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

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

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

→ a < a′
→ a′ < c
→ b < b′
→ b′ < c
a < x , b < x →

where c ≻ b′ ≻ b ≻ a′ ≻ a. This set of clauses is unsatisfiable. From the first two clauses we obtain a < c; from the third and fourth clause b < 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 ≮ b′, from which we get a ≮ 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 ≮ c ∨ b ≮ b′, from which a contradiction can be derived by one more chaining and two resolution steps.

6 Partial Equivalence Relations

Let ∼ be a transitive relation that also satisfies the symmetry axiom x ∼ y → y ∼ x. Symmetry is usually built into chaining by using literals s ∼ t in both directions. Now consider a chaining inference

\frac{C , u ≁ x D , s ∼ t}{Cσ , D , uσ ≁ t}

where σ = [s/x], t ⪰̸ s, s ∼ t is strictly maximal in C, and uσ ≁ s is maximal in Dσ. Let τ = [t/x]. Then the conclusion logically follows from Cτ ∨ uτ ≁ t and D ∨ s ∼ t. Thus, all such inferences (in which the first premise is maximal) are redundant. In particular, chaining through variables in a negative literal can be shown to be unnecessary. Note that this holds for clauses in general, not just Horn clauses. As a consequence, the resolution inferences with the symmetry axiom mentioned above are the only inferences in which this axiom can participate. Thus, the presence of the symmetry axiom allows us to restrict variable chainings, which in turn cuts down on the number of inferences with symmetry.

A few variable chainings are still needed. For example, the set of two clauses

→ x ∼ a
a ∼ b →

is unsatisfiable. But if c ≻ b ≻ a (and because of the minimality of the constant a, also x ⪰ a), then we need to chain through x in the first clause to derive a contradiction. (If a is not minimal, we can chain the first clause with itself through a, to obtain x ∼ y, which can then be resolved with the second clause to yield a contradiction.)

Another important consequence of symmetry is that transitivity resolution can be replaced by the following inference rule.

Equality Factoring:

\frac{C , u ∼ v , u′ ∼ v′}{Cσ , vσ ≁ v′σ , uσ ∼ v′σ}

where σ is the most general unifier of u and u′; vσ ⪰̸ uσ, v′σ ⪰̸ uσ, and v′σ ⪰̸ vσ; and uσ ∼ vσ is strictly maximal in Cσ ∨ u′σ ∼ v′σ.

Equality factoring corresponds to transitivity resolution of a (suitable) clause with itself. Any other transitivity resolutions are unnecessary for symmetric relations and the resulting chaining system is refutationally complete for partial equivalence relations.

Equivalence relations are transitive symmetric relations that are also reflexive. The latter property that can be built in as an (harmless) inference:

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

7 Congruence Relations

Rewrite techniques have primarily been applied to equivalence relations ∼ that also satisfy the congruence axioms

x ≈ y → f(…, x, …) ≈ f(…, y, …)
x ≈ y , P (…, x, …) → P (…, y, …)

for all function symbols f and predicate symbols P. Repeated resolutions with congruence axioms allow one to build a “context” around the terms in a maximal positive literal, so that from a clause C ∨ s ≈ t with maximal “equality” literal s ≈ t we may produce any clause C ∨ u[s] ≈ u[t]. Combining such inferences with chaining, we obtain what may be called subterm chaining, but is actually known as paramodulation or superposition. (Paramodulation corresponds to ordinary chaining; superposition, to ordered chaining.) A typical example is the following inference rule; for further details and references see Bachmair and Ganzinger (1994).

Superposition:

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

where (i) σ is a most general unifier of s and s′, (ii) sσ ≈ tσ is strictly maximal in Cσ, and tσ ⪰̸ sσ, (iii) uσ ≈ vσ is strictly maximal in Dσ, and vσ ⪰̸ uσ, and (iv) s′ is not a variable.

A similar inference rule is needed for superposition into negative equalities. The congruence axioms for predicate symbols also require one to paramodulate into arbitrary literals.

Ordered Paramodulation:

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

where (i) σ is a most general unifier of s and s′, (ii) sσ ≈ tσ is strictly maximal in Cσ, and tσ ⪰̸ sσ, (iii) L[s′]σ is not an equality literal and is maximal in Dσ, and (iv) s′ is not a variable.

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) turns 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, et al. (1992) and Nieuwenhuis and Rubio (1992) in which paramodulation into parts of clauses that have been generated by unfiers of previous inferences are avoided.

We emphasize that the above results apply to symmetric relations. There are interesting theories with non-symmetric operators that satisfy congruence or similar properties. For example, ordered ring structures satisfy axioms such as

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

that express monotonicity or anti-monotonicity properties. (Subterm) chaining methods for such ordering relations have been proposed by Manna and Waldinger (1986), Manna and Waldinger (1992), but completeness may require chaining into or even below variables, which is impractical. Levy and Agustí (1993) have had some success with several examples, including lattice theory.

To illustrate the difficulties, let us consider the 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 <^{R} a ∗ a <^{L} a ∗ b to derive a < a ∗ b. (If < were symmetric, we would also have a rewrite proof a <^{L} b <^{R} b∗b <^{R} a∗b and the variable 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 congruence 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 syntactic ordering is defined). 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 congruence 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.

8 Summary and Discussion

We have proposed chaining with ordering restrictions as an inference mechanism for dealing with transitive relations and have established its refutational completeness for Horn clauses. An extension to the inference system renders it refutationally complete for general clauses and, in the case of symmetric transitive relations, reduces to equality factoring, which is known from superposition calculi. All inference systems are compatible with a notion of redundancy that covers the simplification techniques commonly used in rewrite-based theorem provers (subsumption, tautology deletion, etc).

A key question in applications of chaining is to what extent variable chaining is needed. The ordering restrictions imposed in our calculi considerably cut down on such chainings, though some are still needed in general. In the presence of symmetry, almost no variable chaining is needed. Variable chainings can be completely excluded for dense total orderings with no endpoints, provided certain variable elimination rules are applied (Bledsoe and Hines 1980, Bledsoe, Kunen and Shostak 1985). The application of rewrite techniques to such theories is discussed in Bachmair and Ganzinger (1993a). The latter paper also discusses various aspects of an implementation of rewrite-based chaining systems.

Chaining techniques have also been applied to set theory Hines (1990), though no completeness results are known yet for the theorem proving systems that have been proposed. Other applications include the use of standard theorem proving techniques for certain modal and temporal logics based on their Kripke semantics. The accessibility relations on which these semantics are based are usually transitive (see Ohlbach 1993 for an overview of translation methods for such logics). In these logics the entailment relation is still monotone so that it can be identified with entailment in first-order logic. It is conceivable that ordered chaining can also be applied fruitfully to certain logics for which entailment is non-monotone.

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.

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, 1993a. Ordered Chaining for Total Orderings. Technical Report MPI-I-93-250, Max-Planck-Institut für Informatik, Saarbrücken. Short version to appear in Proc. CADE’94.

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

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 Technical Report MPI-I-91-208.

L. Bachmair, H. Ganzinger, Chr. Lynch and W. Snyder, 1992. Basic Paramodulation and Superposition. In D. Kapur, editor, Automated Deduction — CADE’11, Lecture Notes in Computer Science, vol. 607, pp. 462–476, Berlin, Springer-Verlag.

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 Resolution-based 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.

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.

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.

Z. Manna and R. Waldinger, 1986. Special Relations in Automated Deduction. Journal of the ACM, Vol. 33, pp. 1–60.

Z. Manna and R. Waldinger, 1992. The Special-Relation Rules are Incomplete. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, pp. 492–506, Saratoga Springs, NY, Springer LNAI 607.

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

H. J. Ohlbach, 1993. Translation Methods for Non-Classical Logics – An Overview. Technical Report MPI-I-93-225, Max-Planck-Institut für Informatik, Saarbrücken.

John Pais and G.E. Peterson, 1991. Using Forcing to Prove Completeness of Resolution and Paramodulation. Journal of Symbolic Computation, Vol. 11, pp. 3–19.

Gerald E. Peterson, 1983. A technique for establishing completeness results in theorem proving with equality. SIAM J. on Computing, Vol. 12, No. 1, pp. 82–100.

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.

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, Vol. 11, pp. 21–49.

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.

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

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