MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Associative-Commutative Superposition

Leo Bachmair Harald Ganzinger

MPI–I–93–267 December 1993

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

Im Stadtwald D 66123 Saarbrücken

Germany Addresses

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

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

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

many, hg@mpi-sb.mpg.de

Acknowledgements

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

Abstract

We present an associative-commutative paramodulation calculus that generalizes the associativecommutative completion procedure to first-order clauses. The calculus is parametrized by a selection function (on negative literals) and a well-founded ordering on terms. It is compatible with an abstract notion of redundancy that covers such simplification techniques as tautology deletion, subsumption, and simplification by (associative-commutative) rewriting. The proof of refutational completeness of the calculus is comparatively simple, and the techniques employed may be of independent interest.

Keywords

Term Rewriting, Theorem Proving, Equational Deduction

Contents

1 Introduction 1

2 Preliminaries 1 2.1 Clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 2.2 Reduction Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.3 Associative-Commutative Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . 3

3 Associative-Commutative Superposition 4 3.1 Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Lifting Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.3 Redundancy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

4 Refutational Completeness 7

5 Summary 11

1 Introduction

Rewrite techniques are one of the more successful approaches to equational reasoning. In theorem proving these techniques usually appear in the form of completion-like procedures, such as ordered completion (Bachmair, Dershowitz and Plaisted 1989, Hsiang and Rusinowitch 1987), associative-commutative completion (Peterson and Stickel 1981), or basic completion (Bachmair, Ganzinger, Lynch, et al. 1992, Nieuwenhuis and Rubio 1992). Traditionally completion procedures were formulated for sets of equations (unit clauses), but ordered completion has been generalized to arbitrary non-unit clauses, resulting in several variants of paramodulation called superposition (Rusinowitch 1991, Zhang 1988, Bachmair and Ganzinger 1990, Pais and Peterson 1991), and the basic strategy has actually first been developed for first-order clauses. Associativity and commutativity have been built into ordered paramodulation (Paul 1992, Rusinowitch and Vigneron 1991), a calculus (Hsiang and Rusinowitch 1991) that does not generalize completion, but includes similar rewrite techniques; and Wertz (1992) designed an associative-commutative superposition calculus. Unfortunately, the completeness proofs proposed for these calculi are technically involved and quite complicated.

The calculus described in this paper is obtained by applying the technique of extended rules (Peterson and Stickel 1981) to a superposition calculus of Bachmair and Ganzinger (1994). A similar calculus has been discussed by Wertz (1992), and our completeness proof, like Wertz’s proof, is based on the model construction techniques we originally proposed in Bachmair and Ganzinger (1990). The main difference with our current approach is that we use non-equality partial models to construct an equality model. These modifications were motivated by our recent work on rewrite techniques transitive relations in general Bachmair and Ganzinger (1993), and allow us to more naturally deal with associative-commutative rewriting.

Completion procedures are based on commutation properties (often called “critical pair lemmas”) of the underlying rewrite relation. We believe that our approach may be of independent interest in that it provides a general method for extending such procedures from unit clauses to Horn clauses to full clauses. Clauses are interpreted as conditional rewrite rules (with positive and negative conditions); new clauses need to be inferred with suitably designed inference rules, so that this clausal rewriting relation is welldefined and satisfies the required commutation properties. Associative-commutative superposition represents a non-trivial application of this general methodology.

The next section contains basic notions and terminology of theorem proving and rewriting. The associative-commutative superposition calculus is described in Section 3, and proved complete in Section 4.

2 Preliminaries

2.1 Clauses

We consider first-order languages with equality. A term is an expression f(t_{1}, …, t_{n}) or x, where f is a function symbol of arity n, x is a variable, and t_{1}, …, t_{n} are terms. For simplicity, we assume that equality is the only predicate in our theory. By an atomic formula (or atom) we mean a multiset {s, t}, called an equality and usually written s ≈ t, where s and t are terms.^{1} A literal is either a multiset (of multisets)

1The symmetry of equality is thus built into the notation.

{{s}, {t}}, called a positive literal and also written s ≈ t, or a multiset {{s, t}}, called a negative literal and written s ≉ t or ¬(s ≈ t). A clause is a finite multiset of literals. We write a clause by listing its literals ¬A_{1}, …, ¬A_{m}, B_{1}, …, B_{n}, or as a disjunction ¬A_{1} ∨ ⋯ ∨ ¬A_{m} ∨ B_{1} ⋯ ∨ B_{n}. An expression is said to be ground if it contains no variables.

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

An interpretation is called an equality interpretation if it satisfies the reflexivity axiom

x ≈ x

the transitivity axiom

x ≉ y ∨ y ≉ z ∨ x ≈ z

and all congruence axioms

x ≉ y ∨ f(…, x, …) ≈ f(…, y, …)

