Rewrite-Based Equational Theorem

Proving

With Selection and Simplification

Leo Bachmair Harald Ganzinger

MPI–I–91–208 September 1991 Authors’ 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-W-6600 Saarbrücken,

Germany, hg@cs.uni-sb.de

Publication Notes

An extended abstract of this paper appeared in the proceedings of the Second Int. Workshop on Conditional and Typed Rewriting, Montréal 1990. The present report has been submitted for publication elsewhere and will be copyrighted if accepted.

Acknowledgements

Marianne Haberstrau and Robert Nieuwenhuis have found two errors in a preliminary version of the paper. We are very grateful for their careful reading. We also wish to thank Uwe Waldmann for his valuable comments.

The research described in this paper was supported in part by the National Science Foundation under grant CCR-8901322, by the ESPRIT project PROSPECTRA (ref. no. 390), and by a travel grant from the Deutsche Forschungsgemeinschaft.

Abstract

We present various refutationally complete calculi for first-order clauses with equality that allow for arbitrary selection of negative atoms in clauses. Refutation completeness is established via the use of well-founded orderings on clauses for defining a Herbrand model for a consistent set of clauses. We also formulate an abstract notion of redundancy and show that the deletion of redundant clauses during the theorem proving process preserves refutation completeness. It is often possible to compute the closure of nontrivial sets of clauses under application of non-redundant inferences. The refutation of goals for such complete sets of clauses is simpler than for arbitrary sets of clauses, in particular one can restrict attention to proofs that have support from the goals without compromising refutation completeness. Additional syntactic properties allow to restrict the search space even further, as we demonstrate for so-called quasi-Horn clauses. The results in this paper contain as special cases or generalize many known results about Knuth-Bendix-like completion procedures (for equations, Horn clauses, and Horn clauses over built-in Booleans), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.

Keywords

Theorem Proving, First-Order Logic, Equality, Paramodulation, Rewrite Techniques, Simplification, Saturation

1 Introduction

Methods for dealing with the equality predicate are of central concern in automated theorem proving. One of the more successful approaches to equational theorem proving is based on the use of equations as (one-way) rewrite rules. For instance, the so-called completion method (Knuth and Bendix 1970) attempts to construct a convergent (i.e., terminating and Church-Rosser) rewrite system for a given set of (universally quantified) equational axioms. Two terms can be rewritten to identical normal forms if, and only if, they are equal. A convergent rewrite system thus provides a decision procedure for its equational theory. The completion procedure may fail in general, but has been extended to a refutationally complete theorem prover (cf. Lankford 1975, Hsiang and Rusinowitch 1987, and Bachmair, Dershowitz and Plaisted 1989). Completion procedures for conditional equations (i.e., Horn clauses with equations as the only atomic formulas) have been described by Kounalis and Rusinowitch (1988), and by Ganzinger (1987a, b).

The two main components of completion are (i) the deductive inference rule of superposition and (ii) various mechanisms for deleting redundant equations via simplification by rewriting. There have been several attempts to extend completion to first-order clauses, based on the observation that superposition is a restricted form of paramodulation (Robinson and Wos 1969). Another technique common in clausal theorem proving, demodulation (Wos et al. 1967), is essentially a special case of simplification by rewriting.

Consider, for instance, paramodulation (for variable-free formulas):

\frac{Γ → Δ, s ≈ t Λ → Π, u[s] ≈ v}{Γ, Λ → Δ, Π, u[t] ≈ v}

and suppose that ≻ is an ordering which is total on variable-free terms and formulas. We say that the paramodulation inference is ordered (with respect to ≻) if (i) s ≻ t; (ii) s ≈ t is strictly maximal with respect to Γ ∪ Δ; and (iii) u[s] ≈ v is strictly maximal with respect to Λ ∪ Π. An ordered paramodulation inference is said to be a superposition inference if (iv) u[s] ≻ v. The superposition is called strict if in addition (v) s does not occur in Γ. A weak superposition inference is a paramodulation inference for which conditions (i), (iii), and (iv)—but not necessarily (ii)—are satisfied.

Hsiang and Rusinowitch (1989) have proved that ordered paramodulation is refutationally complete, whereas Rusinowitch (1991) has established the refutation completeness of weak superposition. Strict superposition is unfortunately not complete (Bachmair and Ganzinger 1990).

For example, consider the set of clauses

c ≈ d →
→ b ≈ d
a ≈ d → a ≈ c
→ a ≈ b, a ≈ d

where a, b, c, and d are constants. This set is unsatisfiable: from the last three clauses we may infer that a ≈ b ≈ c ≈ d, which contradicts the first clause. However, if ≻ is an ordering in which a ≻ b ≻ c ≻ d, then the only clause that can be obtained from the above clauses by superposition is a ≈ d → b ≈ c, a ≈ d, which is a tautology. No further clauses, in particular no contradiction, can be deduced by superposition.

However, several moderate enrichments of the (strict) superposition calculus are indeed refutationally complete (Bachmair and Ganzinger 1990). In this paper we generalize the deductive part of (conditional) completion to first-order clauses, and more importantly also deal with simplification, which is indispensable for any practical use of completion.^{1} We introduce an abstract notion of redundancy (of clauses and inferences) and use it as the fundamental concept in formulating a framework for theorem proving with simplification. We present criteria that can be used in tests for checking redundancy and show that under reasonable conditions on the search strategy employed by a theorem prover, deletion of redundant clauses does not destroy refutation completeness. The notion of saturation of a set of clauses, in the sense that all non-redundant inferences are computed, generalizes completion (with simplification) to first-order clauses. In addition, we show that arbitrary selection functions on negative literals can be used with these superposition calculi.

The simplification techniques to which our results apply include, among others, deletion of tautologies, subsumption, case analysis, and contextual reductive rewriting. We also investigate ways of improving the search for a refutation of a given goal with respect to a set of clauses that is already saturated. The results presented here for the case of first-order clauses include and generalize results about ordered completion of equations (Bachmair, Dershowitz and Plaisted 1989; Bachmair 1991), completion of Horn clauses (Kounalis and Rusinowitch 1988, Ganzinger 1987b), and ground completion of Horn clauses over built-in Booleans (Zhang and Rémy 1985, Ganzinger 1987a, Nieuwenhuis and Orejas 1991).

The paper is organized as follows. In the next chapter we introduce our terminology and basic definitions. We describe superposition calculi with selection functions on negative literals in Chapter 3 and prove their refutation completeness in Chapter 4. The notions of redundancy and saturation, as well as modular criteria for redundancy, are also introduced in Chapter 4. In Chapter 5 we outline an abstract framework for theorem proving with simplification and discuss various specific simplification mechanisms, such as case analysis and contextual reductive rewriting. In Chapter 6 we study refutation of goals for so-called quasi-Horn programs and include various results about Horn clauses and inductive theorem proving.

2 Preliminaries

2.1 Equational clauses

We formulate our inference rules in an equational framework and define clauses in terms of multisets.

A multiset over a set X is a function M from X to the natural numbers. Intuitively, M(x) specifies the number of occurrences of x in M. We say that x is an element of M if M(x) > 0, and M is a submultiset of M′ (written M ⊆ M′) if M(x) ≤ M′(x), for all x. A multiset M is called finite if M(x) = 0 for all but finitely many x. The union and intersection of multisets are defined by the identities M_{1} ∪ M_{2}(x) = M_{1}(x) + M_{2}(x) and M_{1} ∩ M_{2}(x) = min(M_{1}(x), M_{2}(x)). If M is a multiset and S a set, we write M ⊆ S to indicate that every element of (the multiset) M is an element of (the set) S, and use M ∩ S to denote the set {x ∈ S : M(x) ≥ 1}. For simplicity, we often use a set-like notation to describe multisets. For example, {x, x, x} denotes the multiset M for which M(x) = 3 and M(y) = 0, for y ≠ x.

1Rusinowitch (1991) does discuss simplification to some extent, but for practical purposes his simplification techniques are inadequate even for the very simplest case—completion of sets of universally quantified equations.

An equation is an expression s ≈ t, where s and t are (first-order) terms built from given function symbols and variables. We identify s ≈ t with the multiset {s, t}. By a ground expression (i.e., a term, equation, formula, etc.) we mean an expression containing no variables.

A clause is a pair of multisets of equations, written Γ → Δ. The multiset Γ is called the antecedent; the multiset Δ, the succedent. We usually write Γ_{1}, Γ_{2} instead of Γ_{1} ∪ Γ_{2}; Γ, A or A, Γ instead of Γ∪{A}; and A_{1}, …, A_{m} → B_{1}, …, B_{n} instead of {A_{1}, …, A_{m}} → {B_{1}, …, B_{n}}. A clause A_{1}, …, A_{m} → B_{1}, …, B_{n} represents an implication A_{1} ∧⋯∧A_{m} ⊃ B_{1} ∨⋯∨B_{m}; the empty clause, a contradiction. Clauses of the form Γ, A → A, Δ or Γ → Δ, t ≈ t are called tautologies.

2.2 Equality Herbrand interpretations

