Rewrite-Based Equational Theorem Proving With Selection and Simplification^{∗}

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

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

To appear in the Journal of Logic and Computation.

Abstract

We present various refutationally complete calculi for first-order clauses with equality that allow for arbitrary selection of negative atoms in clauses. Refutational 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 refutational 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 it suffices to consider only those proofs that have support from the goals, without compromising refutational completeness. For certain classes of formulas the search space can be restricted 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 with Boolean conditions), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.

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 reasoning is the use of equations as one-way rewrite rules, so that a formula can be simplified by repeatedly replacing an instance of the left-hand side of a rule by its right-hand side until a simplest possible form (a normal form) is obtained. The completion procedure [22], for instance, attempts to construct a convergent rewrite system (one for which normal forms exist and are unique) from a given set of universally quantified equational axioms. A convergent rewrite system provides a decision procedure for the underlying equational theory: two terms can be rewritten to identical normal forms if, and only if, they are equal. The completion procedure may fail to find a convergent system, but has been extended to a refutationally complete theorem prover (cf. [25, 19, 3]). The two main components of completion are, first, a deductive inference rule called superposition and, secondly, various mechanisms for deleting redundant equations via simplification by rewriting. These features have been extended to conditional rewrite rules, that is, Horn clauses in which equations are the only atomic formulas [16, 15, 23]. In this paper we generalize the rewriting approach to general first-order clauses, and combine it with new techniques for equational theorem proving, based on the observation that superposition is a restricted form of paramodulation [33], while demodulation [36], a technique common in clausal theorem proving, is a form of simplification by rewriting.

∗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), by the German Ministery of Research and Technology (BMFT) under grants ITS 9102 and ITS 9103, and by a travel grant from the German Science Foundation (DFG). An extended abstract appeared in the proceedings of the Second Int. Workshop on Conditional and Typed Rewriting, Montréal 1990, LNCS 516.

The restrictions by which one obtains superposition from paramodulation can be formulated in terms of a well-founded ordering ≻ on terms and atomic formulas. Consider the paramodulation inference for variable-free formulas,

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

where Γ, Δ, Λ, and Π are multisets of atomic formulas and a clause A_{1}, …, A_{m} → B_{1}, …, B_{n} represents an implication A_{1} ∧ ⋯ ∧ A_{m} ⊃ B_{1} ∨ ⋯ ∨ B_{m}. If (i) s ≻ t and (ii.a) s ≈ t ≻ Γ, Δ, then the clause Γ → Δ, s ≈ t can be viewed as a conditional rewrite rule with positive and negative conditions (atoms in Γ and negated atoms in Δ, respectively) and the inference itself, as an application of this conditional rule to the second premise. We shall see that we can employ a slightly more restrictive notion of conditional rewriting by requiring in addition (ii.b) s ≻ u for all terms u in Γ (though we may not assume that s ≻ u for all terms u in Δ). To optimize the effect of conditional rewriting a rule should be applied to a maximal atom, (iii) u[s] ≈ v ≻ Λ, Π; or even to the maximal term thereof, (iv) u[s] ≻ v. Paramodulation calculi that satisfy all constraints, (i)–(iv), have been known as superposition calculi.

Ordered paramodulation, a calculus in which only conditions (i), (ii.a), and (iii) are imposed, was introduced and shown to be refutationally complete in [18]. The paper [34] established the completeness of paramodulation with constraints (i), (iii), and (iv). The claim, advanced in [37, 38], that refutational completeness is also preserved if conditions (i), (ii.a), (iii), and (iv) are imposed, turns out to be wrong [4]. For example, the set of clauses

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

where a, b, c, and d are constants, is unsatisfiable.^{1} However, if a ≻ b ≻ c, we can derive no other clause by superposition than the tautology b ≈ b, a ≈ c → a ≈ c.

1This example was communicated to us by Christopher Lynch and Wayne Snyder.

We have previously shown that completeness can be restored to the superposition calculus, with all constraints (i), (ii.a), (ii.b), (iii) and (iv) imposed, by adding either a new inference rule called equality factoring or else a paramodulation rule called merging paramodulation that satisfies all constraints except (iv), but needs to be applied only in certain special cases [4]. In this paper we consider another variant of this superposition calculus with slightly different ordering constraints and with arbitrary selection functions on negative literals. Furthermore, we show that superposition can be combined with a variety of simplification techniques including those used in the completion procedure. Such techniques, though indispensable for practical purposes, have received relatively little attention in the literature.

The papers [32] and [34] discuss simplification by (unconditional) rewriting, but derive their completeness results under more stringent conditions than appear to be necessary, so that only some but not all aspects of the completion procedure are covered. 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 sufficient criteria 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 refutational completeness. The notion of saturation of a set of clauses, in the sense that all non-redundant inferences are computed, generalizes completion to first-order clauses. The simplification techniques to which our results apply include, among others, deletion of tautologies, subsumption, case analysis, narrowing, 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 firstorder clauses include and generalize results about ordered completion of equations [3, 2], completion of Horn clauses [23, 15], and ground completion of Horn clauses with Boolean conditions [39, 16, 29].

The paper is organized as follows. In the next chapter we introduce our terminology and basic definitions. In Chapter 3 we describe superposition calculi with selection functions on negative literals. In Chapter 4 we introduce the notions of redundancy and saturation and prove the refutational completeness of our calculi in the presence of redundancy. In Chapter 5 we describe sufficient criteria for redundancy, outline an abstract framework for theorem proving with simplification. In Chapter 6 we discuss various specific simplification mechanisms, such as case analysis and contextual reductive rewriting. In Chapter 7 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.

An equation is an expression s ≈ t, where s and t are (first-order) terms built from given function symbols and variables.^{2} 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.

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.

2.2 Equality Herbrand interpretations

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. Occasionally, we identify a set of equations E with a symmetric binary relation in the obvious way. If E is a set of ground equations, we denote by E^{∗} the smallest congruence containing 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 C is true in every model of N.

2We may, where appropriate, assume the vocabulary of function symbols to be a many-sorted signature with the usual typing constraints for equations, terms and substitutions.

2.3 Convergent rewrite systems

Convergent rewrite systems provide a convenient formalism for describing and reasoning about equality interpretations. 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 has to be reducible by E.

A rewrite system E is said to be convergent if the rewrite relation ⇒_{E} is wellfounded 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 follows from the well-known critical pair lemma for term rewriting systems that left-reduced, well-founded ground rewrite systems are convergent (cf. [20]).

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 {{s, t}}, and an occurrence in the succedent with the multiset {{s}, {t}}. We identify clauses with finite multisets of occurrences of equations. By ≻^{o} we denote the twofold multiset ordering (≻_{mul})_{mul} of ≻, 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. In [4] we have identified an occurrence of an equation s ≈ t in the antecedent of a clause with the multiset {{s, t, ⊥}} (with an auxiliary and minimal symbol ⊥) 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 refutational completeness of the corresponding superposition calculus.