where f ranges over all function symbols. (Symmetry is already built into the notation.) We say that I is an equality model of N if it is an equality interpretation satisfying N. A set N is equality satisfiable if it has an equality model, and equality unsatisfiable otherwise.

We will consider the problem of checking whether a given set of clauses has an equality model, and for that purpose have to reason about Herbrand interpretations. Two concepts are useful in this context: rewrite systems and reduction orderings.

2.2 Reduction Orderings

An ordering is a transitive and irreflexive binary relation. A rewrite relation is a binary relation ≻ on terms such that s ≻ t implies u[sσ] ≻ u[tσ], for all terms s, t, u[sσ], and u[tσ] in the given domain.^{2} By a rewrite ordering we mean a transitive and irreflexive rewrite relation; by a reduction ordering, a transitive and well-founded rewrite relation. (A binary relation ≻ is well-founded if there is no infinite sequence t_{1} ≻ t_{2} ≻ … of elements.)

Any ordering ≻ on a set S can be extended to an ordering on finite multisets over S (which for simplicity we also denote by ≻) as follows: M ≻ N if (i) M ≠ N and (ii) whenever N(x) > M(x) then M(y) > N(y), for some y such that y ≻ x. If ≻ is a total (resp. well-founded) ordering, so is its multiset extension. If ≻ is an ordering on terms, then its multiset extension is an ordering on equations; its twofold multiset extension, an ordering on literals; and its threefold multiset extension, an ordering on clauses.

2In our notation for terms we follow Dershowitz and Jouannaud (1990).

2.3 Associative-Commutative Rewriting

An equivalence (relation) is a reflexive, transitive, and symmetric binary relation. A congruence (relation) is an equivalence such that s ≻ t implies u[s] ≻ u[t], for all terms s, t, u[s], and u[t] in the given domain. Note that if I is an equality interpretation, then the set of all pairs (s, t) and (t, s), for which s ≈ t is true in I, is a congruence relation on ground terms. Conversely, if ∼ is a congruence relation, then the set of all ground equations s ≈ t, for which s ∼ t, is an equality interpretation. In short, equality interpretations can be described by congruence relations. Rewrite systems can be used to reason about congruence relations.

By a rewrite system we mean a binary relation on terms. Elements of a rewrite system are called (rewrite) rules and written s → t. If R is a rewrite system, we denote by →_{R} the smallest rewrite relation containing R. The transitive-reflexive closure of →_{R} is denoted by →_{R}^{∗}; while ↔_{R}^{∗} denotes the smallest congruence relation containing R. A rewrite system R is said to be terminating if the rewrite relation →_{R} is well-founded.

We assume that some function symbols f are associative and commutative, i.e., satisfy the axioms

f(x, f(y, z)) ≈ f(f(x, y), z)
f(x, y) ≈ f(y, x)

For the rest of the paper, let AC be a set of such axioms. We write f ∈ AC, if AC contains the associativity and commutativity axioms for f, and also use AC to denote the binary relation containing the pairs (f(x, f(y, z)), f(f(x, y), z)) and (f(x, y), f(y, x)). We say that two terms u and v are AC-equivalent if u ↔_{AC}^{∗} v.

A reduction ordering ≻ is AC-compatible if u′ ↔_{AC}^{∗} u ≻ v ↔_{AC}^{∗} v′ implies u′ ≻ v′, for all terms u, u′, v, and v′. If ≻ is AC-compatible, we write u ⪰ v to indicate that u ≻ v or u ↔_{AC}^{∗} v. We say that a rewrite system R is AC-terminating if there exists an AC-compatible reduction ordering ≻ such that s ≻ t, for all rules s → t in R.

Associativity and commutativity are built into rewriting via matching. If R is a rewrite system, we denote by AC\R the set of all rules u′ → v, such that u′ ↔_{AC}^{∗} u for some rule u → v in R. The rewrite relation →_{AC\R} corresponds to rewriting by R via AC-matching. We say that a term t can be rewritten (modulo AC) to another term t′ if t →_{AC\R} t′. Terms that cannot be rewritten are said to be in AC-normal form or AC-irreducible. We write u ↓_{AC\R} v if there exist terms u′ and v′ such that u →_{AC\R}^{∗} u′ ↔_{AC}^{∗} v′ ←_{AC\R}^{∗} v. Given an AC-compatible reduction ordering, we also write u ↔_{AC∪R}^{⪯t} v (resp. u ↔_{AC∪R}^{≺t} v) to indicate that there exists a sequence

t_{0} ↔_{AC∪AC\R} ⋯ ↔_{AC∪AC\R} t_{n}

such that t ⪰ t_{i} (resp. t ≻ t_{i}), for all i with 0 ≤ i ≤ n.

If R is AC-terminating and we have u ↓_{AC\R} v, for all terms u and v with u ↔_{AC∪R}^{∗} v, then R is called AC-convergent. We shall use AC-convergent rewrite systems to describe equality models of AC.