We write A[s] to indicate that A contains s as a subexpression and (ambiguously) denote by A[t] the result of replacing a particular occurrence of s by t. By Aσ we denote the result of applying the substitution σ to A and call Aσ an instance of t. If Aσ is ground, we speak of a ground instance. We shall also consider instances of multisets of equations and of clauses. For example, the multiset {a ≈ b, a ≈ b} is an instance of {x ≈ b, a ≈ y}. Composition of substitutions is denoted by juxtaposition. Thus, if τ and ρ are substitutions, then xτρ = (xτ)ρ, for all variables x.

An equivalence is a reflexive, transitive, symmetric binary relation. An equivalence ∼ on terms is called a congruence if s ∼ t implies u[s] ∼ u[t], for all terms u, s, and t. If E is a set of ground equations, we denote by E^{∗} the smallest congruence ∼ such that s ∼ t whenever s ≈ t ∈ E.

By an (equality Herbrand) interpretation we mean a congruence on ground terms. An interpretation I is said to satisfy a ground clause Γ → Δ if either Γ ⊈ I or else Δ ∩ I ≠ ∅. We also say that a ground clause C is true in I, if I satisfies C; and that C is false in I, otherwise. An interpretation I is said to satisfy a non-ground clause Γ → Δ if it satisfies all ground instances Γσ → Δσ. For instance, a tautology is satisfied by any interpretation. A clause which is satisfied by no interpretation (e.g., the empty clause) is called unsatisfiable. An interpretation I is called a (equality Herbrand) model of N if it satisfies all clauses of N. A set N of clauses is called consistent if it has a model; and inconsistent (or unsatisfiable), otherwise. We say that N implies C, and write N ⊧ C, if every model of N satisfies C.

Convergent rewrite systems provide a convenient formalism for describing and reasoning about equality interpretations.

2.3 Convergent rewrite systems

A binary relation ⇒ on terms is called a rewrite relation if s ⇒ t implies u[sσ] ⇒ u[tσ], for all terms s, t and u, and substitutions σ. A transitive, well-founded rewrite relation is called a reduction ordering. By ⇔ we denote the symmetric closure of ⇒; by ⇒^{∗} the transitive, reflexive closure; and by ⇔^{∗} the symmetric, transitive, reflexive closure. Furthermore, we write s ⇓ t to indicate that s and t can be rewritten to a common form: s ⇒^{∗} v and t ⇒^{∗} v, for some term v. A rewrite relation ⇒ is said to be Church-Rosser if the two relations ⇔^{∗} and ⇓ are the same.

A set of equations E is called a rewrite system with respect to an ordering ≻ if we have s ≻ t or t ≻ s, for all equations s ≈ t in E. If all equations in E are ground, we speak of a ground rewrite system. Equations in E are also called (rewrite) rules. When we speak of “the rule s ≈ t” we implicitly assume that s ≻ t. By ⇒_{E^{≻}} (or simply ⇒_{E}) we denote the smallest rewrite relation for which s ⇒_{E} t whenever s ≈ t ∈ E and s ≻ t. A term s is said to be in normal form (with respect to E) if it can not be rewritten by ⇒_{E}, i.e., if there is no term t such that s ⇒_{E} t. A term is also called irreducible, if it is in normal form, and reducible, otherwise. For instance, if s ⇓_{E} t and s ≻ t, then s is reducible by E.

A rewrite system E is said to be convergent if the rewrite relation ⇒_{E} is well-founded and Church-Rosser. Convergent rewrite systems define unique normal forms. A ground rewrite system E is called left-reduced if for every rule s ≈ t in E the term s is irreducible by E \ {s ≈ t}. It is well-known that left-reduced, well-founded rewrite systems are convergent (cf. Huet 1980).

2.4 Clause orderings

Any ordering ≻ on a set S can be extended to an ordering ≻_{mul} on finite multisets over S as follows: M ≻_{mul} N if (i) M ≠ N and (ii) whenever N(x) > M(x) then M(y) > N(y), for some y such that y ≻ x. If ≻ is a total [well-founded] ordering, so is ≻_{mul}. Given a set (or multiset) S and an ordering ≻ on S, we say that x is maximal relative to S if there is no y ∈ S with y ≻ x; and strictly maximal if there is no y ∈ S with y ⪰ x.

If ≻ is an ordering on terms, then the corresponding multiset ordering ≻_{mul} is an ordering on equations, which we denote by ≻^{e}.

We have defined clauses as pairs of multisets of equations. Alternatively, clauses may also be thought of as multisets of occurrences of equations. We identify an occurrence of an equation s ≈ t in the antecedent of a clause with the multiset (of multisets) {{s, ⊥}, {t, ⊥}}, and an occurrence in the succedent with the multiset {{s}, {t}}, where ⊥ is a new symbol.^{2} We identify clauses with finite multisets of occurrences of equations. By ≻^{o} we denote the twofold multiset ordering (≻_{mul})_{mul} of succ, which is an ordering on occurrences of equations; by ≻^{c} we denote the multiset ordering ≻_{mul}^{o}, which is an ordering on clauses. If ≻ is a well-founded [total] ordering, so are ≻^{e}, ≻^{o}, and ≻^{c}.

Observe the difference between the ordering ≻^{e} on equations and the ordering ≻^{o} on occurrences of equations. For example, if s ≻ t ≻ u, then s ≈ t ≻^{e} s ≈ u, but nonetheless we have Γ, s ≈ u → Δ ≻^{c} Γ → s ≈ t, Δ as the occurrence of s ≈ u (in the antecedent) is larger than the occurrence of s ≈ t (in the succedent).

The superposition calculi described below are defined in terms of these orderings.^{3} In Bachmair and Ganzinger (1990) we have identified an occurrence of an equation s ≈ t in the antecedent of a clause with the multiset {{s, t, ⊥}} and an occurrence in the succedent with the multiset {{s, t}}, and consequently obtained a slightly different clause ordering and inference system. The above ordering has the advantage that it eliminates certain technical complications in the proof of the refutation completeness of the corresponding superposition calculus.

2The symbol ⊥ is not part of the vocabulary of the given first-order language. It is assumed to be minimal with respect to any given ordering. Thus t ≻ ⊥, for all terms t.

3We shall also use orderings to define simplification techniques that are compatible with superposition. In a few cases the simplification techniques used in completion require information about the substitution by which an instance of a clause is obtained. For that purpose it is necessary to consider pairs (C, σ) of clauses and substitutions, and not just instances Cσ, so that an ordering may distinguish between pairs (C, σ) and (D, τ) even when the instances Cσ and Dτ are identical. For the sake of simplicity we have chosen not to use this slightly more sophisticated formalism in this paper.

3 Ordered Inference Rules with Selection

We shall consider inference rules

\frac{C_{1} ⋯ C_{n}}{C}

where C_{1}, …, C_{n} (the premises) and C (the conclusion) are clauses.

Definition 1 Let ≻ be a reduction ordering. We say that a clause C = Γ → Δ, s ≈ t is reductive for s ≈ t if t ⪰̸ s and s ≈ t is a strictly maximal occurrence of an equation in C.^{4}

For example, if s ≻ t ≻ u and s ≻ v, for every term v occurring in Γ, then Γ → s ≈ u, s ≈ t is reductive for s ≈ t, but Γ, s ≈ u → s ≈ t is not. In general, if a clause C is reductive for s ≈ t, then s must not occur in the antecedent of C.

The following inference rules are defined with respect to ≻. The first rule encodes the reflexivity of equality:

Equality resolution:  \frac{Λ, u ≈ v → Π}{Λσ → Πσ}

where σ is a most general unifier of u and v and uσ ≈ vσ is a maximal occurrence of an equation in Λσ, uσ ≈ vσ → Πσ.

The next inference rule represents a variant of factoring, restricted to the succedent of clauses:

Ordered factoring:  \frac{Γ → Δ, A, B}{Γσ → Δσ, Aσ}

where σ is a most general unifier of A and B and Aσ is a maximal occurrence of an equation in Γσ → Δσ, Aσ, Bσ.

The following superposition rules represent restricted versions of paramodulation:

Superposition, left:  \frac{Γ → Δ, s ≈ t u[s′] ≈ v, Λ → Π}{u[t]σ ≈ vσ, Γσ, Λσ → Δσ, Πσ}

where (i) σ is a most general unifier of s and s′, (ii) the clause Γσ → Δσ, sσ ≈ tσ is reductive for sσ ≈ tσ, (iii) vσ ⪰̸ uσ and uσ ≈ vσ is a maximal occurrence of an equation in uσ ≈ vσ, Λσ → Πσ,^{5} and (iv) s′ is not a variable.

Superposition, right:  \frac{Γ → Δ, s ≈ t Λ → u[s′] ≈ v, Π}{Γσ, Λσ → u[t]σ ≈ vσ, Δσ, Πσ}

where (i) σ is a most general unifier of s and s′, (ii) the clause Γσ → Δσ, sσ ≈ tσ is reductive for sσ ≈ tσ, (iii) the clause Λσ → uσ ≈ vσ, Πσ is reductive for uσ ≈ vσ, and (iv) s′ is not a variable.