3 Ordered Inference Rules with Selection

We shall design inference rules for equational clauses that approximate a certain notion of “conditional rewriting.”

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.

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.

If the reduction ordering ≻ is total on ground terms (also called complete), then a reductive ground clause A_{1}, …, A_{m} → B_{1}, …, B_{n}, s ≈ t can be thought of as a conditional rewrite rule A_{1}, …, A_{m}, ¬B_{1}, …, ¬B_{n} → s ≈ t (with positive and negative conditions) where all conditions are strictly smaller than s ≈ t. A non-ground clause is reductive if one of its ground instances is potentially a conditional rule. Paramodulation corresponds to conditional rewriting applied to ground clauses: “replace s by t whenever all conditions are satisfied”. The completeness of paramodulation calculi, as we will show below, is ultimately based on a suitable definition of “satisfiability of conditions.”^{3}

We consider inference rules

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

where C_{1}, …, C_{n} (the premises) and C (the conclusion) are clauses. The following inference rules are defined with respect to ≻. The first inference rule encodes the reflexivity of equality:

3We remark that reductivity could be strengthened by replacing the condition “t ⪰̸ s” by “sσ ≻ tσ, for some ground substitution σ”. We have chosen a weaker notion of reductivity, as we apply our results not only to complete, but more generally to completable orderings (i.e., orderings that can be extended to a complete ordering). Even so, the definition may be improved, for it would suffice to require that “there exists a ground substitution σ such that s ≻′ t, for some (fixed) complete extension ≻′ of ≻”. For example, consider a vocabulary consisting of constants 0 and 1 and binary function symbols f and g. Let ≻ denote a lexicographic path ordering with f ≻ 1 ≻ 0 and g ≻ 0.

Then f(x, 1) and f(0, 0) are uncomparable, and hence f(x, 1) ⪰̸ f(0, 0) and f(0, 0) ⪰̸ f(x, 1), while all ground instances of f(x, 1) are greater than f(0, 0) in any complete extension of ≻. Consequently the equation f(x, 1) ≈ f(0, 0) is oriented from left to right in any reductive ground instance. For reasons of readability we nevertheless only use the more crude approximations.

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σ, Λσ → Πσ,^{4} 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.

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 replace ordered factoring by the following more general inference rule:

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 (iii) sσ ≈ tσ is a maximal occurrence of an equation in Γσ → Δσ, sσ ≈ tσ, s′σ ≈ t′σ.

An alternative is to keep ordered factoring and add 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.

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

The example in the introduction indicates that multiple occurrences of the maximal term in the succedent may cause the incompleteness of superposition alone. Repeated application of merging paramodulation to ground clauses (in conjunction with ordered factoring) has the effect of merging atoms in the succedent which contain the same maximal term. In the example, a merging paramodulation of the second clause into the first clause produces → a ≈ c, a ≈ c, from which we obtain → a ≈ c by ordered factoring. Equality factoring represents a different way of eliminating one occurrence of the maximal term in the succedent. In the example, b ≈ c → a ≈ c is obtained from the first clause by equality factoring. In either case, a contradiction can be derived with the new clause. Syntactically, equality factoring seems to be simpler and more intuitive. From the semantic point of view, merging paramodulation is attractive as it may serve to construct the “perfect” model of a consistent set of clauses, cf. [5].

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 binary inference with most general unifier σ, then Cσ ⪰̸^{c} Dσ. This additional ordering constraint excludes, for instance, the superposition of s ≈ t into s ≈ u, if s ≻ t ≻ u. 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 smaller (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.^{5} 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 → Π.

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.

5An 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.

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 inference 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 in [16]. (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 [12], 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 (called predicate terms) P (t_{1}, …, t_{n}), where P is some predicate symbol and t_{1}, …, t_{n} are terms built from function symbols and variables. Predicate terms are of a distinguished sort so that they cannot occur as proper subterms of any term. We then have equations s ≈ t between (non-predicate) terms, called function equations, and equations P (t_{1}, …, t_{n}) ≈ ⊤, called predicate equations, where ⊤ 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}) ≈ ⊤ by P (t_{1}, …, t_{n}).

Clauses of the form Γ, P (t_{1}, …, t_{n}) ≈ ⊤ → Δ or Γ → Δ, P (t_{1}, …, t_{n}) ≈ ⊤ in which P (t_{1}, …, t_{n}) ≈ ⊤ 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}) ≈ ⊤ on a clause Λ → Π, P (t_{1}, …, t_{n}) ≈ ⊤ results in a tautology Γσ, Λσ → Δσ, Πσ, ⊤ ≈ ⊤ and is therefore redundant. The remaining inferences are left or selective superpositions of the form

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

Note that the trivial equation ⊤ ≈ ⊤ 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.

To conclude this section, let us point out that the use of selection functions to disallow certain inferences generalizes the idea, underlying hyperresolution, of combining several inference steps into larger ones. For example, let → Γ_{1}, A_{1}, …, → Γ_{n}, A_{n} be positive (ground) clauses (called electrons) and let A_{1}, …, A_{n} → Δ be another (ground) clause (called the nucleus). If each atom A_{i} is strictly maximal in its respective positive clause, then → Γ_{1}, …, Γ_{n}, Δ can be obtained by a sequence of n selective resolution steps, where at each step one of the atoms A_{i} is selected. The same clause can be deduced by (positive) hyperresolution in one single inference. In other words, hyperresolution discards all intermediate clauses so as to prevent further inferences with them. However, a similar effect is achieved by selective resolution, as clauses with selected atoms must not occur as the first premise, so that selection essentially serves as a mechanism for marking “auxiliary” clauses that can only occur in inference sequences producing a non-auxiliary clause. Hyperresolution can be simulated by discarding newly deduced auxiliary clauses. One disadvantage of hyperresolution is that the same auxiliary clause may occur as an intermediate result in different “hyper-inferences” and, since it is always discarded, may have to be recomputed over and over again. With selection functions one has the option of keeping these auxiliary clauses, so as to avoid recomputation. (The above remarks also apply to general clauses, though for simplicity we have illustrated the approach with ground clauses only. Factoring needs to be applied to electrons only.) A similar technique has already been suggested in [24]. Systematic renaming of (positive into negative) atoms provides further flexibility for the application of selection functions [27]. We will moreover describe techniques for eliminating redundant clauses, so that, for example, redundant intermediate clauses may be ignored. Our completeness results below also show that hyperresolution and similar techniques can be combined with paramodulation and superposition. (Note however that right superposition steps can not be combined into hyper-inferences.)