It is a standard result from the theory of term rewriting (see Dershowitz and Jouannaud 1990 for details and further references) that an AC-terminating rewrite system R is AC-convergent if (i) u ↓_{AC\R} v whenever u ←_{AC\R} t ↔_{AC} v (a property called local AC-coherence) and (ii) u ↓_{AC\R} v whenever u ←_{AC\R} t →_{R} v (a property called local AC-confluence).

Any rewrite system R can easily be extended to a locally AC-coherent system by a technique proposed by Peterson and Stickel (1981). An extended rule is a rewrite rule of the form f(x, u) → f(x, v), where f ∈ AC, u is a term f(s, t), and x is a variable not occurring in u or v. We also say that f(x, u) → f(x, v) is an extension of u → v. If R is a rewrite system, we denote by R^{e} the set R plus all extensions of rules in R. Any rewrite system AC\R^{e} is locally AC-coherent: if u ←_{AC\R^{e}} t ↔_{AC} v, then u ↔_{AC}^{∗} u′ ←_{AC\R^{e}} v, for some term u′.

The local AC-confluence property is satisfied whenever it can be shown to hold for certain “minimal” rewrite sequences u ←_{AC\R} t →_{R} v that are also called “critical overlaps.” We only have to consider certain ground rewrite systems R where critical overlaps involve extended rules in R^{e}. This is summarized in the following lemma.

Lemma 1 Let R be a ground rewrite system contained in an AC-compatible reduction ordering ≻ and suppose that no left-hand side of a rule in R can be rewritten modulo AC by any other rule in R or any extended rule in R^{e}. Furthermore, let t be a ground term, such that for all ground instances f(u, u′) → f(u, u′′) and f(v, v′) → f(v, v′′) of extended rules in R^{e}, where f(u, u′) ↔_{AC}^{∗} f(v, v′) and t ⪰ f(u, u′), we have f(u, u′′) ↓_{AC\R^{e}} f(v, v′′). Then w ↓_{AC\R^{e}} w′ for all ground terms w and w′ such that w ↔_{AC∪AC\R}^{⪯t} w′.

If the same conditions are only satisfied for ground instances of extended rules with t ≻ f(u, u′), then w ↓_{AC\R^{e}} w′ for all ground terms w and w′ such that w ↔_{AC∪AC\R}^{≺t} w′.

The lemma can be proved by standard techniques from term rewriting.

3 Associative-Commutative Superposition

We formulate our inference rules in terms of a reduction ordering. Furthermore, negative literals in a clause may be marked, in which case they are said to be selected. We assume that at least one literal is selected in each clause in which the maximal literal is negative. (If the maximal literal is positive, there may be no selected literals.)

Let ≻ be a well-founded AC-compatible reduction ordering, such that s ↔_{AC}^{∗} t or s ≻ t or t ≻ s, for all ground terms s and t. (Such orderings have been described by Narendran and Rusinowitch (1991) and Rubio and Nieuwenhuis (1993).) We say that a clause C ∨ s ≈ t is reductive for s ≈ t (with respect to ≻) if there exists a ground instance Cσ ∨ sσ ≈ tσ such that sσ ≻ tσ and sσ ≈ tσ ≻ Cσ. By an extended clause we mean a reductive clause C ∨ f(x, s) ≈ f(x, t), where f ∈ AC, s is a term f(u, v), and x is a variable not occurring in C, s, or t. We also say that C ∨ f(x, s) ≈ f(x, t) is an extension of C ∨ s ≈ t. We will see that only extensions of certain reductive clauses without selected literals are needed. (Such extensions are themselves reductive.)

Associativity and commutativity are built into the inference rules via AC-unification. Two terms u and v are AC-unifiable if uσ ↔_{AC}^{∗} vσ, for some substitution σ. If two terms u and v are AC-unifiable, then there exists a complete set of AC-unifiers CSU_{AC}(u, v), such that for any substitution σ with uσ ↔_{AC}^{∗} vσ there exist substitutions τ ∈ CSU_{AC}(u, v) and ρ, such that xσ ↔_{AC}^{∗} (xτ)ρ, for all variables x in u and v. We assume that a function CSU_{AC} is given and call a substitution in CSU_{AC}(u, v) a most general AC-unifier of u and v.

3.1 Inference Rules

The calculus S_{AC}^{≻} consists of the following inference rules. (We assume that the premises of an inference share no common variables. If necessary the variables in one premise need to be renamed.)

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

where (i) σ is a most general AC-unifier of s and s′, (ii) the clause Cσ ∨ sσ ≈ tσ is reductive for sσ ≈ tσ and C ∨ s ≈ t either contains no selected literals or is an extended clause,^{3} (iii) the clause Dσ ∨ uσ ≈ vσ is reductive for uσ ≈ vσ and either contains no selected literals or is an extended clause, and (iv) s′ is not a variable.