4If the reduction ordering ≻ is assumed to be complete (i.e., total on ground terms), we could use a somewhat stronger formulation of reductivity where instead of t ⪰̸ s we require that sσ ≻ tσ, for some ground substitution σ. However, our results apply not only to complete orderings, but more generally to completable orderings (i.e., orderings contained in a complete ordering); cf. the discussion of ordered completion in Bachmair (1991).

5Since we do not require factoring in the antecedent, the equation uσ ≈ vσ may also occur in Λσ.

The example given in the introduction shows that superposition is not refutationally complete, but has to be combined with additional inference rules. For instance, we may add the following inference rule, which in essence generalizes ordered factoring:

Equality factoring:  \frac{Γ → Δ, s ≈ t, s′ ≈ t′}{Γσ, tσ ≈ t′σ → Δσ, s′σ ≈ t′σ}

where (i) σ is a most general unifier of s and s′; (ii) tσ ⊁ sσ and t′σ ⊁ s′σ; and (iii) sσ ≈ tσ is a maximal occurrence of an equation in Γσ → Δσ, sσ ≈ tσ, s′σ ≈ t′σ.

An alternative to equality factoring is the paramodulation rule:

Merging Paramodulation: \frac{Γ → Δ, s ≈ t Λ → u ≈ v[s′], u′ ≈ v′, Π}{Γσ, Λσ → uσ ≈ v[t]σ, uσ ≈ v′σ, Δσ, Πσ}

where (i) σ is the composition τρ of a most general unifier τ of s and s′, and a most general unifier ρ of uτ and u′τ, (ii) the clause Γσ → Δσ, sσ ≈ tσ is reductive for sσ ≈ tσ, (iii) the clause Λσ → Πσ, uσ ≈ vσ, u′σ ≈ v′σ is reductive for uσ ≈ vσ, (iv) uτ ≻ vτ and v′σ ⪰̸ vσ, and (v) s′ is not a variable.

Merging paramodulation is designed in such a way that its repeated application to ground clauses (in conjunction with ordered factoring) has the effect of merging atoms in the succedent containing a maximal term.

By E we denote the inference system consisting of equality resolution, equality factoring, and superposition; by P the inference system consisting of equality resolution, ordered factoring, superposition, and merging paramodulation. (If necessary, we indicate the underlying ordering by writing E^{≻} or P^{≻}.) In each case the following additional restrictions are imposed: (a) the premises of an inference rule must not share any variables (if necessary, the variables in one premise are renamed); and (b) if C and D are the premises of a paramodulation inference with σ the mgu obtained from superposing C on D, then Cσ ⪰̸^{c} Dσ. Later on we will define a notion of redundancy for inferences which restricts the inference systems even further. For example, inferences involving tautologies will be redundant.

An essential property of the above inference rules is that the conclusion of a ground inference is always simpler (with respect to the ordering ≻^{c}) than the maximal premise (which is always the second premise in the case of a paramodulation inference).

We shall also discuss variants of the above inference rules that are controlled by a selection function that assigns to each clause a (possibly empty) multiset of (occurrences of) equations in the antecedent. If S is such a selection function, then the equations in S(C) are called selected. Selected equations can be arbitrarily chosen and need not be maximal.^{6} Also, S(C) = ∅ indicates that no equation is selected.

The following inference rules are defined with respect to a given selection function S.

Selective resolution:  \frac{Λ, u ≈ v → Π}{Λσ → Πσ}

where σ is a most general unifier of u and v and u ≈ v is a selected equation in Λ, u ≈ v → Π.

6An ordering may be used, however, for further distinctions if more than one equation is selected. The corresponding modifications required for this technique are straightforward and will not be discussed below.

Selective superposition: \frac{Γ → Δ, s ≈ t u[s′] ≈ v, Λ → Π}{u[t]σ ≈ vσ, Γσ, Λσ → Δσ, Πσ}

where (i) σ is a most general unifier of s and s′, (ii) the clause C = Γ → Δ, s ≈ t contains no selected equations and Cσ is reductive for sσ ≈ tσ, (iii) vσ ⪰̸ uσ and u ≈ v is a selected equation in u ≈ v, Λ → Π, and (iv) s′ is not a variable.

By E_{S} [P_{S}] we denote the system consisting of the above two selective inference rules plus all inference rules of E [P], with the additional restriction on the latter rules that no premise contain any selected literals. For instance, in the presence of a selection function right superposition can only be applied to premises that contain no selected equations.

A selection function S for which S(C) is a singleton whenever the antecedent of C is non-empty, is called unitary. An inference system for Horn clauses with arbitrary unitary selection functions, which is based on the inference system E_{S}, has been described by Ganzinger (1987a). (The two inference systems E_{S} and P_{S} are identical in the Horn clause case, as ordered factoring, equality factoring, and merging paramodulation cannot be applied to Horn clauses.)

A selection function S for which S(C) is non-empty whenever the antecedent of C is non-empty determines a so-called positive superposition strategy. In positive strategies only clauses with empty antecedent are paramodulated into other clauses. An example of such an inference system, also for Horn clauses, is the maximal-literal unit strategy (Dershowitz 1991), where for each clause the complete antecedent is selected and ordering constraints are imposed on selected equations.

The case of first-order clauses with equality and additional arbitrary predicates is included in the above framework. From now on we shall assume that a set of predicate symbols is given in addition to the set of function symbols. Thus we also consider expressions P (t_{1}, …, t_{n}), where P is some predicate symbol and t_{1}, …, t_{n} are terms built from function symbols and variables. We then have equations s ≈ t between (non-predicate) terms, called function equations, and equations P (t_{1}, …, t_{n}) ≈ tt, called predicate equations, where tt is a distinguished unary predicate symbol that is taken to be minimal in the given reduction ordering ≻. For simplicity, we usually abbreviate P (t_{1}, …, t_{n}) ≈ tt by P (t_{1}, …, t_{n}).

Clauses of the form Γ, P (t_{1}, …, t_{n}) ≈ tt → Δ or Γ → Δ, P (t_{1}, …, t_{n}) ≈ tt in which P (t_{1}, …, t_{n}) ≈ tt is a maximal equation can evidently not be part of an equality or selective resolution inference. Furthermore, superposition of a clause Γ → Δ, P (s_{1}, …, s_{n}) ≈ tt on a clause Λ → Π, P (t_{1}, …, t_{n}) ≈ tt results in a tautology Γσ, Λσ → Δσ, Πσ, tt ≈ tt and is therefore redundant. The remaining inferences are left or selective superpositions of the form

\frac{Γ → Δ, P (s_{1}, …, s_{n}) ≈ tt P (t_{1}, …, t_{n}) ≈ tt, Λ → Π}{Γσ, Λσ, tt ≈ tt → Δσ, Πσ.}

Note that the trivial equation tt ≈ tt in the antecedent can be eliminated by resolution. Thus we obtain a derived inference rule:

Ordered resolution: \frac{Γ → Δ, P (s_{1}, …, s_{n}) P (t_{1}, …, t_{n}), Λ → Π}{Γσ, Λσ → Δσ, Πσ}

with the restrictions associated with selective or left superposition.

4 Refutation Completeness

We shall next prove that the above superposition calculi are refutationally complete in the sense that a contradiction (the empty clause) can be derived from any inconsistent set of clauses. In the proof we shall have to argue about ground instances of given clauses and inferences.

Definition 2 Let π be an inference in I with premises C_{1}, …, C_{n} and conclusion C, where the clauses C_{1}, …, C_{n} have no variables in common. By an instance of π we mean any inference in I with premises C_{1}σ, …, C_{n}σ and conclusion Cσ.

It can easily be seen that any resolution or factoring inference from ground instances of N is a ground instance of an inference from N. For superposition this correspondance need not necessarily hold. For instance, let N be the set of three clauses

{→ a ≈ b, → f(a) ≈ f(b), p(g(x)) → p(f(x))}.

If a ≻ b, f(a) ≻ f(b), and p(f(x)) ≻ p(g(x)), then

π = \frac{→ f(a) ≈ f(b) p(g(x)) → p(f(x))}{p(g(a)) → p(f(b))}

is a superposition inference and

\frac{→ f(a) ≈ f(b) p(g(a)) → p(f(a))}{p(g(a)) → p(f(b))}

is a ground instance of π, while the superposition inference

\frac{→ a ≈ b p(g(a)) → p(f(a))}{p(g(a)) → p(f(b))}

is an inference from ground instances of N, but not a ground instance of any inference from N. Such problematic inferences, which arise from superpositions into the “variable” or “substitution part” of a clause, cannot be “lifted” to the general level, but as we shall see need not be considered.

Definition 3 We say that an instance Cσ of a clause C is reduced with respect to a rewrite system R if xσ is irreducible by R, for all variables x occurring in C.

Lemma 1 Let C and D be clauses with no variables in common, and let Cσ = Γ → Δ, s ≈ t and Dσ be ground instances, such that Dσ ≻^{c} Cσ and s ≈ t is a maximal occurrence of an equation in Cσ, and Dσ is a reduced ground instance of D with respect to {s ≈ t}. Then any superposition or merging paramodulation inference with premises Cσ and Dσ is a ground instance of a similar inference from C and D.

4.1 Construction of Equality Interpretations

Let N be a set of clauses and ≻ be a reduction ordering which is total on ground terms. We define an interpretation I by means of a convergent rewrite system R as follows.