4 Refutational 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. As is typical for such completeness proofs, we shall primarily have to argue about ground 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. Ground inferences that are not instances of general inferences may cause considerable technical problems. Many completeness results rely on the observation that if one includes all “functional-reflexive axioms” of the form f(x_{1}, …, x_{n}) ≈ f(x_{1}, …, x_{n}) and allows paramodulation into variables, then the conclusion of any paramodulation inference is an instance of a clause that can be deduced (in one or more steps) on the non-ground level. Since paramodulation into variables is impractical for automated theorem proving, we show instead that problematic ground inferences are superfluous for the purpose of establishing completeness.

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.

Note that (ordered) factoring is not required for this version of the Lifting Lemma, since we have defined clauses in terms of multisets (rather than sets) of atoms. Also note that a merging paramodulation on the ground level may correspond to a superposition inference on the non-ground level. (For a proof of a similar lifting lemma see [32].)

4.1 Construction of Equality Interpretations

Let N be a set of clauses and ≻ be a reduction ordering which is total on ground terms. The construction described in this section, as we will show later, defines a model for any set of clauses that is closed under sufficiently many superposition inferences and does not contain the empty clause. We construct partial interpretations by starting with the empty set and inspecting ground instances of N in ascending order. Whenever a ground clause C is false in the partial interpretation constructed so far, we attempt to set the truth value of an equation in C to true, so as to make C itself true. This process of gradually extending partial interpretations has to be set up in such a way that the satisfiability of previously considered clauses is preserved, the main difficulty being that changing the truth value of one equation may have a side effect on others. For example, if b ≈ c is true in a given partial interpretation, then by setting the truth value of a ≈ b one implicitly sets the truth value of a ≈ c as well. The ordering ≻^{c} is designed so as to eliminate some technical complications in dealing with these side effects.^{6} We describe partial interpretations via canonical sets of ground rewrite rules, which also allows us to restrict the attention to rewrite proofs when arguing about the validity of equations and clauses.

Formally, 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}.

If u ≈ v occurs in the succedent of C, the situation is different as C may produce an equation in I.

6A well-founded ordering on clauses has already been used in [38]—in an approach to constructing Herbrand interpretations which unfortunately does not always yield a desired model.

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 (partial) 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. The above calculi contain restricted versions of paramodulation. Both ordering constraints and selection of equations in the antecedent of a clause are ways of pruning the search space of ordinary paramodulation. 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 non-local restrictions which are based on a suitable 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′. A set 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. Recall that ≻ is assumed to be total on ground terms.

Lemma 6 Let N be a set of clauses saturated on N′ (with respect to some inference system E_{S} or P_{S}) and C = Γ → s ≈ t, Δ be 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 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 assume that 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 C′ 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′ with 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. By saturation, the conclusion of this inference has to be true in I_{C}, which again leads to a contradiction. In either case, 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 Again, we use induction on the clause ordering ≻^{c}. 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′. We assume that whenever D is a ground instance of N with C ≻^{c} D, then D is true in (R_{D} ∪ E_{D})^{∗} and hence true in I_{C}.

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 the induction hypothesis and Lemma 5, we may infer that C is reduced with respect to R_{C}. 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}. Let D = Λ → u ≈ v, Π be a clause that produces the rule u ≈ v, where C ≻^{c} D, 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. Then C is false in I_{C} but, by Lemma 7, is true in (R_{C} ∪ E_{C})^{∗}. This 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, it is inconsistent. 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.

5 Redundancy Criteria

Clausal theorem proving can be interpreted as a process of constructing saturated sets of clauses. We emphasize, however, that our notion of saturation differs from the one traditionally used in theorem proving, in that we do not require that a saturated set be closed under application of all inferences, but only under application of nonredundant inferences. We have proved completeness by showing that every saturated set that does not contain the empty clause, has a model that can be obtained by some standard construction based on a given well-founded ordering. We have defined redundancy in such a way that this model is uniquely characterized by the set of nonredundant ground (instances of) clauses. For instance, in the case of stratified logic programs, this model coincides with the unique perfect model of a program. Thus redundancy enables us to single out certain “preferred” models of a given saturated set of clauses, and also induces a notion of computation by conditional rewriting over such models. For further details see [5].

These observations apply to saturated sets of clauses, though, whereas in theorem proving one typically starts from an unsaturated set. During the construction of a saturated set we also would like to take advantage of redundancy, say, by deleting redundant clauses. Unfortunately, a clause need not remain redundant if new clauses are derived and added to a given set of clauses. For example, given three clauses → s ≈ u, → s ≈ t, and t ≈ u → a ≈ b, and an ordering in which a ≻ b ≻ s ≻ t ≻ u, the third clause can be shown to be redundant. But the set is not saturated and from the first two clauses we may deduce → t ≈ u, at which point the previously redundant clause becomes productive (and hence non-redundant). In this section, we introduce another notion, compositeness, that is slightly weaker for saturated sets (compositeness implies redundancy on saturated sets), but has the advantage of being stable under both addition of clauses and deletion of composite clauses. Compositeness is general enough to cover all simplification and deletion techniques common in rewrite-based theorem proving and will be the fundament for our abstract framework for simplification-based theorem provers.

Definition 6 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 (and ordering ≻), 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.

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

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. Also note that if > is an extension of the ordering ≻, then a clause or inference is composite with respect to N and > whenever it is composite with respect to N and ≻.

Let I be a (sound) clausal inference system and let I(N) be the set of clauses that can be deduced from premises in N by applying an inference in I. A theorem prover based on I can be viewed as a procedure that applies the following transition rules to sets of clauses:

Deduction:  \frac{N}{N ∪ \{C\}}  if C ∈ I(N)

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

Deduction adds logical consequences; 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}, so that I may contain inference rules other than those in E_{S} and P_{S}.

For example, let → s ≈ t and → u ≈ v[s] be two unit clauses, 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. (These two inferences correspond to the simplification of right-hand sides of rewrite rules in the Knuth-Bendix completion procedure.) Actually one might even consider to add clauses which are not logical consequences, as long as consistency or inconsistency is preserved.

Inferences not in E_{S} and P_{S} are optional and not strictly needed for refutational completeness. Hence, for the remainder of this section let I denote some inference system from the families E_{S} or P_{S}. (If necessary, we write I^{≻} to indicate the underlying ordering.)

Definition 8 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 9 A theorem proving derivation is called fair (with respect to I) if every inference from N_{∞} (in I) is composite with respect to ⋃_{j} N_{j}.