Negative AC-Superposition: \frac{C, s ≈ t D, u[s′] ≉ v}{Cσ, Dσ, u[t]σ ≉ vσ}

where (i) σ is a most general AC-unifier of s and s′, (ii) the clause Cσ ∨ sσ ≈ tσ is reductive for sσ ≈ tσ and C ∨ s ≈ t either contains no selected literals or is an extended clause, (iii) the literal u ≉ v is selected in D ∨ u ≉ v and vσ ⪰̸ uσ, and (iv) s′ is not a variable.

Reflective AC-Resolution:  \frac{C, u ≉ v}{Cσ}

where σ is a most general AC-unifier of u and v and u ≉ v is a selected literal in the premise.

AC-Factoring:  \frac{C, s ≈ t, s′ ≈ t′}{Cσ, tσ ≉ t′σ, s′σ ≈ t′σ}

where σ is a most general AC-unifier of s and s′, t′σ ⊁ tσ, the literal sσ ≈ tσ is maximal in Cσ, and the premise contains no selected literals.

3.2 Lifting Properties

In proving the refutational completeness of a superposition calculus S_{AC}^{≻}, we shall have to argue about ground instances of clauses and inferences. The connection between the general level and the ground level is usually stated in the form of so-called “lifting” properties.

Let C_{1} … C_{n} be clauses and let

\frac{C_{1}σ … C_{n}σ}{D}

be a ground inference, i.e., all clauses C_{i}σ and D are ground. (We assume that each clause C_{i}σ is marked in the same way as C_{i}; that is, Lσ is selected in Cσ if and only if L is selected in C.) We say that this ground inference can be AC-lifted if there is an inference

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

3In other words, selection is ignored for extended clauses.

such that Cσ ↔_{AC}^{∗} D. In that case, we also say that the ground inference is an ACinstance of the general inference.

Lifting is no problem for resolution and factoring inferences, but is more difficult for superposition inferences. For example, if N contains two clauses f(x, x) ≈ x and a ≈ b, where a ≻ b, then there is a superposition inference from ground inferences

\frac{a ≈ b f(a, a) ≈ a}{f(a, b) ≈ a}

but no superposition inference from the clauses themselves. To prove completeness, one has to show that all necessary inferences can be AC-lifted. Let us illustrate the conditions under which AC-superposition inferences can be lifted. (The case of negative AC-superposition is similar.)

Let C ∨ s ≈ t and D ∨ u[s′] ≈ v be two clauses, each either containing no selected literals or being an extended clause. An AC-superposition inference

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

from ground instances of these clauses, where s′τ ↔_{AC}^{∗} sτ, can be AC-lifted if s′ is a non-variable subterm of u. (Proof. The ordering restrictions require that sτ ≈ tτ is strictly maximal in Cτ and sτ ≻ tτ, and uτ ≈ vτ is strictly maximal in Dτ and uτ ≻ vτ. Consider the inference

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

where σ is a most general AC-unifier of s and s′, such that for some substitution ρ we have xτ ↔_{AC}^{∗} (xσ)ρ, for all variables x occurring in s′ or s, and yτ = (yσ)ρ, for all other variables y. It can easily be shown that Cσ ∨ sσ ≈ tσ is reductive for sσ ≈ tσ and Dσ ∨ uσ ≈ vσ is reductive for uσ ≈ vσ. Also, s′ is not a variable, so that the inference is an AC-superposition inference. Moreover, the conclusion of the ground inference is AC-equivalent to an instance of the conclusion of the general inference.)

3.3 Redundancy

Simplification techniques, such as tautology deletion, subsumption, demodulation, contextual rewriting, etc., represent an essential component of automated theorem provers. These techniques are based on a concept of redundancy (Bachmair and Ganzinger 1994), which we shall now adapt to the AC-case.

Let RA denote the set consisting of the reflexivity axiom, F the set of all congruence axioms, and T the set consisting of the transitivity axiom, cf. Section 2. Furthermore, for any ground term s, let T_{⪯s} be the set of all ground instances u ≉ v ∨ v ≉ w ∨ u ≈ w of the transitivity axiom, for which s ⪰ u and s ⪰ v and s ⪰ w; and T_{≺s} be the set of all ground instances for which s ≻ u and s ≻ v and s ≻ w;

Let N be a set of clauses. A ground clause C (which need not be an instance of N) is said to be AC-redundant with respect to N (and ordering ≻) if there exist ground instances C_{1}, …, C_{k} of N, such that C ≻ C_{j}, for all j with 1 ≤ j ≤ k, and C is true in every model of AC ∪ RA ∪ F ∪ T_{⪯s} ∪ {C_{1}, …, C_{k}}, where s is the maximal term in C. It can easily be seen that the clauses C_{1}, …, C_{k} can be assumed to be non-redundant. A non-ground clause is called AC-redundant if all its ground instances are.