First, we use induction on the clause ordering ≻^{c} to define sets of equations E_{C}, R_{C}, and I_{C}, for all ground instances C of clauses of N. Let C be such a ground instance and suppose that E_{C′}, R_{C′}, and I_{C′} have been defined for all ground instances C′ of N for which C ≻^{c} C′. Then

R_{C} = ⋃_{C≻^{c}C′}E_{C′} and I_{C} = R_{C}^{∗}.

Moreover

E_{C} = {s ≈ t}

if C is a clause Γ → s ≈ t, Δ such that (i) C is reductive for s ≈ t, (ii) s is irreducible by R_{C}, (iii) Γ ⊆ I_{C}, and (iv) Δ ∩ I_{C} = ∅. In that case, we also say that C produces the equation (or rule) s ≈ t. In all other cases, E_{C} = ∅. Finally, we define I to be the equality interpretation R^{∗}, where R = ⋃_{C} E_{C} is the set of all equations produced by ground instances of clauses of N.

Clauses that produce equations are also called productive. Note that a productive clause C is false in I_{C} = R_{C}^{∗}, but true in (R_{C} ∪ E_{C})^{∗}. The sets R_{C} and R are constructed in such a way that they are left-reduced rewrite systems with respect to ≻. Consequently these rewrite systems are convergent and the truth value of an equation can be determined by rewriting: u ≈ v ∈ I if and only if u ⇓_{R} v. In many cases the truth value of an equation can already be determined by rewriting with R_{C}.

Lemma 2 Let C = Γ → Δ, s ≈ t be a clause where s ≈ t is a maximal occurrence of an equation, and let D be another clause containing s. If C ≻^{c} D and s is irreducible by R_{C}, then R_{C} = R_{D} (and hence I_{C} = I_{D}).

Proof. If C′ is any clause with C ≻^{c} C′ ⪰^{c} D, then E_{C′} = ∅, for otherwise s would be reducible by R_{C}. Therefore R_{C} = R_{D} ∪ ⋃_{C≻^{c}C′≻^{c}D} E_{C′} = R_{D}. □

Lemma 3 Let C = Γ, u ≈ v → Δ and D be ground instances of N with D ⪰^{c} C. Then u ≈ v is true in I_{C} if and only if it is true in I_{D} if and only if it is true in I.

Proof. If u ≈ v is true in I_{C}, then u ⇓_{R_{C}} v. Since R_{C} ⊆ R_{D} ⊆ R, we then have u ⇓_{R_{D}} v and u ⇓_{R} v, which indicates that u ≈ v is true in I_{D} and in I.

On the other hand, suppose u ≈ v is false in I_{C}. If u′ and v′ are the normal forms of u and v with respect to R_{C}, then u′ ≠ v′. Furthermore, if s ≈ t is a rule in R \ R_{C}, then s ≻ u ⪰ u′ and s ≻ v ⪰ v′. (Clauses which produce rules for terms not greater than u or v are smaller than C.) Therefore, u′ and v′ are in normal form with respect to R, which implies that u ≈ v is false in I and in I_{D}. □

Lemma 4 Let C = Γ → Δ, u ≈ v and D be ground instances of N with D ⪰^{c} C. If u ≈ v is true in I_{C}, then it is also true in I_{D} and in I.

Proof. Use the fact that R_{C} ⊆ R_{D} ⊆ R. □

The above lemmas indicate that the sequence of interpretations I_{C}, with C ranging over all ground instances of N, preserves the truth of ground clauses:

Corollary 1 Let C and D be ground instances of N with D ⪰^{c} C. If C is true in I_{C}, then it is also true in I_{D} and I.

The following lemma allows us to restrict our attention to reduced ground instances of clauses in N.

Lemma 5 Suppose Cσ is a ground instance of a clause C in N, where xσ is reducible by R_{Cσ}, for some variable x occurring in C. Then there is a ground instance Cτ of C, such that (i) Cσ ≻^{c} Cτ and (ii) Cτ is true in I_{Cσ} if and only if Cσ is true in I_{Cσ}.

Proof. If xσ ⇒_{R_{Cσ}} t, define τ to be the substitution for which xτ = t and yτ = yσ, for all y with y ≠ x. □

4.2 Redundancy and Saturation

We shall prove that the interpretation I is a model of N, provided N is consistent and saturated, i.e., closed under sufficiently many applications of superposition inference rules.

(Selected) superposition and merging paramodulation are restricted versions of ordinary paramodulation. The ordering constraints and the selection of specific equations in the antecedent of a clause can be thought of as ways of pruning the search space of ordinary paramodulation. While these constraints are local in that they depend on information contained in a given clause, we shall demonstrate that the search space can be further decreased by certain non-local restrictions which are based on the concept of redundancy (of clauses and inferences). Intuitively, a clause is redundant if it does not contribute to the definition of the intended model I of N. An inference is redundant if either one of its premises is redundant or else its conclusion does not contribute to the definition of the intended model I of N. Saturation then means that all non-redundant inferences have been computed.

The following definitions refer to a given set of clauses N and the interpretation I constructed from N. If C is a ground clause, we denote by N_{C} the set of all ground instances C′ of N for which C ≻^{c} C′.

Definition 4 A ground instance C of a clause in N is said to be redundant if it is true in I_{C}. A clause in N is called redundant if all its ground instances are redundant.

By Corollary 1, redundant clauses are true in I. The interpretation I is completely determined by productive clauses, which are non-redundant.

Definition 5 An inference π from ground instances of N is said to be redundant if either one of its premises is redundant or else its conclusion is true in I_{C}, where C is the maximal premise of π. An inference from N is redundant if all its ground instances are redundant. We say that N is saturated on N′ if every ground instance of an inference from N, the premises of which are in N′, is redundant.

For instance, we will deal with sets N that are saturated on N_{C}, for some ground clause C. Evidently, if N is saturated on N′, then it is also saturated on any subset of N′. Also, N is simply called saturated if all ground instances of inferences from N are redundant. The essential properties of saturated sets are given in the following lemma.

Lemma 6 Let N be a set of clauses saturated on N′ (with respect to some inference system E_{S} or P_{S}). Suppose C = Γ → s ≈ t, Δ is a non-redundant ground instance of some clause D in N, where N_{C} ∪ {C} ⊆ N′, s ≻ t, the term s is irreducible by R_{C}, and s ≈ t is a maximal occurrence of an equation in C. Then (i) C = Dσ is a reduced ground instance of D with respect to R_{C}; (ii) C contains no selected equation; (iii) C produces s ≈ t; and (iv) Γ ⊆ I and Δ ∩ I = ∅.

Proof. The proof is by induction on the clause ordering ≻^{c}. Suppose N is saturated on N′. Let C = Γ → s ≈ t, Δ be a non-redundant clause, such that N_{C} ∪ {C} ⊆ N′, s ≻ t, the term s is irreducible by R_{C}, and s ≈ t is a maximal occurrence of an equation in C. Since C is non-redundant, we have Γ ⊆ I_{C} and (Δ ∪ {s ≈ t}) ∩ I_{C} = ∅. We have to prove that C satisfies properties (i)-(iv). Let us assume properties (i)-(iv) hold for all suitable clauses C′ with C ≻^{c} C′.

(i) Suppose C = Dσ is not reduced, i.e., xσ is reducible by R_{C}, for some variable x occurring in D. (Note that xσ can not occur in s, as s is irreducible by R_{C}.) By Lemma 5 there exists a ground instance C′ = Dτ = Γ′ → Δ′, s ≈ t′, such that C ≻^{c} C′, Γ′ ⊆ I_{C}, and (Δ′ ∪ {s ≈ t′}) ∩ I_{C} = ∅. By Lemma 2 we have R_{C′} = R_{C}, which implies that C′ is false in I_{C′} and hence non-redundant. Since C ≻^{c} C′, we may use the induction hypothesis to infer that properties (i)-(iv) hold for C′. In particular, C′ produces some equation s ≈ t′′. Since E_{C′} ⊆ R_{C}, this contradicts the assumption that s is irreducible by R_{C}.

For the remaining part of the proof, we assume that C is a reduced ground instance of D with respect to R_{C}.

(ii) Suppose C contains a selected equation. We distinguish two subcases.

If C is a clause Γ′, u ≈ u → Δ, s ≈ t, where u ≈ u is selected, then C′ = Γ′ → Δ, s ≈ t may be obtained from C by selective resolution. Since N is saturated on N_{C} ∪ {C}, the resolution inference has to be redundant. Thus C′ has to be true in I_{C}, which contradicts that Γ′ ⊆ I_{C} and (Δ ∪ {s ≈ t}) ∩ I_{C} = ∅.

If C is a clause Γ′, u ≈ v → Δ, s ≈ t, where u ≻ v and u ≈ v is selected, then u ⇓_{R_{C}} v and therefore u is reducible by R_{C}. Let C′ = Λ → Π, w ≈ w′, where C ≻^{c} C′, be a non-redundant clause that produces the rule w ≈ w′, where w is a subterm of u. Using the induction hypothesis, we may infer that the clause contains no selected equations, Λ ⊆ I_{C}, Π ∩ I_{C} = ∅, and w ≈ w′ ∈ I_{C}. Consider the inference