It can readily be seen that if an ordering ≻ is contained in another ordering >, then any fair derivation with respect to I^{≻} is also fair with respect to I^{>}. It is also important to notice that because of the monotonicity of the ground inferences with respect to ≻^{c} (the conclusions are smaller than the maximal premises) an inference becomes composite once its conclusion has been deduced. Therefore a fair derivation can be constructed by systematically adding conclusions of non-composite inferences from persisting clauses.

Definition 10 A set of clauses N is called complete if all inferences from N are composite with respect to N.

For instance, any set containing the empty clause is complete. Another (nontrivial) example of a complete set of clauses is the theory of a total order, cf. Example 2 in Section 6. The connection between fairness, completeness, and saturation is summarized in the following lemmas.

Lemma 12 The limit N_{∞} of a fair theorem proving derivation is complete, while all clauses in (⋃_{j} N_{j}) \ N_{∞} are 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, using Lemma 11, composite with respect to ⋃_{j} N_{j}. Again applying Lemma 11 we infer that all clauses in (⋃_{j} N_{j}) \ N_{∞} are composite with respect to N_{∞}. Therefore every inference from N_{∞} is composite with respect to N_{∞} by virtue of the fact that fairness implies the compositeness of all inferences from N_{∞} with respect to ⋃_{j} N_{j}.

A reduction ordering ≻ is called complete if it is total on ground terms, and is called completable if it is contained in some complete ordering >.

Lemma 13 Let ≻ be a reduction ordering and > be a complete reduction ordering containing ≻. If N is a complete set of clauses with respect to I^{≻} and does not contain the empty clause, then N is saturated with respect to I^{>}.

Proof If N is complete with respect to I^{≻}, then it is also complete with respect to I^{>}. Suppose N does not contain the empty clause. We shall prove that N is saturated with respect to I^{>} on N_{C} ∪ {C}, for all ground instances C of N.

Suppose that C is a 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.

The following theorem applies not only to complete orderings, such as certain lexicographic path orderings, but also to completable orderings, for instance, all recursive path orderings.

Theorem 2 Let N_{0}, N_{1}, N_{2}, … be a fair theorem proving derivation. 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}.

6 Simplification and Deletion Techniques

The notion of compositeness provides a framework for proving the compatiblity of simplification and elimination techniques with any of our inference systems. (Such a technique is called compatible with an inference system if its application does not affect the refutational completeness of the latter.) It should be emphasized that compositeness as we have defined it here is not necessarily compatible with other ordering-based inference systems for first-order logic with equality. In particular the “basic” variants of the systems E_{S} and P_{S} as they are discussed in [7] require a different notion of compositeness and, hence, different techniques for simplification and elimination.

The purpose of this section is to give examples of techniques that have been proposed in the literature and, in some cases, to extend them to first-order clauses. While some of these techniques have been proved useful in the Horn clause case by practical experiments on a number of nontrivial examples [16], more experience is needed for the case that we consider here. Note that the set of composite clauses (with respect to some given set of clauses N) may not even be recursively enumerable. For example, given a complete set E of equations, the problem of proving the compositeness of some equation s ≈ t with respect to E is essentially equivalent to proving that s ≈ t is an inductive consequence of E.

So we cannot hope for a complete calculus of compositeness. Also there is a trade-off between performing many unsophisticated compositeness tests in relatively short time or, alternatively, trying to eliminate as many new clauses as possible by a more extensive search for proofs of compositeness. The latter option will have to be chosen whenever one actually intends to verify the consistency of a (consistent) set of clauses. In a practical implementation one would have to leave it to the user to specify particular tactics. Only simplification techniques that do not involve too much computational overhead should be provided automatically. In the extreme case the user himself will have to provide certain proofs of compositeness, perhaps with the assistance of a proof editor or a similar tool, and have the system only check the ordering constraints of clauses involved.

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.

Proofs of compositeness. The definition of compositeness for a clause C with respect to a set of clauses N requires one to prove that any ground instance Cσ follows from smaller ground instances of N. Different ground instances may require different proofs, and in general induction on all ground substitution instances is needed. In many cases such an induction can be turned into an implicit induction over the term ordering, which is the intention behind the following definition.

If N and M are sets of clauses and if C is a (general) clause we say that N implies C below M, denoted N ⊧_{≺M} C, if there exist instances (not necessarily ground) C_{i}σ_{i} of N and clauses D_{i} in M, 1 ≤ i ≤ n, such that ⊧ C_{1}σ_{1} ∧ … ∧ C_{n}σ_{n} ⊃ C and D_{i} ≻^{c} C_{i}σ_{i}, for all i with 1 ≤ i ≤ n.^{7} If M is a singleton {D} we also write N ⊧_{≺D} C.

Proposition 1 If N ∪ {C} ⊧_{≺C} C then C is composite in N.

Proof Suppose that there exist instances C_{i}σ_{i} of N ∪ {C}, 1 ≤ i ≤ n, such that ⊧ C_{1}σ_{1} ∧ … ∧ C_{n}σ_{n} ⊃ C and C ≻^{c} C_{i}σ_{i}. Let Cτ be a ground instance of C. We use induction on the clause ordering ≻^{c} and assume that all ground instances Cρ of C such that Cτ ≻^{c} Cρ are composite in N. We have C_{1}σ_{1}τ, …, C_{n}σ_{n}τ ⊧ Cτ and Cτ ≻^{c} C_{i}σ_{i}τ by stability of ≻ (and ≻^{c}) under substitution. If C is different from any of the C_{i} we are done. Otherwise, if, say, C_{1} = C then we may apply the induction hypothesis and assume that C_{1}σ_{1}τ is composite in N, that is, there exist ground instances D_{j} of N, 1 ≤ j ≤ m, such that C_{1}σ_{1}τ ≻^{c} D_{j} and D_{1}, …, D_{m} ⊧ C_{1}σ_{1}τ. Hence D_{1}, …, D_{m}, C_{2}σ_{2}τ, …, C_{n}σ_{n}τ ⊧ Cτ. This way we can replace all occurrences of C among the C_{i} by smaller instances from N and infer the compositeness of Cτ with respect to N.

This essentially means that for a proof of compositeness of C, smaller instances of C, in the sense made precise by the proposition, may be used. Also note that if N ⊧_{≺M} C_{i}, for all i with 1 ≤ i ≤ m, and N ∪ {C_{1}, …, C_{m}} ⊧_{≺M} C, then N ⊧_{≺M} C.

Proposition 2 Let C be the conclusion of an inference π with a set of premises M ⊆ N. Let σ be the most general unifier that is computed for π. If N ⊧_{≺Mσ} C then π is composite in N.