Remark. We emphasize that AC-redundancy is defined with respect to arbitrary interpretations, not just equality interpretations. In particular, there are restrictions on the use of the transitivity axiom. The restrictions are of more theoretical than practical significance, as all the usual simplification techniques can be formalized using AC-redundancy. Wertz (1992) uses a different notion of redundancy, where restrictions are imposed, not on transitivity, but instead on the use of the associativity and commutativity axioms.

For example, consider the (unit) clauses s[u′] ≈ t and u ≈ v, where u′ ↔_{AC}^{∗} uσ, for some substitution σ. If uσ ≻ vσ and either s ≻ uσ or else t ≻ vσ, then s[u′] ≈ t is AC-redundant with respect to any set N containing u ≈ v and s[vσ] ≈ t. In practice, this allows one to replace s[u′] ≈ t by s[vσ] ≈ t in the presence of the equation u ≈ v. In other words, the subterm u′ can be rewritten modulo AC to a smaller term vσ.

An AC-superposition inference in which both premises are ground instances of extended clauses with maximal terms t and t′, respectively, such that t ↔_{AC}^{∗} t′, is called AC-redundant with respect to N if its conclusion is either AC-redundant or is a member of N. Any other ground inference with conclusion B and maximal premise C is called AC-redundant with respect to N if there exist ground instances C_{1}, …, C_{k} of N, such that C ≻ C_{j}, for all j with 1 ≤ j ≤ k, and B is true in every model of AC ∪ RA ∪ F ∪ T_{≺s} ∪ {C_{1}, …, C_{k}}, where s is the maximal term in C. A non-ground inference is called AC-redundant if all its ground instances are AC-redundant. One way to render an inference in S_{AC}^{≻} redundant is to add its conclusion to the set N.

We say that a set of clauses N is saturated up to AC-redundancy if all inferences, the premises of which are non-redundant clauses in N or extensions of non-redundant clauses in N, are AC-redundant.

Let us conclude this section by pointing out that extended clauses are redundant, but inferences with them are not. Therefore it is possible to dispense with extended rules altogether, and instead encode inferences with them directly in an “extended” AC-superposition calculus, cf., Rusinowitch and Vigneron (1991).

4 Refutational Completeness

In this section we will show how to define an equality model for saturated clause sets that do not contain the empty clause. The definition of a suitable model uses induction on ≻ and is adapted from Bachmair and Ganzinger (1994). The presence of extended rules causes technical complications, though, and requires certain modifications in the model construction process.

Given a set N of ground clauses, we define a corresponding Herbrand interpretation I using induction on ≻. For every clause C in N we define R_{C} to be the set ⋃_{C≻D} E_{D}; and denote by I_{C} the set {u ≈ v : u and v ground, u ↓_{AC\R_{C}^{e}} v}, which we also call the AC-rewrite closure of R^{e}. Furthermore, if C is a clause C′ ∨ s ≈ t, where (s ≈ t) ≻ C′ and s ≻ t, then E_{C} = {s ≈ t} if (i) C is false in I_{C}, (ii) C′ is false in the AC-rewrite closure of (R_{C} ∪ {s ≈ t})^{e}, and (iii) the term s is irreducible by AC\R_{C}^{e}. In that case, we also say that C is productive and that it produces s ≈ t. In all other cases, E_{C} = ∅. Finally, let R be ⋃_{C} E_{C} and let I be the AC-rewrite closure of R^{e}.

The Herbrand interpretation I is intended to be an equality model of N ∪ AC, provided N is saturated and does not contain the empty clause. The following lemmas state the essential properties of the interpretations I and I_{C}.

Lemma 2 Let C be a ground clause (which need not be in N) and D be a clause in N with D ⪰ C. If ¬A is a negative literal in C with A ∉ I_{D}, then A ∉ I. As a consequence, if C is true in I_{D}, then it is also true in I and in any interpretation I_{D′} with D′ ∈ N and D′ ≻ D.

Proof. Let ¬A be a negative literal in C such that A ∉ I_{D}. If B ∈ I \ I_{D}, then B ≻ ¬A, and therefore A ∉ I. Also, if A is a positive atom in C and A ∈ I_{D}, then A is contained in any set I_{D′} with D′ ≻ D and in I. From this we may conclude that if C is true in I_{D}, then it is also true in I and in any interpretation I_{D′} with D′ ∈ N and D′ ≻ D. □

The next lemma follows immediately from the definition of the interpretations I_{C} and I.

Lemma 3 The interpretation I and all interpretations I_{C} are models of the associativity, commutativity, reflexivity, symmetry, and all congruence axioms.