\frac{Λ → Π, w ≈ w′ Γ, u[w] ≈ v → Δ, s ≈ t}{Λ, Γ, u[w′] ≈ v → Π, Δ, s ≈ t}

by selective paramodulation. Since C is a reduced ground instance with respect to R_{C}, this inference is a ground instance of an inference from N. Since N is saturated on N_{C} ∪ {C}, the inference has to be redundant. That is, the conclusion C′′ has to be true in I_{C}, which contradicts that Λ ∪ Γ ∪ {u[w′] ≈ v} ⊆ I_{C} and (Π ∪ Δ ∪ {s ≈ t}) ∩ I_{C} = ∅.

For the remaining part of the proof, we assume that C contains no selected equations.

(iii) If Δ is of the form Δ′, s ≈ t, then the clause Γ → Δ′, s ≈ t can be obtained from C by ordered factoring, whereas Γ, t ≈ t → Δ′, s ≈ t can be obtained by equality factoring. Both clauses are false in I_{C}. However, since N is saturated with respect to E_{S} or P_{S}, at least one of the two clauses has to be true in I_{C}, which is a contradiction. We may therefore assume that s ≈ t does not occur in Δ, which implies that C produces s ≈ t.

(iv) First observe that Γ ⊆ I_{C} ⊆ I. Now suppose Δ contains an equation u ≈ v which is true in I. Since Δ ∩ I_{C} = ∅, we have u ≈ v ∈ I \ I_{C}, which is only possible if s = u and t ⇓_{I_{C}} v. Since t ≻ v, the term t is reducible by R_{C}. We distinguish two cases.

If N is saturated on N_{C} ∪ {C} with respect to E_{S}, then the clause Γ, t ≈ v → Δ′, s ≈ v, which can be obtained from C by equality factoring, has to be true in I_{C}. This contradicts that Γ ∪ {t ≈ v} ⊆ I_{C} and Δ ∩ I_{C} = ∅.

Suppose N is saturated N_{C} ∪ {C} with respect to P_{S}. Since t is reducible by R_{C}, there exists a clause C′ = Λ → Π, w ≈ w′, C ≻^{c} C′, that produces a rule w ≈ w′, where w is a subterm of t. Consider the inference

\frac{Λ → Π, w ≈ w′ Γ → Δ′, s ≈ v, s ≈ t[w]}{Λ, Γ → Π, Δ′, s ≈ v, s ≈ t[w′]}

by merging paramodulation. The conclusion of this inference has to be true in I_{C}, which again leads to a contradiction.

In sum, we may conclude that Δ ∩ I = ∅. □

Lemma 7 Suppose N is saturated on N′ and does not contain the empty clause. If C is a ground instance of N and (N_{C} ∪ {C}) ⊆ N′, then C is true in (R_{C} ∪ E_{C})^{∗}.

Proof. Suppose N is saturated on a set N′ and does not contain the empty clause. Let C be a ground instance of N, such that (N_{C} ∪ {C}) ⊆ N′.

If C is redundant or produces an equation, then it is true in (R_{C} ∪ E_{C})^{∗}. Let us therefore assume that C is neither redundant nor productive. In other words, E_{C} = ∅ and C is false in I_{C}. Using Lemma 5 we may infer that C is a reduced ground instance of N with respect to R_{C}. Also, C can not be the empty clause. Let s denote the maximal term in C.

(i) Suppose C is a clause Γ′, s ≈ s → Δ, where s ≈ s is either a maximal or a selected occurrence of an equation. The clause C′ = Γ′ → Δ can be obtained from C by selective or equality resolution. Since N is saturated on N_{C} ∪ {C}, the inference has to be redundant. Thus C′ has to be true in I_{C}, which contradicts that Γ′ ⊆ I_{C} and Δ ∩ I_{C} = ∅.

(ii) Suppose C is a clause Γ′, s ≈ t → Δ, where s ≻ t and s ≈ t is either a maximal or a selected occurrence of an equation. Then s ≈ t ∈ I_{C} and s is reducible by R_{C}. Let D = Λ → u ≈ v, Π be a clause that produces the rule u ≈ v, where u ≻ v and u is a subterm of s. Then C ≻^{c} D and using Lemma 6 we may infer that Λ ⊆ I_{C}, u ≈ v ∈ I_{C}, Π ∩ I_{C} = ∅, and D contains no selected equations.

Consider the inference

\frac{Λ → u ≈ v, Π Γ′, s[u] ≈ t → Δ}{Γ′, Λ, s[v] ≈ t → Δ, Π}

by (selective) superposition. Since N is saturated on N_{C} ∪ {C}, the conclusion C′ of this inference has to be true in I_{C}. This contradicts that (Γ′ ∪ Λ) ⊆ I_{C}, s[v] ≈ t ∈ I_{C} and (Δ ∪ Π) ∩ I_{C} = ∅.

(iii) Suppose C is Γ → Δ′, s ≈ t, where s ≻ t, s ≈ t is a maximal occurrence of an equation in C, and the term s is reducible by R_{C}. If s ≈ t occurs in Δ′ we can derive a contradiction again using the fact that N is in particular saturated (on N_{C} ∪ {C}) by ordered factoring. Hence s ≈ t is a strictly maximal occurrence in C. Let D = Λ → u ≈ v, Π, where C ≻^{c} D, be a clause that produces the rule u ≈ v, where u ≻ v and u is a subterm of s. Using Lemma 6 we may infer that Λ ⊆ I_{C}, u ≈ v ∈ I_{C}, Π ∩ I_{C} = ∅, and D contains no selected equations.

Consider the inference

\frac{Λ → u ≈ v, Π Γ → Δ′, s[u] ≈ t}{Γ, Λ → Δ′, Π, s[v] ≈ t}

by right superposition. Saturation of N on N_{C} ∪{C} implies that the conclusion C′ of this inference has to be true in I_{C}. This contradicts that (Γ ∪ Λ) ⊆ I_{C}, s[v] ≈ t ∉ I_{C}, and (Δ′ ∪ Π) ∩ I_{C} = ∅. □

Corollary 2 If N is saturated, then every non-redundant ground instance of N is productive.

Proof. Suppose C is a non-redundant ground instance of N, i.e., C is false in I_{C}. By Lemma 7 C is true in (R_{C} ∪ E_{C})^{∗}, which implies that E_{C} ≠ ∅. In other words, C produces an equation. □

Theorem 1 A saturated set of clauses N is consistent if and only if it does not contain the empty clause.

Proof. If N contains the empty clause, then it has no model. On the other hand, if N is saturated and consistent, then by Lemma 7 every ground instance C of N is true in (R_{C} ∪ E_{C})^{∗} and hence true in I. In other words, I is a model of N. □

Let us remark that while we have assumed that the reduction ordering ≻ is complete (i.e., total on ground terms), it is sufficient to require that ≻ be completable (i.e., contained in some complete ordering >). For if a set N of clauses is saturated with respect to some inference system E_{S}^{≻} (or P_{S}^{≻}), then it is also saturated with respect to the more restrictive system E_{S}^{>} (or P_{S}^{>}). Therefore our results apply not only to complete orderings, such as certain lexicographic path orderings, but to all completable ordering, for instance, all recursive path orderings.

We conclude this section with a remark on subsumption.

Definition 6 A clause C = Γ → Δ is said to subsume a clause D = Λ → Π if there exists a substitution σ such that Γσ ⊆ Λ and Δσ ⊆ Π. We say that C properly subsumes D if C subsumes D but not vice versa.

Proposition 1 If N ∪ {C} is a saturated and consistent set of clauses, where C subsumes D, then N ∪ {C, D} is also saturated.

Proof. Let I be the interpretation constructed from N ∪ {C, D}. Also, let N′ be the set of all ground instances of N ∪ {C, D} and N′′ be the set of all ground instances of N ∪ {C}. It suffices to show that all clauses in N′ \ N′′ are redundant. Let Dσ be a clause in N′ \ N′′. Since C subsumes D, the clause D can be written as Γ, Λ → Δ, Π, where Cτ = Γ → Δ, for some τ. Since Dσ ∉ N′′, we have Dσ ≻^{c} Cτσ. Since N ∪ {C} is saturated, Cτσ is true in I_{Dσ}, which implies that Dσ is also true in I_{Dσ}. Hence Dσ is redundant. □

4.3 Modular Redundancy Criteria

Clausal theorem proving can be interpreted as a process of constructing saturated sets of clauses. However, the notion of redundancy we have introduced above is too general to be directly applicable to theorem proving. In this section we describe sufficient conditions for redundancy that cover all simplification and deletion techniques common in rewrite-based theorem proving.

Definition 7 Let N be a set of clauses and C be a ground clause (not necessarily a ground instance of N). We call C composite with respect to N, if there exist ground instances C_{1}, …, C_{k} of N such that C_{1}, …, C_{k} ⊧ C and C ≻^{c} C_{j}, for all j with 1 ≤ j ≤ k. A non-ground clause is called composite if all its ground instances are composite.^{7}