The proof is similar to the one for the last proposition.

Note that the property ⊧_{≺M} does not explicitly refer to the vocabulary and to the algebra of ground terms. Hence ⊧_{≺M} is stable under enrichments of the vocabulary, whenever the ordering ≻ can be extended correspondingly.

7Note that ⊧ C_{1}σ_{1} ∧ … ∧ C_{n}σ_{n} ⊃ C is equivalent to requiring C_{1}σ_{1}τ, …, C_{n}σ_{n}τ ⊧ Cτ, for all ground substitutions τ.

Case analysis. Case analysis uses valid disjunctions to split a formula into subcases. The first step in a case analysis consists of splitting a clause C = Γ → Δ into n + 1 clauses C_{i} = A_{i}, Γ → Δ, 1 ≤ i ≤ n, plus C_{0} = Γ → Δ, A_{1}, … A_{n}, where the A_{i} are arbitrary equations, and n ≥ 1. Any of the C_{i} is greater than the original clause C. Suppose, however, that these can be further simplified, that is, there exist clauses D_{i}, 0 ≤ i ≤ n, such that N ⊧_{≺C} D_{i} ↔ C_{i} and C ≻^{c} D_{i}. Then, replacing C by the D_{i} is an admissible simplification as C is composite in (N \ {C}) ∪ {D_{1}, …, D_{n}}.

Often case analysis needs to be applied recursively to some of the cases C_{i} to be able to simplify it. Contextual rewriting [39, 28] or splitting of clauses [15] are particular techniques for case analysis. In contextual rewriting the A_{i} are chosen such that the existence of simplifications D_{i} for the corresponding C_{i}, i > 0, is guaranteed.

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 = 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 if D′ = Λ, A[tσ] → Π (or D′ = Λ → Π, A[tσ], respectively), N ⊧ D′. Moreover N ∪ {D′} ⊧_{≺D} D. Therefore D is composite in (N \ {D}) ∪ {D′} and hence can be deleted from N after D′ has been added.

Replacing D by D′ generalizes simplification by contextual reductive rewriting as described in [16] for a completion procedure for conditional equations, and in particular covers ordinary unconditional rewriting (also called demodulation). In the case of full first-order clauses by a reductive conditional rewrite rule one means a clause C = Γ → Δ, s ≈ t, where s is a strictly maximal term that, in addition, contains all variables of C. If the term s matches a proper subterm of a clause D, then D ≻^{c} Cσ. The equations in Δ play the role of negative conditions, and (v) above gives a criterion for verifying them. In practice, proofs of implications such as Λ → B and B → Π, cf. (iv) and (v), respectively, can be carried out by adding the skolemized antecedent to N and invoking contexual reductive rewriting recursively.

Example 1. This example demonstrates how case analysis and contextual reductive rewriting are to be combined in practice. In the following we assume a two-sorted signature with sorts for elements and lists.^{8} We do not specify any vocabulary for elements as the compositeness proofs will not depend on it anyway. Suppose a lexicographic path ordering ≻ to be given over a precedence in which

sorted ≻ ins ≻ : ≻ nil ≻ <.

The following clauses define < to be a total ordering, nil is the empty list, “:” is “cons” on elements and lists, ins is ordered insertion of elements into lists, and sorted specifies when a list is sorted in ascending order.

x < x →  (1)
x < y, y < x →  (2)

8Technically, as nonequality atoms A are viewed as equations A ≈ ⊤, we need a third sort for non-equality atoms.

→ x < y, x ≈ y, y < x  (3)
x < y, y < z → x < z  (4)
→ ins(nil, x) ≈ x:nil  (5)
→ y < x, ins(y:l, x) ≈ x:y:l  (6)
y < x → ins(y:l, x) ≈ y:ins(l, x)  (7)
→ sorted(nil)  (8)
→ sorted(x:nil)  (9)
sorted(y:l) → sorted(x:y:l), y < x  (10)
sorted(x:y:l) → x < y, x ≈ y  (11)
sorted(x:l) → sorted(l)  (12)
sorted(l) → sorted(ins(l, x))  (13)
y < x, sorted(y:l) → sorted(y:ins(l, x))  (14)

Superposing 7 into 14^{9} yields as conclusion

y < x, z < x, sorted(y:z:l) → sorted(y:z:ins(l, x)).  (15)

Using the previously described methods, in particular Proposition 2, we will prove that this inference is composite with respect to 1–14. All instances of 1–14 that we use in the (alternative) proof of 15 will be smaller than the instance

y < x, sorted(y:z:l) → sorted(y:ins(z:l, x))  (16)

of 14. This clause is the maximal premise of the inference that produced 15, instantiated by the most general unifier of the inference. Compositeness of 15 then follows from Proposition 2.

Analysis on y < z, y ≈ z, and z < y splits 15 into the cases

y < z, y < x, z < x, sorted(y:z:l) → sorted(y:z:ins(l, x))  (17)
y ≈ z, y < x, z < x, sorted(y:z:l) → sorted(y:z:ins(l, x))  (18)
z < y, y < x, z < x, sorted(y:z:l) → sorted(y:z:ins(l, x))  (19)
y < x, z < x, sorted(y:z:l) → sorted(y:z:ins(l, x)),
y < z, y ≈ z, z < y  (20)

20 follows from 3. In clause 19 we may use 1 and 11 to conclude that its antecedent is unsatisfiable. For clause 17 we make a case analysis on sorted(z:ins(l, x)), yielding

sorted(z:ins(l, x)), y < z, y < x, z < x, sorted(y:z:l)
→ sorted(y:z:ins(l, x))  (21)
y < z, y < x, z < x, sorted(y:z:l)
→ sorted(y:z:ins(l, x)), sorted(z:ins(l, x))  (22)

21 can be contextually rewritten, using 10, to

sorted(z:ins(l, x)), y < z, y < x, z < x, sorted(y:z:l) → ⊤ ≈ ⊤

914 itself can be generated from superposing 7 into 13. To prove the compositeness of 15 would be required for making the process of saturating 1–13 become finite.

which is a tautology. (Remember that non-equality atoms A are considered as abbreviations for equations A ≈ ⊤. Note also that the properties for < allow to prove the negation of z < y in 10 from the condition y < z in 21.) 22 can be contextually rewritten by 13 to

y < z, y < x, z < x, sorted(y:z:l) → sorted(y:z:ins(l, x)), ⊤ ≈ ⊤

which is again a tautology. The condition sorted(z:l) of 13 follows from sorted(y:z:l) by 12. In a similar way one can prove the compositeness of 18.