We emphasize that transitivity need not be satisfied by all interpretations I_{C} or I, and consequently these interpretations need not be equality interpretations. However, if the clause set N is saturated, then “sufficiently many” instances of the transitivity axiom are true in each interpretation I_{C}, so that the final interpretation I does indeed satisfy transitivity, and hence is an equality interpretation. The following lemma is essential in this regard.

Lemma 4 The interpretation I_{C} is a model of T_{⪯t} (resp. T_{≺t}) if and only if for all ground terms u and v with u ↔_{AC∪R_{C}^{e}}^{⪯t} v (resp. u ↔_{AC∪R_{C}^{e}}^{≺t} v) we have u ↓_{AC\R_{C}^{e}} v.

Proof. First let us assume that we have u ↓_{AC\R_{C}^{e}} v for all ground terms u and v with u ↔_{AC∪R_{C}^{e}}^{⪯t} v. We show that I_{C} is a model of T_{⪯t}. Let u, v, and w be ground terms with t ⪰ u, t ⪰ v, and t ⪰ w. If u ≈ v and v ≈ w are true in I_{C}, then u ↓_{AC\R_{C}^{e}} v and v ↓_{AC\R_{C}^{e}} w. In other words, we have u ↔_{AC∪R_{C}^{e}}^{⪯t} w; hence u ↓_{AC\R_{C}^{e}} w and u ≈ w is true in I_{C}.

On the other hand, if I_{C} is a model of T_{⪯t}, then we have u ↓_{AC\R_{C}^{e}} w whenever u ←_{AC\R_{C}^{e}} v →_{AC\R_{C}^{e}} w, for some term v with t ⪰ v. Using Lemma 1, we may conclude that u′ ↓_{AC\R_{C}^{e}} v′ for all ground terms u′ and v′ with u′ ↔_{AC∪R_{C}^{e}}^{⪯t} v′. □

We now come to the main properties of the model construction.

Lemma 5 Let N be a set of clauses that is saturated up to AC-redundancy, does not contain the empty clause, but contains an extension of every non-redundant reductive clause in N. Let I be the interpretation constructed from the set of all ground instances of N ∪ RA. Then for every ground instance C of a clause in N ∪ RA we have:

(1) If s is the maximal term in C, then I_{C} is a model of T_{⪯s}.

(2) If C is an instance Ĉσ of a clause in N, such that xσ is reducible by AC\R_{C}^{e}, for some variable x in Ĉ, then C is true in I_{C}.

(3) If C is an instance of a clause with a selected literal, then it is true in I_{C}.

(4) If C is non-productive, then it is true in I_{C}.

(5) If C = C′ ∨ A produces A, then C is a non-redundant instance of a clause in N with no selected literals and C′ is false in I.

Proof. We use induction on ≻. Let C be a ground instance of N ∪ RA with maximal term s and assume (1)-(7) are already satisfied for all ground instances C′ of N with C ≻ C′.

(1) Since for every ground term t there is at least one clause with maximal term t (namely the ground instance t ≈ t of the reflexivity axiom), we may use the induction hypothesis to infer that I_{C} is a model of T_{≺s}. By Lemmas 1 and 4, it is therefore sufficient to prove that for any two ground instances f(u, u′) → f(u, u′′) and f(v, v′) → f(v, v′′) of extended rules in R_{C}^{e}, with s ↔_{AC}^{∗} f(u, u′) ↔_{AC}^{∗} f(v, v′), we have f(u, u′′) ↓_{AC\R_{C}^{e}} f(v, v′′).

Suppose u′ ≈ u′′ is produced by C′ ∨u′ ≈ u′′ and v′ ≈ v′′ is produced by D′ ∨v′ ≈ v′′. Both clauses are strictly smaller than C, so that by the induction hypothesis, they are true in I_{C}, whereas C′ and D′ are false in I. By AC-superposition we obtain the clause C′′ = C′ ∨ D′ ∨ f(u, u′′) ≈ f(v, v′′). Since this inference can be AC-lifted, we may use saturation up to AC-redundancy, to infer that either C′′ is a ground instance of N or else there exist ground instances C_{1}, …, C_{k} of N, such that C′′ ≻ C_{j}, for all j with 1 ≤ j ≤ k, and C′′ is true in every model of AC ∪ RA ∪ F ∪ T_{⪯t} ∪ {C_{1}, …, C_{k}}, where t is the maximal term in C′′. Since C ≻ C′′ and s ≻ t, we may use the induction hypothesis to infer that C′′ is true in I_{C}, if it is a ground instance of N, and that I_{C′′} is a model of AC ∪ RA ∪ F ∪ T_{⪯t} ∪ {C_{1}, …, C_{k}}, otherwise. In either case, we may conclude that C′′ is true in I_{C}, which implies that f(u, u′′) ≈ f(v, v′′) is true in I_{C}, and thus f(u, u′′) ↓_{AC\R_{C}^{e}} f(v, v′′). (The importance of part (1) rests in the fact that it allows us to apply AC-redundancy.)