Lemma 8 If a clause C is composite with respect to N, then for every ground instance Cσ there exist non-composite ground instances C_{1}, …, C_{k} of N such that C_{1}, …, C_{k} ⊧ Cσ and Cσ ≻^{c} C_{j}, for all j with 1 ≤ j ≤ k.

Proof. Let C be a clause that is composite with respect to N and let Cσ be a ground instance of C. Furthermore, let N′ = {C_{1}, …, C_{k}} be a minimal set of ground instances of N with respect to ≻_{mul}^{c}, such that C_{1}, …, C_{k} ⊧ Cσ and Cσ ≻^{c} C_{j}, for all j. We claim that all clauses C_{j} are non-composite. For if some clause C_{j} is composite with respect to N, then there exists a set N′′ = {D_{1}, …, D_{n}} of ground instances of clauses in N, such that D_{1}, …, D_{n} ⊧ C_{j}. But then (N′ \{C_{j}})∪N′′ ⊧ Cσ and N′ ≻_{mul}^{c} (N′ \{C_{j}})∪N′′, which contradicts the minimality assumption about N′. □

Lemma 9 Let C be a composite ground instance of some clause in N. If N is saturated on N_{C} and does not contain the empty clause, then C is redundant.

Proof. Let C_{1}, …, C_{k} be ground instances of N, such that C_{1}, …, C_{k} ⊧ C and C ≻^{c} C_{j}, for all 1 ≤ j ≤ k. We may use Lemma 7 to infer that each clause C_{j} is true in (R_{C_{j}} ∪ E_{C_{j}})^{∗} and hence true in I_{C}. Thus C is true in I_{C} and hence redundant. □

Definition 8 A ground inference π with conclusion B is called composite with respect to N if either some premise is composite, or else there exist ground instances C_{1}, …, C_{k} of N such that C_{1}, …, C_{k} ⊧ B and C ≻^{c} C_{j}, for all j with 1 ≤ j ≤ k, where C is the maximal premise of π. A non-ground inference is called composite if all its ground instances are composite.

Lemma 10 Let π be a composite ground instance of an inference from N with maximal premise C. If N is saturated on N_{C} and does not contain the empty clause, then π is redundant.

Proof. Suppose π is a composite ground instance of an inference from N with maximal premise C and conclusion B, where N is saturated on N_{C}. We may use Lemma 9 to infer that π is redundant whenever some premise is composite. If all premises are non-redundant, then there exist ground instances C_{1}, …, C_{k} of N such that C_{1}, …, C_{k} ⊧ B and C ≻^{c} C_{j}, for all j with 1 ≤ j ≤ k. Since N is saturated on N_{C} and C ≻^{c} C_{j}, for all j, each clause C_{j} is true in I_{C}. Hence B is true in I_{C}, which shows that the inference π is redundant. □

7Again, a more refined way of comparing substitution instances of clauses in N might be based on pairs of clauses and substitutions and involve the subsumption ordering on clauses.

Lemma 11 (i) If N ⊆ N′, then any inference or clause which is composite with respect to N is also composite with respect to N′.

(ii) If N ⊆ N′ and all clauses in N′ \ N are composite with respect to N′, then any inference or clause which is composite with respect to N′ is also composite with respect to N.

Proof. Part (i) is obvious; for part (ii) use Lemma 8. □

The lemma shows that compositeness with respect to a set N is preserved if clauses are added to N or if composite clauses are deleted. The concept of compositeness thus provides a useful basis for simplification and deletion in a theorem prover.

5 Theorem Proving with Simplification and Deletion

We next consider the problem of constructing a saturated set from a given set of clauses N.

5.1 Theorem Proving Derivations

A theorem prover computes derivations using the following two inference rules on sets of clauses:

Deduction: \frac{N}{N ∪ \{C\}} if N ⊧ C

Deletion:  \frac{N ∪ \{C\}}{N} if C is composite with respect to N ∪ \{C\}

Deduction adds clauses that logically follow from given clauses; deletion eliminates composite clauses.

Deduction of a clause D to N which triggers a subsequent deletion of another clause C represents a simplification. If D is needed to prove the compositeness of C, it will be smaller than C with respect to ≻^{c}, so that we have a derived inference

Simplification: \frac{\frac{N ∪ \{C\}}{N ∪ \{C, D\}}}{N ∪ \{D\}}

Note that simplification may require the deduction of (logically sound) clauses other than those that can be obtained by E_{S} or P_{S}. This is also the reason why we have not restricted the above deduction to a superposition calculus, but allow for the application of any sound inference rule.

For example, let → s ≈ t and → u ≈ v[s] be two unit clause, where s ≻ t and u ≻ v. If we deduce → u ≈ v[t] (by paramodulation, not superposition), then the clause → u ≈ v[s] becomes composite and hence can be deleted.

Definition 9 A (finite or countably infinite) sequence N_{0}, N_{1}, N_{2}, … of sets of clauses is called a theorem proving derivation if each set N_{i+1} can be obtained from N_{i} by deduction or deletion. The set N_{∞} = ⋃_{j} ⋂_{k≥j} N_{k} is called the limit of the derivation. Clauses in N_{∞} are called persisting.

Definition 10 A theorem proving derivation is called fair (with respect to E_{S} or P_{S}) if every inference from N_{∞} is composite with respect to ⋃_{j} N_{j}.

A fair derivation can be constructed, for instance, by systematically adding conclusions of noncomposite inferences from persisting clauses. It is important to notice that because of the monotonicity of the ground inferences with respect to ≻^{c} — the conclusions are smaller than the maximal premises — adding the conclusion of an inference makes the inference to become composite afterwards.

Definition 11 A set of clauses N is called complete (with respect to E_{S} or P_{S}) if all inferences from N are composite with respect to N.

For instance, any set containing the empty clause is complete. Another example of a complete set of clauses is the theory of a total order p:

→ p(x, x)
→ p(x, y), p(y, x)
p(x, y), p(y, z) → p(x, z)
p(x, y), p(y, x) → x ≈ y

The proof of completeness is rather tedious and proceeds by case analysis on the inequalities with respect to ≻ between the terms to be substituted for variables. (Any total reduction ordering on ground terms is suitable. We assume that p(s, t) ≻ p(u, v) if and only if either s ≻ u or else s = u and t ≻ v.) For example, consider the ordered resolution inference

\frac{p(x, y), p(y, z) → p(x, z) p(x, z), p(z, x) → x ≈ z}{p(x, y), p(y, z), p(z, x) → x ≈ z}

If any two of the variables x, y, and z are instantiated by the same ground term, the inference is composite as one of the premises would be composite. If pairwise distinct ground terms s, t, and u are substituted for x, y, and z, respectively, then the inference is ordered only if s ≻ u ≻ t. But then

\begin{matrix}p(t, u), p(u, s) & → & p(t, s), \\ p(s, t), p(t, s) & → & s ≈ t, \\ p(u, s), p(s, t) & → & p(u, t), \\ p(t, u), p(u, t) & → & t ≈ u \end{matrix} ⊧ p(s, t), p(t, u), p(u, s ) → s ≈ u .

In other words, the conclusion of the ground inference logically follows from ground instances of clauses simpler than the maximal premise. Thus the inference is composite.

Note that this case analysis on the ordering between variables—a technique that has also been described by Martin and Nipkow (1989) in the context of ordered completion of equations—is independent of the signature, that is, of any additional function or predicate symbols that might exist besides p.

Fairness, completeness, and saturation are related in the following way.

Lemma 12 If N_{0}, N_{1}, N_{2}, … is a fair theorem proving derivation (with respect to E_{S} or P_{S}), then N_{∞} is complete and every clause C in (⋃_{j} N_{j}) \ N_{∞} is composite with respect to N_{∞}.

Proof. If C is a clause in (⋃_{j} N_{j}) \ N_{∞} then it is composite with respect to some set N_{j} and hence composite with respect to ⋃_{j} N_{j}. We may use Lemma 11 to infer that (i) all clauses in in (⋃_{j} N_{j}) \ N_{∞} are composite with respect to N_{∞}, and (ii) every ground instance of an inference from N_{∞} is composite with respect to N_{∞}. □

Lemma 13 Any complete set of clauses that does not contain the empty clause is saturated.

Proof. Suppose N is complete set of clauses and does not contain the empty clause. We shall prove that N is saturated on N_{C} ∪ {C}, for all ground instances C of N.

Let C be minimal ground instance of N with respect to the clause ordering ≻^{c}, such that N is not saturated on N_{C} ∪ {C}. Then N is saturated on N_{C} and there exists some non-redundant ground instance π of an inference from N, the maximal premise of which is C. Since N is complete, the inference π has to be composite. Using Lemma 10 we may infer that π is redundant, which is a contradiction. □

Theorem 2 Let N_{0}, N_{1}, N_{2}, … be a fair theorem proving derivation (with respect to E_{S} or P_{S}). If ⋃_{j} N_{j} does not contain the empty clause, then N_{∞} is saturated and N_{0} is consistent.

Proof. By fairness, the set N_{∞} is complete. If it does not contain the empty clause, then by Lemma 13 it is saturated. Using Lemma 12 we may infer that the interpretation I constructed from N_{∞} is a model of ⋃_{j} N_{j}. □

5.2 Simplification and Deletion Techniques