Subsumption. Subsumption is one of the few simplification techniques which 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 C in N 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. Any ordering ⊳ that is well-founded on all sets of pairs (C, σ) which denote the same ground clause Cσ may be lexicographically combined with ≻^{c} and used for the definitions of redundancy and compositeness. As an example one may take ⊳ to be the subsumption ordering, so that (C, σ) is considered greater than (D, τ), if Cσ ≻^{c} Dτ or else if Cσ = Dτ and D properly subsumes C. Then a clause that is strictly subsumed by a clause in N becomes composite in N. For the sake of simplicity we have chosen not to use this slightly more sophisticated formalism in this paper.

Exploiting ordering constraints. The above technique of proofs of compositeness is too weak in certain cases and needs to be extended by exploiting the ordering constraints that are attached to the various inference rules. This has been recognized in the context of unfailing completion of equations in [26] and applied to first-order clauses in [21]. The latter paper in particular also proposes to propagate ordering constraints from inference to inference by explicitly attaching them to the clauses. A precise analysis of refutational completeness issues for this very useful variation of ordered inference systems can be found in [31].

The method is roughly as follows. An ordering constraint γ is a quantifier-free first-order formula over atomic formulas of the form s = t or s ≻ t, where s and t are terms over the given vocabulary. A solution of γ is a ground substitution σ for the variables in γ such that γσ is true in the algebra of ground terms over the given vocabulary, with “=” and “≻” interpreted as syntactic equality and as the given (complete) reduction ordering, respectively. The ordering restrictions that are attached to the inference rules of our calculi can be viewed as constraints in this sense. For example, a right superposition of the form

\frac{u ≈ v → s ≈ t l[w] ≈ r}{uσ ≈ vσ → l[t]σ ≈ rσ}

is constrained by

sσ ≻ tσ ∧ sσ ≻ uσ ∧ sσ ≻ vσ ∧ lσ ≻ rσ ∧ (lσ ≻ sσ ∨ (sσ = lσ ∧ tσ ≻ rσ)).

(In the presence of a complete reduction ordering ≻, a constraint of form x ⪰̸ y can be equivalently written as y ≻ x.) The relation ⊧_{≺M} may be generalized to include ordering constraints in the following way. If N and M are sets of clauses, if γ is an ordering constraint, and if C is a (general) clause we say that N implies C below M and γ, denoted N ⊧_{≺M}^{γ} C, if there exist instances C_{i}σ_{i} of N (not necessarily ground) and clauses D_{i} in M, 1 ≤ i ≤ n, such that C_{1}σ_{1}τ, …, C_{n}σ_{n}τ ⊧ Cτ and D_{i}τ ≻^{c} C_{i}σ_{i}τ, 1 ≤ i ≤ n, for all solutions τ of γ. In other words, proofs of C from N need only be given for those instances of C that satisfy the given constraint γ. Proposition 2 can now be sharpened as follows.

Proposition 3 Let C be the conclusion of an inference π with a set of premises M ⊆ N. Let σ be the most general unifier that is computed for π and let γ be the ordering constraint associated with π. If N ⊧_{≺Mσ}^{γ} C then π is composite in N.

Example 2. An example of a complete set of clauses is the theory of a total nonstrict 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

Completeness can be established by applying Proposition 3 to the inferences between these clauses. Any total reduction ordering on ground terms is suitable. We only 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}

The associated ordering constraint, in a somewhat simplified form, is

p(x, z) ≻ p(x, y) ∧ p(x, z) ≻ p(y, z) ∧ p(x, z) ≻ p(z, x).

The constraint then implies that x ≻ z ≻ y. Moreover

( p(y, z) ∧ p(z, x) ⊃ p(y, x) ) ∧
( p(x, y) ∧ p(y, x) ⊃ x ≈ y ) ∧
( p(z, x) ∧ p(x, y) ⊃ p(z, y) ) ∧
( p(y, z) ∧ p(z, y) ⊃ y ≈ z )
⊃  ( p(x, y) ∧ p(y, z) ∧ p(z, x) ⊃ x ≈ z )

is valid, and all premises of this implication are smaller than the second premise of the resolution inference for any solution of x ≻ z ≻ y. Therefore, using Proposition 3, we may conclude the compositeness of this inference. As in the first example, the proof of compositeness is independent of the signature, that is, of any additional function or predicate symbols that might exist besides p.

7 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. It is known, for instance, that with the right choice of ordering, saturation by ordered resolution terminates for large classes of formulas (without equality); see [13] for further details. Recently some of these results have been extended to include equality [14, 9]. In particular in the latter paper we demonstrate that the powerful concept of redundancy which we have introduced above allows us to design simplification rules appropriately so that termination is in fact always guaranteed. In such cases completion becomes a decision procedure for satisfiability.

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

∃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, but N ∪ {G} is inconsistent, then {G} forms a set of support for some refutation of N ∪ {G}. Notice that this is not true in general for arbitrary sets N of clauses.^{10} Also, clauses in N with selected equations often need not be considered during the refutation of goals.

• Under certain additional assumptions it may be sufficient to compute only socalled N-linear binary inferences where one premise is contained in N, while the other is not. 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.

10In general, the set-of-support restriction is not refutationally complete with paramodulation, or with ordered resolution. In [35] a “lazy paramodulation” calculus is described that is complete with set of support.

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

Definition 11 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 clauses define predicates by clauses with no function equations in the succedent. They define functions by clauses Γ → Δ, s ≈ t, possibly with predicate equations as “negative conditions” Δ. In addition, all predicate equations, positive or negative, are smaller than the equation s ≈ t. 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 function equation in the succedent cannot be premises of ordered resolution and ordered factoring inferences. Moreover, if a quasi-Horn clause is superposed on a clause which has no function equation in its succedent then the conclusion of this inference has no function equation in the succedent either.

Definition 12 A pair (N, M) of finite sets of clauses is called a quasi-Horn clause program if (i) N ∪ M is complete with respect to some inference system E_{S}, (ii) N is a set of quasi-Horn clauses without equations selected by S, and (iii) M is a set of clauses where each clause has a function equation in its antecedent that is selected by S. If in addition N consists of Horn clauses only, then (N, M) is called a Horn clause program.

The following modification of a previous example is a quasi-Horn clause program with M = ∅. It defines a function for ordered insertion where the inequalities are expressed by a predicate < and a derived predicate ≥. The set of clauses is complete with respect to any lexicographic path ordering with precedence ins, ≥, < (in decreasing order).

sx < 0 →
→ 0 < sx
x < y → sx < sy
sx < sy → x < y
x < y, x ≥ y →
→ x < y, x ≥ y
→ ins(nil, x) ≈ x:nil
→ x ≥ y, ins(y:l, x) ≈ x:y:l
x ≥ y → ins(y:l, x) ≈ y:ins(l, x)