(2) Suppose C = Ĉσ is a ground instance of N, such that xσ is reducible by AC\R_{C}^{e}, say xσ →_{AC\R_{C}^{e}} u. Let σ′ be the same substitution as σ, except that xσ′ = u, and let C′ be the clause Ĉσ′. Since C ≻ C′, we may use the induction hypothesis and Lemma 2 to infer that C′ is true in I_{C}. Furthermore, since xσ ≈ u is true in I_{C}, a literal Lσ in C is true in I_{C} if and only if the corresponding literal Lσ′ in C′ is true in I_{C}. This implies that C is true in I_{C}.

If C is an instance Ĉσ, where xσ is irreducible for all variables x in Ĉ, then any inference with maximal premise C can be AC-lifted. We call C an AC-reduced ground instance of N in that case.

(3) Let C = C′ ∨ s ≉ t be an AC-reduced ground instance of a clause in which the literal corresponding to s ≉ t is selected. The assertion is obviously true if s ≈ t is false in I_{C}. So let us assume s ↓_{AC\R_{C}^{e}} t.

(3.1) If s ↔_{AC}^{∗} t, then C′ is a reflective AC-resolvent of C. Resolution inferences can be lifted, so that we may use saturation up to AC-redundancy, to infer that C′ is true in I_{C}.

(3.2) If s and t are not AC-equivalent, then we have either s ≻ t or t ≻ s. We discuss only one case, as the other is similar. Suppose s ≻ t, in which case s is reducible by AC\R_{C}^{e} and can be written as s[u′], where u′ ↔_{AC}^{∗} u, for some clause D = D′ ∨ u ≈ v with maximal literal u ≈ v, and s[v] ↓_{AC\R_{C}^{e}} t. The clause D is either productive or else is a ground instance of an extension of a productive clause. Since C ≻ D, we use the induction hypothesis to infer that D′ is false in I. Also, if D is productive, it is non-redundant and hence must be a ground instance of a clause with no selected literals. The clause C′′ = C′ ∨ D′ ∨ s[v] ≉ t can be obtained from C and D by negative AC-superposition. By saturation up to redundancy, C′′ must be true in I_{C}. Since D′ and s[v] ≈ t are false in I_{C}, we may infer that C′, and thus C, is true in I_{C}.

(4) Suppose C is false in I_{C} but non-productive. That is, C violates one of the other two conditions imposed on productive clauses.

(4.1) If condition (ii) is violated, then C is of the form C′ ∨ s ≈ t ∨ s′ ≈ t′, where s ≈ t is a maximal literal, s ≻ t ≻ t′, s ↔_{AC}^{∗} s′, and t ↓_{AC\R_{C}^{e}} t′. We obtain the clause C′′ = C′ ∨ t ≉ t′ ∨ s′ ≈ t′ from C by AC-factoring. Using saturation up to redundancy, we may infer that C′′ is true in I_{C}. Since t ≈ t′ is true in I_{C}, this implies that C′∨s′ ≈ t′, and therefore C, is true in I_{C}, which is a contradiction.

(4.2) Otherwise, C must be a clause C′ ∨ s ≈ t with maximal literal s ≈ t, where s ≻ t and s is reducible by AC\R_{C}^{e}. Then there exists a clause D = D′ ∨ u ≈ v with maximal literal u ≈ v, such that s can be written as s[u′] and u′ ↔_{AC}^{∗} u. Moreover, D is either productive or is a ground instance of an extension of a productive clause. By the induction hypothesis, the clause D′ is false in I and if D is productive it is a non-redundant instance of a clause with no selected literals. Thus, we may obtain from C and D by AC-superposition the clause C′′ = C′ ∨ D′ ∨ s[v] ≈ t, which by saturation has to be true in I_{C}. Since D′ is false in I_{C}, either C′ or s[v] ≈ t must be true in I_{C}. If C′ is true in I_{C}, so is C. If s[v] ↓_{AC\R_{C}^{e}} t, then we have s = s[u′] →_{AC\R_{C}^{e}} s[v] ↓_{AC\R_{C}^{e}} t, which indicates that s ≈ t, and hence C, is true in I_{C}—a contradiction.

(5) A productive clause C = C′ ∨ A is false in I_{C}, hence is non-redundant and, by part (3), cannot be an instance of a clause with selected literals. The definition of productive clauses also ensures that C′ is false in the AC-rewrite closure of (R_{C} ∪ E_{C})^{e}, and hence false in I. □

The lemma indicates that under the given assumptions I is an equality model of AC ∪N. (Any non-productive ground instance C of N is true in I_{C}, while non-productive ground instances C are true in the AC-rewrite closure of (R_{C} ∪E_{C})^{e}. Furthermore, I is a model of T_{⪯t}, for all ground terms t; and hence is a model of T.)