Most simplification techniques proposed for theorem proving are specific tests for compositeness. We discuss some of these.

If C is a clause and N is a set of clauses, let in the following N_{C} denote the set of all (ground or non-ground) instances Dσ of clauses D in N such that C ≻^{c} Dσ. Let us write [N] ⊧ C if Nσ ⊧ Cσ, for all ground instances Cσ and Nσ of C and N, respectively. Note that [N] ⊧ C implies that C is composite in N, if C ≻^{c} D, for all clauses D in N. (N ⊧ C and C ≻^{c} D, for all clauses D in N, does not necessarily imply that C is composite in N. It may be the case that although C ≻^{c} D for each clause D in N, to prove that some ground instance Cσ follows from N requires to use a ground instance Dτ of N with Dτ ≻^{c} Cσ.)

Elimination of redundant atoms. Let C = Γ, u ≈ v → Δ be a clause in N. If N ⊧ Γ → u ≈ v, Δ, then N ⊧ Γ → Δ, so that C can be simplified to Γ → Δ. A particular case is the elimination of multiple occurrences of atoms in the antecedent. For example, if C = Γ, u ≈ v, u ≈ v → Δ, then the clause Γ, u ≈ v → u ≈ v, Δ is a tautology and hence trivially implied by N. Redundant atoms in the succedent can be eliminated in a similar way.

Case analysis. The first step in a case analysis consists of splitting a clause C = Γ → Δ into n clauses C_{i} = A_{i}, Γ → Δ, where [N_{C}] ⊧ Γ → A_{1}, …, A_{n}, Δ. Each clause C_{i} logically follows from C and hence can be deduced. If in addition there exist clauses D_{i}, such that N_{C} ⊧ D_{i} ⊃ C_{i} and C ≻^{c} D_{i}, for all i with 1 ≤ i ≤ n, then [N_{C} ∪ {D_{1}, …, D_{n}}] ⊧ C, which indicates that C is composite in N ∪ {D_{1}, …, D_{n}}.

In practice, simplification is usually employed to construct clauses D_{i} that are logically equivalent to the respective clauses C_{i}, but simpler than C. The possibility of such simplification depends to some extent on the choice of the “cases” C_{i}. The case analysis can also be applied recursively to the clauses C_{i}. Contextual rewriting (Zhang and Rémy 1985, Navarro 1987) or splitting of clauses (Ganzinger 1987b) are particular instances of a case analysis.

Contextual reductive rewriting. Let C = Γ → Δ, s ≈ t and D = Λ, A[u] → Π (or D = Λ → Π, A[u]) be clauses in N and σ be a substitution, such that (i) u is sσ, (ii) sσ ≻ tσ, (iii) D ≻^{c} Cσ, (iv) [N_{D}] ⊧ Λ → B, for all equations B ∈ Γσ, and (v) [N_{D}] ⊧ B → Π, for all equations B ∈ Δσ. Then D′ = Λ, A[tσ] → Π (or D′ = Λ → Π, A[tσ]) logically follows from N and moreover [N_{D} ∪ {D′}] ⊧ D. Since D ≻^{c} D′ this indicates that D is composite (and hence can be deleted) after D′ has been deduced.

Replacing D by D′ generalizes simplification by contextual reductive conditional rewriting as described by Ganzinger (1987a) for a completion procedure for conditional equations, and of course also covers ordinary (unconditional) rewriting. (In this context by a reductive conditional rewrite rule one means a clause C = Γ → Δ, s ≈ t, where s is a strictly maximal term. If the term s matches a proper subterm of a clause D, then Cσ ∈ N_{D}.) The contextual aspect of the simplification is expressed in conditions (iv) and (v) where an equation B needs to be true only for those substitutions that make Λ true and Π false. In practice, proofs of [N_{D}] ⊧ Λ → u ≈ v may be conducted by reductive conditional rewriting with (instances of) clauses in N_{C}, using equations in the (Skolemized) antecedent Λ as additional rewrite rules.

6 Refutation of Goals

In this section we consider situations in which a fair theorem proving derivation from some finite initial set of clauses N_{0} terminates after finitely many steps without encountering an inconsistency, so that for some k, N_{∞} = N_{k} is a finite complete set of clauses. Because of the powerful concept of redundancy which we have introduced before there is reason to believe that termination of completion is not unusual in practice.

Finite, complete and consistent sets N of clauses will also be called programs. A formula

¬G = ∃x⃗ (A_{1} ∧ … ∧ A_{n} ∧ ¬B_{1} ∧ … ∧ ¬B_{k})

is a logical consequence of a program N if and only if N ∪{G} is inconsistent, where G is the clause A_{1}, …, A_{n} → B_{1}, …, B_{k} (also called a goal).

The search for a refutation of N ∪ {G} may be simpler and more efficient for several reasons than the search for a refutation in general.

• Since N is complete, inferences between clauses in N are composite and remain composite at any step of a theorem proving derivation from N ∪ {G}. In other words, if N is complete and consistent, {G} forms a set of support for some refutation of N ∪ {G}, if N ∪ {G} is inconsistent. Notice that this is not true in general for arbitrary sets N of clauses.^{8} Also, clauses in N with selected equations need often not be considered during the refutation of goals.

8In general, the set-of-support restriction is not refutationally complete with paramodulation, or with ordered resolution. Snyder and Lynch (1991) describe a “lazy paramodulation” calculus that is complete with set of support.

• Under certain additional assumptions it may be sufficient to compute only so-called N-linear superposition inferences

\frac{C D}{B}

where C ∈ N and D ∉ N. For example, linear SLD-resolution and linear conditional narrowing are refutationally complete for certain Horn clause programs.

• Theorem provers usually employ some backtracking mechanism. If an inference system is don’t care nondeterministic, in the sense that a refutation can be constructed regardless of the order in which inference rules are applied, then backtracking is not needed. For example, rewriting with convergent rewrite systems as it is employed in many completion procedures is don’t care nondeterministic. In certain cases it may even be decidable whether a goal G is refutable, e.g., if the inferences in any refutation of a goal are strictly decreasing in that the conclusion is smaller than some premise with respect to a given well-founded ordering. Thus the validity problem in an equational theory represented by a finite convergent rewrite system is decidable.

The completeness of linear superposition for refutation of goals can be proved for programs with certain syntactic properties.

Definition 12 A quasi-Horn clause is a clause Γ, Σ → Δ or Γ, Σ → Δ, s ≈ t, where Γ contains only function equations, Σ ∪ Δ contains only predicate equations, and sσ ≈ tσ is strictly maximal in Σσ ∪ Δσ, for all ground substitutions σ.

Quasi-Horn clause programs correspond to what are sometimes called Horn clause specifications over “built-in Booleans.” In such programs predicates are defined by clauses Γ → Δ with no function equations in the succedent, whereas functions are defined by clauses Γ → Δ, s ≈ t. The fact that predicates in Γ → Δ, s ≈ t have to be simpler (with respect to the ordering ≻) than the function equation s ≈ t, generalizes the idea of a hierarchical specification over built-in Booleans.

The following example defines a function for ordered insertion where the inequalities are expressed by a predicate < and a derived predicate ≥. Any lexicographic path ordering with a precedence ≻ in which insert precedes > and ≥ will ensure the required syntactic properties.

x′ < 0 →  (1)
→ 0 < x′  (2)
x < y → x′ < y′  (3)
x′ < y′ → x < y  (4)
x < y, x ≥ y →  (5)
→ x < y, x ≥ y  (6)
→ insert(nil, x) = cons(x, nil)  (7)
→ x ≥ y, insert(cons(y, l), x) = cons(x, cons(y, l))  (8)
x ≥ y → insert(cons(y, l), x) = cons(y, insert(l, x))  (9)

It is evident from the syntactic restrictions that merging paramodulation cannot be applied to quasi-Horn clauses and that equality factoring is essentially identical to ordered factoring. Quasi-Horn clauses with a funtion equation in the succedent cannot be premises of ordered resolution and ordered factoring inferences. Moreover, if D has no function equation in its succedent and B is obtained from C and D by one application of (selective) superposition, then B has no function equation in the succedent either.

Lemma 14 Let N ∪M be a complete set of quasi-Horn clauses with respect to an inference system E_{S}, where each clause in M contains selected equations, and let G_{1}, …, G_{n} be clauses with no function equation in the succedent. If N ∪ M ∪ {G_{1}, …, G_{n}} = N_{0}, N_{1}, … is a theorem proving derivation in which no deduction step adds a clause with a function equation in the succedent, then any (selective) superposition inference from N_{∞} is either N-linear or composite in N_{0}.

Proof. Let N_{0}, N_{1}, … be a derivation where no clause with a function equation in the succedent is ever deduced. Thus the only clauses in ⋃_{j} N_{j} with function equations in the succedent are those in N ∪ M. Since clauses in M contain selected equations, the first premise of any (selective) superposition inference from N_{∞} has to be in N. If the second premise is in N ∪ M, then the inference is composite, by the completeness of N ∪ M. If the second premise is not in N ∪ M, the inference is N-linear. □