Lemma 14 Let (N, M) be a quasi-Horn clause program, and let G_{1}, …, G_{n} be clauses with no function equation in the succedent. There exists a fair theorem proving derivation N_{0}, N_{1}, … from N_{0} = N ∪ M ∪ {G_{1}, …, G_{n}} in which only N-linear superposition, ordered resolution, and equality resolution inferences are added and where no inferences involving premises from M are computed.

Proof We construct the derivation N_{0}, N_{1}, … by only adding E_{S} inferences (in a systematic way to achieve fairness). Therefore, if N_{i} contains a clause with function equations in the succedent, this clause is already contained in N ∪ M. Clauses in M contain selected function equations, hence cannot take part in inferences which are not already composite in N ∪ M. Therefore the first premise of any non-composite (selective) superposition inference from N_{i} has to be in N, while the second premise is not in N ∪ M. This proves the linearity property for superposition inferences.

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 Horn clause program. Suppose, moreover, that G is a clause with an empty succedent. There exists a fair theorem proving derivation N_{0}, N_{1}, … from N_{0} = N ∪ M ∪ {G} in which only N-linear superposition, N-linear ordered resolution, and equality resolution inferences are added.

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. If the derivation is restricted to add inferences from E_{S} only, no new clause with a non-empty succedent is ever added.

The corollary in particular says that conditional narrowing can be further restricted by the ordering constraints and selection functions of our paramodulation inference rules and remain a complete method for solving conjunctions of equations.

Let us next consider refutation of ground goals.

Definition 13 A clause C is called universally reductive if there exists an equation A in C such that (i) all variables of C occur in A, (ii) Aσ is strictly maximal in Cσ, for all ground substitutions σ, and (iii) if A is a function equation s ≈ t, then A occurs in the succedent of C, all variables of A occur in s, and sσ ≻ tσ, for all ground substitutions σ.

Theorem 3 Let (N, M) be a quasi-Horn clause program, and let G_{1}, …, G_{n} be ground clauses without function equations in the succedent. If all clauses in N are universally reductive, then N ∪ M ⊧ ¬(G_{1} ∧ … ∧ G_{n}) is decidable by N-linear superposition, ordered factoring, equality resolution, and (non-linear) ordered resolution.

Proof From Lemma 14 follows the existence of a fair theorem proving derivation from N ∪ M ⊧ ¬(G_{1} ∧ … ∧ G_{n}) in which only inferences of the indicated kind are computed. Additionally, any non-composite inference produces a new ground clause which is smaller with respect to the well-founded ordering ≻^{c} than the maximal premise. As a consequence, fair derivations of this kind are finite.

In the example above, where M = ∅, N, the requirements of Theorem 3 are satisfied, 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 solutions of a goal can be enumerated by ordered conditional narrowing. Ordered narrowing is linear ordered superposition where one additionally keeps track of the generated substitutions, and thereby not only refutes a goal but moreover computes its solutions. In the quasi-Horn clause case there may be a refutation of a goal without a witness, that is, a ground substitution that is a solution of the goal. Consider the single clause program

→ r(a), r(b)

together with the goal

r(x) → .

The goal is clearly refutable, but has no solution. On the other hand, there are cases in which some existing solution cannot be found by paramodulation.^{11} Consider the quasi-Horn program

→ 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. The goal

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

has a solution

x ↦ a, y ↦ b, u ↦ c, v ↦ d

which cannot be found by paramodulation without using functional reflexive axioms. Only the solutions x ↦ y and u ↦ v can be found this way.

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 6). 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.

11We assume an appriopriate extension of paramodulation by keeping track of substitutions into goal variables

Theorem 4 Let N ∪ M be a Horn clauses program. 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 (unique) minimal models (initial algebras) of N_{R}, N, and N ∪ M, respectively, coincide, and recursive conditional rewriting with N_{R} is ground convergent.

Proof If K is a saturated set of Horn clauses, the construction of an interpretation I yields the initial model of K [5]. By Lemma 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.

The theorem is of practical relevance only if N_{R} is finite. Otherwise the rewite relation induced by it may not be decidable. Note that if N ∪ M is also complete with respect to an extension of the given signature by infinitely many new constants and with respect to all possible extensions of the given ordering to the new terms, the last result actually implies general convergence on terms with variables. For certain kinds of orderings (e.g., path orderings) and simplification techniques (cf. section 6) completeness of N ∪M will in fact be preserved under such extensions of the signature,

In a Horn clause program, the clauses in M are inductive theorems of the clauses in N. The theorem thus indicates a technique of completion-based inductive theorem proving for Horn clauses. This is another interesting application of selection functions for negative literals. These ideas have been investigated in detail in [17].

8 Conclusions

The main results of this paper are (i) inference systems for first-order clauses with equality with very restrictive local ordering constraints and selection of negative literals, and (ii) a general notion of redundancy that allows for additional global restrictions of the search space. Local restrictions refer to the premises of an inference whereas global restrictions depend on the current state of the theorem proving process, that is, its database of clauses, perhaps together with information of how they have been deduced. The paper sets a framework in which concrete theorem provers can be embedded and their refutational completeness be verified. One might argue that completeness is not an issue in practice. This may be true for some applications. It is certainly not true for others, including proof by consistency, implicit induction, the derivation of executable functional or logic programs from their specifications, and deciding the word problem in first-order theories. All these applications require “compilation” of a given set of source clauses into an equivalent complete set of target clauses. The local and global restrictions on the saturation process increase the chances for the termination of this compilation process considerably.

More recently, our work has been extended in several ways. In [7] we consider “basic” variants (inspired from basic narrowing) of the inference systems that we have presented here and prove refutational completeness in the presence of an appropriate (and different) notion of redundancy. (Independently, Nieuwenhuis and Rubio [30] have obtained similar results.) In [31] the problem of refutational theorem proving for clauses with ordering constraints is investigated. In the setting of this paper one may move the ordering constraints from the meta-level to the object level and consider them part of the formulas. This appears to simplify certain technicalities that arise in practical implementations. In [6] we extend the present concepts to a nonclausal setting and admit arbitrary, quantifier-free first-order formulas. In [8] we consider the problem of theorem proving for hierarchic theories where a set of first-order clauses extends an arbitrary primitive theory. We obtain similar results as in the present paper for a slightly extended inference system.