The proof of the lemma also shows that certain inferences with extended clauses are unnecessary. For instance, AC-superpositions on a proper subterm of an extended clause, i.e., inferences of the form

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

where σ is a most general AC-unifier of s and s′, and the second premise extends the clause D ∨ u[s′] ≈ v, are not needed.

As an immediate corollary of the above lemmas we obtain:

Theorem 1 Let N be a set of clauses that is saturated up to AC-redundancy with respect to the associative-commutative superposition calculus S_{AC}^{≻}. Furthermore, suppose N contains an extension of every non-redundant reductive clause in N. Then N ∪ AC is equality unsatisfiable if and only if it contains the empty clause.

Proof. If N ∪ AC contains the empty clause it is unsatisfiable. If N ∪ AC does not contain the empty clause, let I be the interpretation constructed from the set of all ground instances of N ∪ RA. By Lemmas 3 and 5, I is an equality model of N ∪ AC. □

This theorem shows that associative-commutative superposition calculi provide a basis for refutationally complete theorem provers. Such a theorem prover has to saturate a given set of input clauses up to AC-redundancy. The empty clause will be generated if the input set, plus AC, is equality unsatisfiable. Saturation of clause sets can be achieved by fair application of inference rules. These aspects of the saturation process have been discussed elsewhere, e.g., Bachmair and Ganzinger (1994) or Bachmair, Ganzinger and Waldmann (1992), and apply directly to the present case.

5 Summary

We have presented an associative-commutative superposition calculus and proved its refutational completeness. We have tried to keep the exposition clear and simple, and therefore have not discussed various possible improvements to the calculus, most of which can be derived from redundancy. Some are relatively minor, such as the redundancy of certain inferences involving an extended clause, while others are more important, e.g., the use of redex orderings to achieve a similar effect as critical pair criteria. The main difference of our calculus with other associative-commutative paramodulation calculi is that the associativity and commutativity axioms, but not all instances of the transitivity axiom, are built into our notion of redundancy; whereas other researchers have opted for transitivity and compromised on associativity and commutativity (e.g., Wertz 1992). From a more practical perspective our approach is preferrable, as enough instances of transitivity are provided to cover full associative-commutative rewriting, while otherwise associative-commutative rewriting actually needs to be restricted. In addition, our completeness proof is considerably simpler than previous proofs.

We believe that the approach we have outlined for associativity and commutativity can be applied to other equational theories, such associativity and commutativity with identity (Baird, Peterson and Wilkerson 1989, Jouannaud and Marché 1992); for some work in this direction see Wertz (1992). There is also ongoing work on combining associative-commutative calculi with the basic strategy, and results have been announced by Vigneron (1993) and by Nieuwenhuis and Rubio (1993).

References

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

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

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

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

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

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

Timothy Baird, Gerald Peterson and Ralph Wilkerson, 1989. Complete sets of reductions modulo associativity, commutativity and identity. In Proc. 3rd Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 355, pp. 29–44, Berlin, Springer-Verlag.

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

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

Jieh Hsiang and Michael Rusinowitch, 1987. On Word Problems in Equational Theories. In Proc. 14th ICALP, Lecture Notes in Computer Science, vol. 267, pp. 54–71, Berlin, Springer-Verlag.

Jean-Pierre Jouannaud and Claude Marché, 1992. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, Vol. 104, pp. 29–51.

Paliath Narendran and Michaël Rusinowitch, 1991. Any Ground Associative-Commutative Theory has a Finite Canonical System. In Ronald V. Book, editor, Proc. 4th Rewriting Techniques and Applications 91, Como, Italy, Springer-Verlag.

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

R. Nieuwenhuis and A. Rubio, 1993. AC-superposition with constraints: No AC-unifers needed. Submitted, 1993.

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

E. Paul, 1992. A general refutational completeness result for an inference procedure based on associative-commutative unification. Journal of Symbolic Computation, Vol. 14, pp. 577–618.

G. Peterson and M. Stickel, 1981. Complete sets of reductions for some equational theories. Journal of the ACM, Vol. 28, pp. 233–264.

A. Rubio and R. Nieuwenhuis, 1993. A precedence-based total AC-compatible ordering. In Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 374–388, Berlin, Springer-Verlag.

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

M. Rusinowitch and L. Vigneron, 1991. Automated deduction with associativecommutative operators. In Proc. Int. Workshop on Fundamentals of Artificial Intelligence Research, Lecture Notes in Artificial Intelligence, vol. 535, pp. 185–199, Berlin, Springer-Verlag.

L. Vigneron, 1993. Associative-commutative dedution with constraints. Technical Report 93-R-196, CRIN, Nancy.

U. Wertz, 1992. First-Order Theorem Proving Modulo Equations. Technical Report MPI-I-92-216, Max-Planck-Institut für Informatik, Saarbrücken.

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