The lemma indicates that for quasi-Horn programs the refutation of goals without function equations in the succedent is linear with respect to the equality part of the logic. Ordered resolution, which covers the non-functional aspects of the program, is still nonlinear (but fortunately is a rather restricted form of resolution). The clauses in M, which contain selected equations, might be called nonoperational. They have presumedly been used in the construction of the complete set N ∪ M, but are not needed for the refutation of goals.

Corollary 3 Let N ∪ M be a complete set of Horn clauses with respect to some inference system E_{S}, where each clause in M contains selected equations. Moreover, let G be a clause with empty succedent and let N ∪ M ∪ {G} = N_{0}, N_{1}, … be a theorem proving derivation in which no deduction step adds a clause with a non-empty succedent. Then N_{∞} is complete with respect to E_{S} if and only if it is complete with respect to N-linear (selective) superposition, N-linear ordered resolution, and selective and equality resolution.

Proof. By the completeness of N ∪ M, any inference is composite if both premises are in N ∪ M. Since any two-premise inference rule in E_{S} requires at least one premise with a non-empty succedent, the only non-composite inferences with two premises have to be N-linear. Selective and equality resolution require only one premise. □

The corollary indicates that certain ordered variants of conditional narrowing are complete for refuting the negations of a conjunction of equations in a complete set of conditional equations. Note that there are no restrictions about variables. The slightly weaker result obtained by Bertling and Ganzinger (1989) did not admit conditional rewrite rules with variables as their left side.

Let us next consider refutation of ground goals.

Definition 13 A clause C = Γ → Δ is called universally reductive if either the succedent Δ is empty, or else Δ can be written as Δ′, A such that (i) all variables of C also occur in A, (ii) Cσ is reductive for Aσ, for all ground substitutions σ, and (iii) if A is a function equation s ≈ t, then all variables of A occur in s and sσ ≻ tσ, for all ground substitutions σ.

Theorem 3 Let N ∪ M be a finite complete set of quasi-Horn clauses with respect to an inference system E_{S}, where each clause in M contains selected equations, and let G_{1}, …, G_{n} be ground clauses with no function equation in the succedent. If all clauses in N are universally reductive, then N ∪ M ⊧ ¬(G_{1} ∧ … ∧ G_{n}) is decidable by N-linear (selective) superposition, ordered factoring, selective and equality resolution, and (non-linear) ordered resolution.

Proof. The linearity property follows from Lemma 14. The stated requirements ensure that any non-composite inference is ground, so that the conclusion is smaller with respect to the well-founded ordering ≻^{c} than the maximal premise. As a consequence a finite fair derivation can be obtained by applying the given inference rules. □

In the example above, let M be the set consisting of clause (4) (i.e., assume that the condition of clause (4) is selected) and let N be the set of all remaining clauses. Then N and M satisfy the requirements of Theorem 3, hence the ground theory as specified by the example is decidable.

The above results do not cover goal solving, i.e., the process of finding substitutions that refute the goal. In the case of Horn clauses, all irreducible substitutions solving a goal can be enumerated by ordered conditional narrowing. This does not hold for quasi-Horn clauses, in general, as shown by the following example:

→ p, q
p → a ≈ b
q → c ≈ d
→ f(x, x, y, z) ≈ z
→ f(x, y, z, z) ≈ z

where a ≻ b ≻ c ≻ d ≻ p ≻ q and p and q are predicate constants. This set of quasi-Horn clauses is complete, but the solution {x ↦ h(a), y ↦ h(b), u ↦ h(c), v ↦ h(d)} for f(x, y, u, v) ≈ v cannot be obtained from the given axioms and the goal

f(x, y, u, v) ≈ v →

by paramodulation if the functional-reflexive axioms are not available. The difficulty arises from disjunctions of equations which, as in the example above, can easily be specified via propositional variables.

We conclude this section with a few remarks about “don’t care nondeterminism,” a frequent case of which occurs when a superposition inference is actually a simplification by contextual rewriting

\frac{Γ → s ≈ t, Δ Λ, A[sσ] → Π}{Γσ, Λ, A[tσ] → Δσ, Π}

such that “Γσ is true and Δσ is false in context Λ → Π” (as described formally in Section 5). Here Λ, A[sσ] → Π typically is a goal with no function equation in the succedent. Once the new goal Γσ, Λ, A[tσ] → Δσ, Π has been deduced, the old goal Λ, A[sσ] → Π becomes composite and can be deleted. In other words, no further inference with the old goal are required. If N is a Horn clause program this implies the ground confluence of conditional reductive rewriting.

Theorem 4 Let N ∪ M be a complete set of Horn clauses with respect to an inference system E_{S}, where each clause in M contains selected equations. Let N_{R} be a set of universally reductive instances of clauses in N, such that N_{R} has the same reductive ground instances as N. Then the initial algebras of N_{R}, N, and N ∪ M coincide, and recursive conditional rewriting with N_{R} is ground convergent.

Proof. The construction of an interpretation I for a saturated set of clauses K yields the initial model of K, if K is a set of Horn clauses (Bachmair and Ganzinger 1991). By Theorem 6, ground instances of clauses in M are non-productive and therefore do not contribute to the definition of the initial model I of N ∪ M. Ground instances of N_{R} are either redundant or productive. Since productive ground instances are reductive and N_{R} has the same reductive ground instances as N, we may conclude that each productive clause is an instance of a clause in N_{R}. The convergence of recursive rewriting with N_{R} is therefore an immediate consequence of the convergence of the set of rules R defining I. □

Note that if N ∪ M is also complete with respect to an extension of the given signature (and term ordering) by infinitely many new constants, the last result actually implies convergence on general terms. However, the completeness of N ∪ M need not be preserved under such an extension as the compositeness of an inference or clause may depend on the signature.

The clauses in M are inductive theorems of the clauses in N. The theorem thus opens up new ways of completion-based inductive theorem proving for Horn clauses, as it also avoids the problems with the undecidability of inductive reducibility for Horn clauses. This is another interesting application of explicit selection strategies for negative literals. With an appropriate coding, the selection of literals corresponds to the selection of induction variables in more traditional induction techniques. A more elaborate treatment of these ideas is beyond the scope of the present paper.

References

[1] L. Bachmair, 1991. Canonical equational proofs. Birkhäuser, Boston.

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

[3] L. Bachmair and H. Ganzinger, 1990. On restrictions of ordered paramodulation with simplification. In Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449, pp. 427–441, Berlin, Springer-Verlag.

[4] L. Bachmair and H. Ganzinger, 1991. Perfect Model Semantics for Logic Programs with Equality. In Proc. 8th Int. Conf. on Logic Programming, pp. 645–659, MIT Press.

[5] H. Bertling and H. Ganzinger, 1989. Completion-time optimization of rewrite-time goal solving. In Proc. 3rd Int Conf. Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 355, Berlin, Springer-Verlag.

[6] N. Dershowitz, 1991. A Maximal-Literal Unit Strategy for Horn Clauses. To appear in Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Lect. Notes in Comput. Sci., Berlin, Springer-Verlag.

[7] H. Ganzinger, 1987. A completion procedure for conditional equations. In S. Kaplan and J.-P. Jouannaud, editors, Conditional Term Rewriting Systems, Lect. Notes in Comput. Sci., vol. 308, pp. 62–83, Berlin, Springer-Verlag. Revised version in J. Symbolic Computation 11, pp. 51–81.

[8] H. Ganzinger, 1987. Ground term confluence in parametric conditional equational sepcifications. In STACS’87, Lect. Notes in Comput. Sci., vol. 247, pp. 286–298, Berlin, Springer-Verlag.

[9] J. Hsiang and M. Rusinowitch, 1987. On word problems in equational theories. In T. Ottmann, editor, Proc. 14th ICALP, Lect. Notes in Comput. Sci., vol. 267, pp. 54–71, Berlin, Springer-Verlag.

[10] J. Hsiang and M. Rusinowitch, 1989. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Submitted for publication.

[11] G. Huet, 1980. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the ACM, Vol. 27, pp. 797–821.

[12] D. Knuth and P. Bendix, 1970. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford.

[13] E. Kounalis and M. Rusinowitch, 1988. On word problems in Horn theories. In E. Lusk and R. Overbeek, editors, Proc. 9th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 310, pp. 527–537, Berlin, Springer-Verlag.

[14] U. Martin and T. Nipkow, 1989. Ordered Rewriting and Confluence. Technical Report, Univ. of Cambridge, Cambridge, U.K.

[15] M. Navarro, 1987. Técnicas de reescritura para especificaciones condicionales.. Dissertation, Universitat Politècnica de Catalunya.

[16] R. Nieuwenhuis and F. Orejas, 1991. Clausal Rewriting. To appear in Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Lect. Notes in Comput. Sci., Berlin, Springer-Verlag.

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

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

[19] W. Snyder and C. Lynch, 1991. Goal directed strategies for paramodulation. In R. Book, editor, Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 488, pp. 150–161, Berlin, Springer-Verlag.

[20] L. T. Wos, G. A. Robinson, D. F. Carson, and L. Shalla, 1967. The concept of demodulation in theorem proving. J. of the ACM, Vol. 14, pp. 698–709.

[21] H.T. Zhang and J-L. Rémy, 1985. Contextual Rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 202, pp. 46–62, Berlin, Springer-Verlag.