Future work should concentrate on practical implementation of and experimentation with the concepts of this paper. Fortunately, certain subproblems have been solved recently, in particular the problem of solving ordering constraints for the lexicographic path ordering [11, 31]. With this work on implementation we would like to find more examples of interesting first-order theories that can be finitely completed. We also would like to investigate the trade-off between computing many inferences fast or, alternatively, applying computationally complex techniques for testing the redundancy of inferences and clauses. For mathematically difficult cases of consistency proofs we will certainly need to be able to combine user-given proof plans with automatic techniques for simplification and elimination. This links our work to work on logical frameworks and higher-order logic.

The methods that we have applied in this paper are essentially semantic. Our construction of equality interpretations for sets of clauses lets monotone inference systems be viewed as processes which must be able to reduce minimal clauses that are false in the interpretation to still smaller false clauses. For inconsistent sets of clauses the minimal counterexample eventually must become the empty clause. Our notion of redundancy is a natural consequence of this view, as a minimal false clause cannot be a logical consequence of smaller (and therefore valid) clauses. It would be useful to complement this semantic method by proof-theoretic techniques. Proof transformation and proof reduction form the basis of an abstract framework for theorem proving (with elimination of redundant formulas) that has been proposed in [10]. While corresponding proof normalization results have been established for (conditional or unconditional) rewrite systems, it is not clear to what extent this approach can be applied to full first-order logic with equality. For some preliminary work in this direction, see [1].

Acknowledgements. We are grateful to Marianne Haberstrau and Robert Nieuwenhuis for finding two errors in a preliminary version of the paper. We also wish to thank Robert Nieuwenhuis, Wayne Snyder, Uwe Waldmann and the referees for valuable comments.

References

[1] L. Bachmair. Proof normalization for resolution and paramodulation. In Proc. 3rd Int Conf. Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 15–28, Berlin, 1989. Springer-Verlag.

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

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

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

[5] L. Bachmair and H. Ganzinger. Perfect model semantics for logic programs with equality. In Proc. International Conference on Logic Programming ’91, pages 645–659. MIT Press, 1991.

[6] L. Bachmair and H. Ganzinger. Non-clausal resolution and superposition with selection and redundancy criteria. In A. Voronkov, editor, Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 273–284, Berlin, 1992. Springer-Verlag.

[7] L. Bachmair, H. Ganzinger, Chr. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, Automated Deduction — CADE’11, volume 607 of Lecture Notes in Computer Science, pages 462–476, Berlin, 1992. Springer-Verlag.

[8] L. Bachmair, H. Ganzinger, and U. Waldmann. Theorem proving for hierarchic first-order theories. In H. Kirchner and G. Levi, editors, Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 420–445, Berlin, 1992. Springer-Verlag. Revised version to appear in AAECC.

[9] L. Bachmair, H. Ganzinger, and U. Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. Technical Report MPI-I-93-204, Max-Planck-Institut für Informatik, Saarbrücken, 1993.

[10] M. P. Bonacina and J. Hsiang. Completion procedures as semidecision procedures. In S. Kaplan and M. Okada, editors, Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, pages 206–232, Berlin, 1991. Springer-Verlag.

[11] H. Comon. Solving inequations in term algebras. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, pages 62–69, June 1990.

[12] N. Dershowitz. A maximal-literal unit strategy for horn clauses. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, pages 14–25, Berlin, 1991. Springer-Verlag.

[13] Chr. Fermüller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem. 1992. To appear.

[14] Chr. Fermüller and G. Salzer. Ordered paramodulation and resolution as decision procedure. In Proc. LPAR’93, volume (to appear) of Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag.

[15] H. Ganzinger. Ground term confluence in parametric conditional equational specifications. In Proc. 4th Symp. on Theoretical Aspects of Computer Science, Passau, volume 247 of Lecture Notes in Computer Science, pages 286–298, Berlin, 1987. Springer-Verlag.

[16] H. Ganzinger. A completion procedure for conditional equations. In Proc. 1st Int’l Workshop on Conditional Term Rewriting, Orsay, 1987, volume 308 of Lecture Notes in Computer Science, pages 62–83, Berlin, 1988. Springer-Verlag.

[17] H. Ganzinger and J. Stuber. Inductive theorem proving by consistency for firstorder clauses. In J. Buchmann, H. Ganzinger, and W.J. Paul, editors, Informatik — Festschrift zum 60. Geburtstag von Günter Hotz, pages 441–462. Teubner– Verlag, 1992. Also in Proc. CTRS’92, LNCS 656, pp. 226–241.

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

[19] J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. 14th ICALP, volume 267 of Lecture Notes in Computer Science, pages 54–71, Berlin, 1987. Springer-Verlag.

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

[21] C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue Française d’Intelligence Artificielle, 4(3):9–52, 1990. Special issue on automatic deduction.

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

[23] E. Kounalis and M. Rusinowitch. On word problems in Horn theories. In E. Lusk and R. Overbeek, editors, Proc. 9th Int. Conf. on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 527–537, Berlin, 1988. Springer-Verlag.

[24] R. Kowalski and P. Hayes. Semantic trees in automatic theorem proving, pages 87–101. American Elsevier, 1969.

[25] D. Lankford. Canonical inference. Technical Report ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin, 1975.

[26] U. Martin and T. Nipkow. Ordered rewriting and confluence. In M. Stickel, editor, Proc. 10th CADE, volume 449 of Lecture Notes in Computer Science, pages 366–380, Berlin, 1990. Springer-Verlag.

[27] B. Meltzer. Theorem-proving for computers: Some results on resolution and renaming. Computer Journal, 8:341–343, 1966.

[28] M. Navarro. Técnicas de Reescritura para Especificaciones Condicionales. PhD thesis, Universidad Politécnica de Cataluña, Barcelona, 1987.

[29] R. Nieuwenhuis and F. Orejas. Clausal rewriting. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, pages 246–261, Berlin, 1991. Springer-Verlag.

[30] R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In ESOP’92, volume 582 of Lecture Notes in Computer Science, pages 371–389, Berlin, 1992. Springer-Verlag.

[31] R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In Automated Deduction — CADE’11, volume 607 of Lecture Notes in Computer Science, pages 477–491, Berlin, 1992. Springer-Verlag.

[32] G. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM J. Comput., 12:82–100, 1983.

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

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

[35] W. Snyder and C. Lynch. Goal directed strategies for paramodulation. In Proc. RTA’91, volume 488 of Lecture Notes in Computer Science, pages 150– 161, Berlin, 1991. Springer-Verlag.

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

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

[38] H. T. Zhang. Reduction, superposition and induction: Automated reasoning in an equational logic. PhD thesis, Rensselaer Polytechnic Institute, Troy, NY, USA, 1988.

[39] H. T. Zhang and J.-L. Rémy. Contextual rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, volume 202 of Lecture Notes in Computer Science, pages 46–62, Berlin, 1985. Springer-Verlag.