MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Theorem Proving in Cancellative Abelian Monoids

Harald Ganzinger Uwe Waldmann

MPI–I–96–2–001 January 1996

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

Im Stadtwald D 66123 Saarbrücken

Germany Authors’ Addresses

Max-Planck-Institut für Informatik Im Stadtwald 66123 Saarbrücken Germany

E-Mail: {hg,uwe}@mpi-sb.mpg.de

Phone: +49 681 302 {5361,5431}

Publication Notes

An extended abstract of this report has been submitted.

Acknowledgements

The research described in this paper was supported in part by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics). We wish to thank Leo Bachmair, Deepak Kapur, David Plaisted, Georg Struth, and Jürgen Stuber for helpful discussions on the subject of this paper.

Abstract

We describe a refined superposition calculus for cancellative abelian monoids. They encompass not only abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Both the AC axioms and the cancellation law are difficult for a general purpose superposition theorem prover, as they create many variants of clauses which contain sums. Our calculus requires neither explicit inferences with the theory clauses for cancellative abelian monoids nor extended equations or clauses. Improved ordering constraints allow us to restrict to inferences that involve the maximal term of the maximal sum in the maximal literal. Furthermore, the search space is reduced drastically by certain variable elimination techniques.

Keywords

Automated Theorem Proving, First-Order Logic, Superposition, Cancellative Abelian Monoids, Associativity, Commutativity, Variable Elimination, Term Rewriting.

1 Introduction

To be useful in applications such as program verification and synthesis, a theorem prover must combine mathematical with meta-mathematical reasoning. Theories from which program properties are to be derived are divided into parts that specify standard mathematical structures, including numbers, lists, multisets, graphs, and into other parts that provide the axioms for additional free function and predicate symbols. The latter describe, in a more or less ad hoc manner, objects, and their properties, of the particular domain of application for which a program is to be written.

There are several distinct lines of investigation along which previous attempts have been made for attacking this problem. In hierarchic situations where free function symbols either do not exist or where they are defined in a “sufficiently complete” manner on top of the primitive structures, mathematical knowledge can be incorporated by using decision procedures and constraint solvers as black boxes. This is the case, for instance, in constraint logic programming, in resolution theorem proving with theory unification [10, 11], or in theorem proving with constraints [19]. The case of sufficient-completely defined free functions has been investigated e.g. by Bachmair, Ganzinger, and Waldmann [6]; Avenhaus and Becker [1] have described a related order-sorted approach.

In an algebraic context, however, sufficient completeness practically excludes uninterpreted function symbols. The situation is similar when one considers, for instance, theorem provers based on extensions of Presburger arithmetic. As they lack the possibility to handle existential quantification, they are suited for verification (where instantiations are known), but not for proof discovery and program synthesis (Hines [16]). Furthermore, experiments by Boyer and Moore [9] show that mathematical routines rarely have a chance to contribute to a proof, unless they are very tightly interwoven with the rest of the prover. Heuristic approaches that involve such a more sophisticated combination of modules, e.g., in the Boyer-Moore prover or in the PVS-system [22], have proven to be very useful in practice.

Our own line of research is based on the integrating approach, where the inference rules are adapted to the theory in a specific way. Equality is the prime example for this technique: In paramodulation and superposition, there are no resolution inferences with the transitivity or symmetry axioms. Rather, the equality axioms are coded as inference rules, which can be subject to specific ordering restrictions. Other transitive relations, in particular orderings, can be handled by related rewriting techniques yielding chaining calculi as they have been investigated by Bledsoe, Kunen, and Shostak [8], Hines [15], and Bachmair and Ganzinger [3], among others. The laws of associativity and commutativity of binary functions have previously been integrated into paramodulation calculi: Extended clauses and unification modulo AC make explicit inferences with the AC axioms unnecessary (see Peterson and Stickel [23] for the case of unit equations, and Wertz [29] and Bachmair and Ganzinger [2], for the clausal case). Unfortunately, AC-unification is doubly exponential, and it shows in practice. By using constraints, AC-unification can be replaced by the “only” simply exponential problem of AC-unifiability, as described by Nieuwenhuis and Rubio [21], and Vigneron [28]. On the other hand, (some) equality constraints need to be solved for simplification. One of the results of the present paper is that there are other ways to avoid especially prolific cases of AC-unification in the presence of more algebraic structure.

The present paper describes a refined superposition calculus for cancellative abelian monoids. They encompass not only abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Like the AC axioms, the cancellation law is difficult for a general purpose superposition theorem prover, as it creates many variants of clauses which contain sums. The main highlights of our calculus are the following. (i) There is no need for explicit inferences with the theory clauses for cancellative abelian monoids. Hence, there is no generation and recombination of different variants of one and the same clause. (ii) There is no need for extended equations or clauses. By virtue of this fact, many especially prolific instances of AC-unification are avoided. In fact, AC-unification can be replaced by ACU-unification. (iii) The ordering constraints for superposition can be further refined. As in previous calculi one may ignore non-maximal literals, as well as the smaller side of an equation for chaining. Here, in addition, only the maximal term of a (maximal) sum can participate in an inference. (iv) The general notion of redundancy as it was introduced by Bachmair and Ganzinger in [4] can be appropriately refined. It forms the basis for developing specific forms of the usual simplification techniques. Simplification is an indispensable component of any saturation-based theorem prover. In this paper, redundancy will in particular allow to show admissibility of certain variable elimination techniques.

A crucial indication of the practicality of any approach for integrating mathematical theories by specifically refined forms of resolution and paramodulation or chaining is the extent to which they avoid a certain especially prolific form of inference. It is the type of inference in which the main term in one of the premises is a variable, and, hence, unification is no longer an effective filter. For the equational case it is known that paramodulation into or below variables is not needed. For dense, total orderings without endpoints similar results have been obtained in [3, 8, 15, 24]. In the calculus to be described below, inferences are computed with maximal terms in sums. The sum itself, obviously, is not a variable, but the term may be one. The fact that certain inferences involving such variables cannot be avoided is an indication for why non-refined superposition strategies can perform badly for monoids with cancellation. In our refined calculus, only unshielded variables, i.e., variables that do not occur somewhere else as arguments of free function symbols, pose a problem in this regard. That leaves us with the problem of how to deal with unshielded variables. Fortunately unshielded variables can be eliminated in many, though not all cases without affecting refutational completeness.

With these characteristics, the present approach is a considerable improvement over Hsiang, Rusinowitch, and Sakai’s extension of ordered paramodulation [17, 26] to handle cancellation laws. Our approach is related to normalized rewriting modulo the group axioms (Marché [20]) and superposition for integer modules (Stuber [27]). Both handle only the stronger case of groups. As will become apparent, working in “non-groups” makes some aspects of equational theorem proving significantly more difficult while others are simplified. For instance, there will sometimes be a need for abstraction^{1}; in other situations, the number of overlaps is reduced, and in non-groups it may be easier to eliminate positive occurrences of unshielded variables.

2 Algebraic Foundations

An abelian semigroup is an algebraic structure consisting of a non-empty set G and a binary relation + that satisfies the associativity axiom and the commutativity axiom

\begin{aligned}(A) & ∀x, y, z: & x + (y + z) & = (x + y) + z \\ (C) & ∀x, y: & x + y & = y + x. \end{aligned}

An abelian monoid is an abelian semigroup (G, +) with a constant 0 ∈ G such that the identity axiom holds:

(U)  ∀x:  x + 0 = x.

An abelian semigroup (G, +) or monoid (G, +, 0) is called cancellative, if it satisfies additionally the cancellation axiom

(K)  ∀x, y, z:  x + z = y + z ⇒ x = y,

or in other words, if the difference between two elements is uniquely defined whenever it exists. A cancellative abelian semigroup or monoid is an abelian group if and only if difference is a total function. Typical examples of cancellative abelian monoids where difference is partial are the natural numbers under addition, the non-zero integers under multiplication, and multisets under union.

1This would not even be possible in the purely equational framework of [20].

We denote the set of the axioms (A), (C), (U), and (K) by ACUK, and the respective subsets by AC, ACU, and ACK. For m ∈ N^{+}, ∑_{i∈{1,...,m}} x_{i} is an abbreviation for the sum x_{1} + ⋯ + x_{m} and mx is an abbreviation for the m-fold sum x + ⋯ + x. In a monoid, ∑_{i∈∅} x_{i} and 0x are defined as 0.

Lemma 2.1 Let (G, +) be a cancellative abelian semigroup and let b, c ∈ G. If b + c = b, then G is a monoid and c is its unique identity element.

Proof. For every x ∈ G, x + b + c = x + b, hence by cancellation x + c = x. If furthermore b′ + c′ = b′ for some b′, c′ ∈ G, then b′ + c′ = b′ = b′ + c, hence by cancellation c′ = c. □

It is a well-known result that every finite cancellative abelian semigroup is a group. The following lemma generalizes this fact.

Lemma 2.2 Let (G, +) be a cancellative abelian semigroup and I be a finite non-empty set of indices. For all i ∈ I, let a_{i} ∈ G and let f_{i} be a function from G to G. If

⋁_{i∈I} x + f_{i}(x) = a_{i}

holds for every x ∈ G, then G is a group.

Proof. Let b = ∑_{j∈I} 2a_{j}, then

⋁_{i∈I} ∑_{j∈I} 2a_{j} + f_{i}(b) = a_{i} .

Pick any k ∈ I such that

∑_{j∈I} 2a_{j} + f_{k}(b) = a_{k}

and let K = I \ {k}. By Lemma 2.1, ∑_{j∈K} 2a_{j} + a_{k} + f_{k}(b) is an identity element of G. We denote it by 0.

∑_{j∈K} 2a_{j} + a_{k} + f_{k}(b) = 0

As every a_{i} occurs at least once in this sum, every a_{i} has an inverse, namely the remainder of the sum. Let us denote the inverse of a_{i} by a′_{i}, then for every x ∈ G

⋁_{i∈I} x + f_{i}(x) + a′_{i} = 0 .

Thus for every x ∈ G there is an i ∈ I such that f_{i}(x) + a′_{i} is the inverse of x. As every x has an inverse, G is a group. □

3 The Cancellative Superposition Calculus

3.1 Preliminaries

We will develop our calculus in the framework of equational clauses. An equation e is an unordered pair {t, t′}, usually written as t ≈ t′. A literal is either an equation e (also called a positive literal) or a negated equation ¬ e (also called a negative literal). The symbol [¬] e denotes either of these. Instead of ¬ t ≈ t′, we sometimes write t ≉ t′. A clause is a finite multiset of literals. Terms are formed over a many-sorted signature (without subsorts or overloading), so every variable x comes with a unique declaration x: S and every function symbol with a unique declaration f : S_{1} … S_{n} → S (for n ∈ N). In particular, 0 and + have the declarations 0 : → S_{CAM} and + : S_{CAM}S_{CAM} → S_{CAM}.^{2} We consider only well-formed terms and equations and assume that every sort is inhabited, i.e., that for every sort there exists at least one ground term. Predicates p different from ≈ are coded using function symbols p′, so the literal [¬] p(t) is represented by the equation [¬] p′(t) ≈ true. We assume that the reader is familiar with standard concepts and notations in the area of rewriting (to be found for instance in the survey of Dershowitz and Jouannaud [12]), and in the area of superposition-based theorem proving (see Bachmair and Ganzinger [4]).

The symbol =_{ACU} denotes the congruence generated by ACU. The ACUcongruence class of a term t is [t]_{ACU} = { t′ | t =_{ACU} t′ }.

Definition 3.1 A function symbol that is different from 0 and + is called a free function symbol. A term is called atomic, if it is not a variable and its top symbol is different from +. A term t is called a proper sum, if t = t_{1} + t_{2} and t_{1} ≠_{ACU} 0, t_{2} ≠_{ACU} 0.

The set of all terms is the disjoint union of the three sets { t | ∃x: x is a variable, t =_{ACU} x }, { t | ∃s: s is atomic, t =_{ACU} s }, and { t | ∃s: s is a proper sum, t =_{ACU} s }. We can therefore extend the terminology above to ACU-congruence classes, and say that [t]_{ACU} is a variable (an atomic term, a proper sum), if there is some s ∈ [t]_{ACU} with this property.

2There is no scalar multiplication in our signature, so mt is merely an abbreviation for t + ⋯ + t.

We say that a term t occurs in s at the top, if there is a position o ∈ Pos(s) such that s|_{o} = t and for every proper prefix o′ of o, s(o′) equals +. We say that t occurs in s below a free function symbol, if there is a position o ∈ Pos(s) such that s|_{o} = t and s(o′) is a free function symbol for some proper prefix o′ of o. We extend this terminology to ACU-congruence classes, and say that [t]_{ACU} occurs in [s]_{ACU} at the top (below a free function symbol), if there are some t′ ∈ [t]_{ACU} and s′ ∈ [s]_{ACU} with this property. For instance, [2a]_{ACU} and [a + f(a + b)]_{ACU} occur at the top of [3a + 2f(a + b)]_{ACU}, [a]_{ACU} occurs both at the top and below a free function symbol.

Definition 3.2 A reduction ordering ≻ is called ACU-compatible, if s′ =_{ACU} s ≻ t =_{ACU} t′ implies s′ ≻ t′.

Every ACU-compatible reduction ordering extends naturally to a reduction ordering on ACU-congruence classes.

For ground terms, we can obtain an ACU-compatible reduction ordering ≻ from an arbitrary AC-compatible ordering ≻_{1} by defining s ≻ t if s↓ ≻_{1} t↓, where s↓ denotes the normal form of s under rewriting with the rule x + 0 → x. We can lift this ordering to non-ground terms by defining s ≻ t if sθ ≻ tθ for all ground instances sθ and tθ. However, as shown by Jouannaud and Marché [18], it happens quite frequently that ≻ orders a pair of terms in an operationally undesirable way, or that s[x] and t[x] are uncomparable because s[0] ≻ t[0] but s[u] ≺ t[u] for all non-zero ground terms u.^{3} This is a serious problem, if one is interested in classical rewriting. It is not a hindrance, though, for calculi like superposition or unfailing completion, which are preferably implemented using constraints. (In fact, Jouannaud and Marché’s method can be considered as a variant of unfailing completion with constraints.)

Definition 3.3 We say that an ACU-compatible ordering has the multiset property, if whenever a ground atomic term u is greater than v_{i} for every i in a finite index set I ≠ ∅, then u ≻ ∑_{i∈I} v_{i}.

From now on, ≻ will always denote an ACU-compatible ordering that has the multiset property and is total on ACU-congruence classes.^{4} Examples of orderings with these properties are obtained from the associative path ordering (Bachmair and Plaisted [7]) or the ordering of Rubio and Nieuwenhuis [25] with precedence f_{n} ≻ … ≻ f_{1} ≻ + ≻ 0 by comparing s↓ and t↓ as described above.

3Jouannaud and Marché’s statement that “AC1-rewrite orderings cannot really exist” [18] should be taken with a grain of salt, however.

4In practice, it is sufficient if the ordering can be extended to a total ordering.

A ground literal e is called true in a set E of ground equations, if e ∈ E. A ground literal ¬ e is called true in E, if e ∉ E. A ground clause is called true in E, if at least one of its literals is true in E. If a ground literal or clause is not true in E, it is called false in E.

A set E of ground equations is called a model of a clause C, if every ground instance Cθ of C is true in E; it is called a model of a set N of clauses, if it is a model of every C ∈ N. If N and N′ are sets of clauses, we write N ⊧ N′ if every model of N, ACUK, and the equality axioms is a model of N′. In other words, ⊧ denotes entailment modulo ACUK. If C is a clause, N ⊧ C is a shorthand for N ⊧ {C}.

Convention 3.4 For the remainder of this paper, we will work only with ACU-congruence classes, rather than with terms. To simplify notation, we will omit the [ ]_{ACU} and drop the subscript of =_{ACU}. So all terms, equations, substitutions, inference rules, etc., are to be taken modulo ACU, that is, as representatives of their congruence classes.

The ordering restrictions that we use are more refined than usual, in that they are based primarily on maximal terms in sums.

Definition 3.5 Let e be a ground equation, then the maximal atomic term of e (with or without multiplicity) is defined in the following way:

• If e is an equation of the form nu + ∑_{i∈I} s_{i} ≈ mu + ∑_{j∈J} t_{j}, where u, s_{i}, and t_{j} are atomic terms, n ≥ m ≥ 0, n ≥ 1, and u ≻ s_{i} and u ≻ t_{j} for all i ∈ I, j ∈ J, then mt(e) = u and mt_{#}(e) = nu.

• If e is an equation of the form u ≈ v, where u doesn’t have sort S_{CAM} and u ⪰ v, then mt(e) = mt_{#}(e) = u.

Definition 3.6 The symbol ms(t) denotes the multiset of all non-zero atomic terms occurring at the top of a ground term t, i.e.,

• ms(t) = { v_{j} | j ∈ J }, if t = ∑_{j∈J} v_{j} and all v_{j} are non-zero atomic terms. (In particular ms(0) = ∅, as J may be empty.)

• ms(t) = {t}, if t doesn’t have sort S_{CAM}.

If e is a ground equation t ≈ t′, then ms(e) is the multiset union of ms(t) and ms(t′).

Definition 3.7 The ordering ≻_{x} on ground terms is defined as follows: s ≻_{x} t if there is an s′ ∈ ms(s) such that s′ ≻ t′ for all t′ ∈ ms(t). For arbitrary terms, s ≻_{x} t if sθ ≻_{x} tθ for all ground instances sθ and tθ.

Definition 3.8 The ordering ≻ on terms is extended to an ordering ≻_{L} on literals as follows: Every ground literal [¬] s ≈ t is mapped to the quadruple

(mt_{#}(s ≈ t), pol, ms(s ≈ t), {s, t}),

where pol is 1 for negative literals and 0 for positive ones. Two ground literals are compared by comparing their associated quadruples using the lexicographic combination of the ordering ≻ on terms, the ordering > on N, the multiset extension of ≻ and the multiset extension of ≻. The ordering is lifted to possibly non-ground literals in the usual way, so [¬] e_{1} ≻_{L} [¬] e_{2} if and only if [¬] e_{1}θ ≻_{L} [¬] e_{2}θ for all ground instances [¬] e_{1}θ and [¬] e_{2}θ. In order to use the ordering ≻_{L} to compare equations, the latter are identified with positive literals.

The ordering ≻_{C} on clauses is the multiset extension of the literal ordering ≻_{L}.

As ≻_{L} and ≻_{C} are obtained from noetherian orderings by multiset extension and lexicographic combination, they are noetherian, too.

Definition 3.9 A substitution σ is called t-preserving, if tσ = t.

Any ACU-unification algorithm (e.g., Herold and Siekmann [14]) can be used to compute complete sets of t-preserving ACU-unifiers by simply taking all variables in t as constants.

We need the concept of t-preservation when we deal with variables that are known to correspond to atomic terms on the ground level. Consider the two terms s_{1} = 2x and s_{2} = 2y + z. There are unifiers of s_{1} and s_{2}, e.g., {x ↦ y′ + z′, y ↦ y′, z ↦ 2z′}. There is no unifier, though, that maps z to a non-zero atomic ground term. Neither does a z-preserving unifier of s_{1} and s_{2} exist.

Lemma 3.10 Let s_{1} = ∑_{i∈I} m_{i}x_{i} + m′u and s_{2} = ∑_{j∈J} n_{j}y_{j} + n′u, where the x_{i} and y_{j} are pairwise distinct variables, u is either atomic or a variable, and none of the x_{i} and y_{j} occurs in u. Let U be a complete set of u-preserving ACU-unifiers of s_{1} and s_{2}. Suppose that θ is an ACU-unifier of s_{1} and s_{2} and that uθ is a non-zero atomic ground term. Then θ = σρ for some σ ∈ U and some substitution ρ.

Proof. Let U′ be a complete set of ACU-unifiers of s_{1} and s_{2}, and let σ′ ∈ U′ such that θ = σ′ρ′.

If u is atomic, we may assume without loss of generality that σ′ maps all variables in u to fresh variables. So there is a variable renaming τ such that σ′τ is a u-preserving ACU-unifier of s_{1} and s_{2}. Hence σ′τ = στ′ for some σ ∈ U, and θ = στ′τ^{−1}ρ′.

If u is a variable, we may assume without loss of generality that uσ′ = ∑_{k∈K} μ_{k}z_{k} for μ_{k} ∈ N^{+} and fresh variables z_{k}. As uθ = uσ′ρ′ is a non-zero atomic ground term, K = {k_{0}} ∪ K′, where z_{k}ρ′ = 0 for k ∈ K′ and μ_{k_{0}} = 1. Let ρ′′ be the substitution that maps z_{k} to 0 for every k ∈ K′ and let τ be the variable renaming {z_{k_{0}} ↦ u}. Then θ = σ′ρ′ = σ′ρ′′ττ^{−1}ρ′. As σ′ρ′′τ is a u-preserving ACU-unifier of s_{1} and s_{2}, we have σ′ρ′′τ = στ′ for some σ ∈ U. Thus θ = στ′τ^{−1}ρ′. □

Definition 3.11 Let x be a variable occurring in some literal or clause. We say that x is shielded in the literal or clause, if it occurs at least once below a free function symbol. Otherwise, x is called unshielded.

For example, the variables x and z are shielded in x + y + f(x) ≈ g(z), whereas y is unshielded.

We assume to be given a selection function that assigns to every clause a (possibly empty) subset of its negative literals.

Definition 3.12 A variable x that occurs in a literal [¬] e of a clause C is called eligible, if either C has no selected literals and x is unshielded in C, or ¬ e is a selected literal of C and x is unshielded in ¬ e.

The importance of unshielded variables stems from the fact that they may correspond to maximal atomic subterms in a ground instance. If a variable x is shielded in a clause (or selected literal), then the clause or literal contains an atomic subterm t[x]. As xθ ≺ (t[x])θ, an atomic subterm of xθ cannot be maximal.

3.2 The Ideas

We will describe a refutationally complete theorem proving method for firstorder theories that include the axioms of cancellative abelian monoids. As the precise rules, to be given in section 3.3, turn out to be rather complex, we will start with a somewhat informal step-by-step presentation of the essential ideas.

The Superposition Calculus The superposition calculus of Bachmair and Ganzinger [4] is a refutationally complete theorem proving method for arbitrary first-order clauses with equality. Starting from an initial set of formulae, a superposition-based theorem prover computes inferences, e.g.,

\frac{D ∨ s ≈ s′  C ∨ [¬] t[u] ≈ t′}{(D ∨ C ∨ [¬] t[s′] ≈ t′)σ}  σ = mgu(s, u)

and adds their conclusions to the set of formulae. If the initial set is inconsistent, then every fair derivation will eventually produce a contradiction (i.e., the empty clause). The inference rules are restricted forms of paramodulation, resolution, and factoring. For instance, it is sufficient to perform only those superposition inferences that involve maximal literals and maximal sides of equalities. Besides, a global redundancy criterion allows to discard certain inferences and formulae. More precisely, a formula is redundant in a set of formulae N and may be deleted, if it is entailed by smaller clauses in N. An inference is redundant in N (and may be omitted in a fair derivation), if its conclusion follows from clauses in N that are smaller than the largest premise.

Our goal is to develop a refined and otherwise similar calculus for cancellative abelian monoids that makes superpositions with the ACUK axioms superfluous.

Cancellative Superposition Let us first restrict to the case that + is the only non-constant function symbol. In a cancellative abelian monoid, the congruence law and the cancellation law are in a certain sense complementary. The congruence law states that adding equal terms on both sides of an equation preserves truth, and conversely, that dropping equal terms on both sides of an equation preserves falsity. The cancellation law states that dropping equal terms on both sides of an equation preserves truth, and that adding equal terms on both sides of an equation preserves falsity. Hence, if we have an equation u + s ≈ s′ where the atomic term u is larger than s and s′, then we can infer s′ + u + t ≈ u + s + t′ from u + t ≈ t′ by congruence, and s′ + t ≈ s + t′ by cancellation. Similarly, we can infer s′ + u + t ≉ u + s + t′ from u + t ≉ t′ by cancellation, and s′ + t ≉ s + t′ by congruence. Intuitively, this means that rather than replacing the left hand side of a rewrite rule by the right hand side, we replace the maximal atomic part by the remainder: We rewrite u to s′ while adding s to the other side of the (possibly negated) equation. This is the essential reason why extended rules are unnecessary in our calculus.

The method can be generalized to equational clauses. Taking into account that u might occur more than once in a sum we get the (ground) inference rule

Cancellative Superposition \frac{D ∨ mu + s ≈ s′ C ∨ [¬] nu + t ≈ t′}{D ∨ C ∨ [¬] (n−m)u + t + s′ ≈ t′ + s}

where n ≥ m ≥ 1.^{5}

Together with the cancellation, equality resolution, and cancellative equality factoring rules, this rule is refutationally complete for sets of ground clauses, provided that + is the only non-constant function symbol.

Cancellation \frac{D ∨ [¬] nu + t ≈ mu + s}{D ∨ [¬] (n−m)u + t ≈ s}

\underline{Equality Resolution}^{6}  \frac{C ∨ ¬ 0 ≈ 0}{C}

Cancellative Eq. Factoring \frac{D ∨ nu + s ≈ s′ ∨ nu + t ≈ t′}{D ∨ ¬ s + t′ ≈ s′ + t ∨ nu + t ≈ t′}

The inference system remains refutationally complete if we add ordering restrictions, such that inferences are computed only if the literals involved are maximal (or selected) in their clauses and u is atomic and strictly larger than s, s′, t, and t′.

Example 3.13 Suppose that the ordering on constant symbols is given by b ≻ b′ ≻ c ≻ d ≻ d′. We will show that the following four clauses are contradictory with respect to ACUK. (The maximal part(s) of every clause are underlined.)

\underline{2b} + c ≈ d  (1)
\underline{b′} + c ≈ d′  (2)
\underline{d} ≈ d′  (3)
\underline{2b} ≉ b′  (4)

Cancellative superposition of (1) and (4) yields

d ≉ \underline{b′} + c  (5)

Cancellative superposition of (2) and (5) yields

d + \underline{c} ≉ d′ + \underline{c}  (6)

5Recall that we are working with terms modulo ACU. In particular, this implies that s and t may be missing (i.e., zero).

6As the cancellation rule transforms C ∨ ¬ s ≈ s into C ∨ ¬ 0 ≈ 0, it suffices to handle only the latter by equality resolution.

By cancellation of (6) we obtain

\underline{d} ≉ d′  (7)

Cancellative superposition of (3) and (7) produces

\underline{d′} ≉ \underline{d′}  (8)

which by cancellation and equality resolution yields the empty clause.

Speaking in terms of AG-normalized completion (Marché [20]), we can work directly with the symmetrisation; Marché’s Ψ_{AG} and Θ_{AG} have no counterpart in our framework. Consequently, the number of overlaps that have to be considered is reduced. On the other hand, we lack an inverse, which will lead to certain problems once free function symbols are introduced.

The Non-Ground Case Lifting the calculus to non-ground clauses turns out to be a non-trivial task. In the standard superposition calculus, for lifting one simply needs to replace equality in the ground inference by unifiability (or by equality constraints). The situation is similar here, as long as all variables in our clauses are shielded. If a variable is unshielded, however, we have to take into account that it might be instantiated with a sum and that only the maximal atomic part of the sum takes part in the unification. Consider the clauses D = D′(x) ∨ 3x + d ≈ e and C = C′(y) ∨ 5y + 2b ≈ c, where b is the maximal constant. A substitution may map x to μb + s and y to νb + t, for some ν, μ ∈ N and arbitrary ground terms s and t. If 3μ ≤ 5ν + 2, then the resulting ground clauses allow the cancellative superposition inference

\frac{D′(μb + s) ∨ 3μb + 3s + d ≈ e C′(νb + t) ∨ (5ν+2)b + 5t ≈ c}{D′(μb + s) ∨ C′(νb + t) ∨ (5ν+2−3μ)b + 5t + e ≈ c + 3s + d}

How can we represent this infinite number of ground clauses finitely on the non-ground level without introducing second-order variables?

For the left premise, it’s easy. We map the variable x to a sum of two fresh variables, x̂ + x̃. The variable x̂ is meant to subsume the part of μb + s that is consumed during the ground inference (namely μb); the second variable is meant to subsume the part that is left over (namely s).

For the right premise, the situation is a bit more complicated, since not all b’s need to be consumed. Each of the ν b’s produces 5 copies. If μ = 2, then there are 6 b’s to be consumed, thus ν ≥ 1. We may assume that these 6 b’s consist of 5 copies of one of the ν b’s and one of the 2 b’s that were present in the non-ground clause. As for the left premise, it suffices to map y to a sum of two fresh variables, ŷ + ỹ.

If μ = 3, then there are 9 b’s to be consumed, thus ν ≥ 2. Again we may assume that 5 of the 9 b’s are copies of one of the ν b’s. In this case, however, the remaining 4 b’s have to be taken from the 5 copies of the second of the ν b’s. Therefore, we have to map y to the sum ŷ + b + ỹ. The variable ŷ is meant to subsume those b’s, whose 5 copies are completely consumed. The variable ỹ is meant to subsume the part of νb + t that is left over. Finally, there is one b, for which λ of its 5 copies are consumed, where 3 ≤ λ ≤ 4.

We obtain two kinds of non-ground inferences: First, for the case that each of the ν b’s is either completely consumed or left over:

\frac{D′(x) ∨ 3x + d ≈ e C′(y) ∨ 5y + 2b ≈ c}{(D′(x̂ + x̃) ∨ C′(ŷ + ỹ) ∨ (2−λ)b + 5ỹ + e ≈ c + d + 3x̃)σ}

where 0 ≤ λ ≤ 2 and σ is a most general ACU-unifier of 3x̂ and 5ŷ + λb. Second, for the case that one of the ν b’s is only partially consumed:

\frac{D′(x) ∨ 3x + d ≈ e C′(y) ∨ 5y + 2b ≈ c}{(D′(x̂ + x̃) ∨ C′(ŷ + b + ỹ) ∨ (7−λ)b + 5ỹ + e ≈ c + d + 3x̃)σ}

where 3 ≤ λ ≤ 4 and σ is a most general ACU-unifier of 3x̂ and 5ŷ + λb.

In the general case, the maximal equations of the two clauses may have the form

∑_{j∈J} n_{j}y_{j} + ∑_{l∈L} n′_{l}v_{l} + t ≈ t′

with variables y_{j} and unifiable non-variable terms v_{l}. Using the idea above we can still obtain an inference rule that produces only finitely many conclusions. Let v be a most general common instance of all v_{l} (modulo ACU). In the left premise, we map every variable x_{i} to x̂_{i} + x̃_{i}. In the right premise, there are two possibilities: If every v that is substituted into the y_{j}’s is either completely consumed or left over, then it suffices to map every y_{j} to ŷ_{j} + ỹ_{j}. Otherwise, we have to map some y_{j_{0}} to the sum ŷ_{j_{0}} + v + ỹ_{j_{0}}, where λ of the n_{j_{0}} copies of v are consumed. (It is in fact sufficient to pick one j_{0} ∈ J and to restrict to ∑_{l∈L} n′_{l} < λ < n_{j_{0}}. Furthermore, we will show that we may set ŷ_{j} = 0 if either n_{j} ≤ ∑_{l∈L} n′_{l} + n_{j_{0}} − λ or n_{j} > n_{j_{0}}.) A similar technique is also used for cancellation inferences and cancellative equality factoring inferences.

It is obvious that inferences involving unshielded variables may be very prolific. In practice, they should be avoided whenever possible. In Section 5 we will discuss suitable techniques to do this.

Free Function Symbols So far, we have considered signatures where + is the only non-constant function symbol. If we add free function symbols, and possibly other sorts, then we also have to use the inference rules of the traditional superposition calculus, that is equality resolution, standard superposition, and standard equality factoring. But this is not sufficient, as shown by the following example.

Example 3.14 Suppose that the ordering on constant symbols is given by b ≻ b′ ≻ c ≻ d ≻ d′. In every model of the three clauses

\underline{2b} + c ≈ d  (1)
\underline{b′} + c ≈ d′  (2)
\underline{d} ≈ d′  (3)

the terms 2b and b′ are equal. As we have shown in Example 3.13 we can thus refute the set of clauses (1)–(4).

\underline{2b} ≉ b′  (4)

However, the cancellative superposition rule is limited to superpositions at the top of a term. There is no way to perform a cancellative superposition inference below a free function symbol, hence there is no way to derive the empty clause from the clauses (1), (2), (3), and (9).

\underline{f(2b)} ≉ f(b′)  (9)

If we were working in groups, we could simply derive f(d − c) ≉ f(b′). But this is impossible in our context.

Hsiang, Rusinowitch, and Sakai [17, 26] have solved this problem by introducing the following inference rule:

\frac{D ∨ u + s ≈ s′ C ∨ v + s ≈ s′}{D ∨ C ∨ u ≈ v}

In the example above, this rule allows to derive \underline{2b} ≈ b′ from the first three clauses, which can then be applied to (9) by standard superposition. However, there is a drawback of this approach. Before we can apply the rule of Hsiang, Rusinowitch, and Sakai, we have to use clause (3) to replace d by d′ in (1). Since the term d is not maximal in (1), the rule can be only used in conjunction with ordered paramodulation (where inferences may involve smaller parts of maximal literals), but does not work together with strict superposition (where such inferences are excluded).

The concept of abstraction yields another solution for the problem, which fits more smoothly into the superposition calculus. Abstracting out an occurrence of a term v in a clause C[v] means replacing v by a new variable x and adding x ≉ v as a new condition to the clause. In our case, we have to abstract out a term v of sort S_{CAM} occurring immediately below a free function symbol, if there is some other clause D ∨ mu + s ≈ s′ such that (i) mu occurs at the top of v, but (ii) a standard superposition of mu + s into v is impossible. We emphasize that the new variable x is shielded in the resulting clause.

\underline{Abstraction}  \frac{D ∨ mu + s ≈ s′  C ∨ [¬] w[nu + t] ≈ w′}{C ∨ ¬ x ≈ nu + t ∨ [¬] w[x] ≈ w′}

where n ≥ m.

Using this inference rule, the set of clauses (1), (2), (3), and (9) of Example 3.14 can be refuted as follows:

Example 3.15 Abstraction of (1) and (9) yields

x ≉ 2b ∨ \underline{f(x)} ≉ \underline{f(b′)}  (10)

By (non-ground) cancellation of (10) with the unifier {x ↦ b′} we obtain

b′ ≉ \underline{2b} ∨ 0 ≉ 0  (11)

which can be refuted in the same way as (4) in Example 3.13.

The abstraction rule is extended to non-ground premises in the same way as the cancellative superposition rule.

3.3 Inference System

General Remarks

In an expression like ∑_{i∈I} m_{i}x_{i} + ∑_{k∈K} m′_{k}u_{k} + s, every x_{i} is a variable of sort S_{CAM}, every u_{k} is an atomic term of sort S_{CAM}, and s is an arbitrary term of sort S_{CAM}. The coefficients m_{i} and m′_{k} are elements of N^{+}. Both I and K are linearly ordered sets of indices; I and K may be empty, s may be 0, unless explicitly said otherwise.

To simplify the presentation, we give the inference rules for unconstrained clauses. However, it should be mentioned that in fact all ordering conditions may be turned into constraints which are inherited by the conclusions of the inferences. Similarly, it may be advisable in an implementation to work with unifiability constraints as much as possible rather than computing unifiers eagerly.

We use the phrase “most general (t-preserving) ACU-unifier of u and v” to denote some member of a fixed complete set of (t-preserving) ACU-unifiers of u and v.

Cancellation

\frac{D ∨ [¬] e_{1}}{(D ∨ [¬] e_{0})σ}

if the following conditions are satisfied:

• e_{1} = ∑_{j∈J} n_{j}x_{j} + ∑_{l∈L} n′_{l}v_{l} + t ≈ ∑_{i∈I} m_{i}x_{i} + ∑_{k∈K} m′_{k}u_{k} + s.

• e_{0} = μz + ∑_{j∈J̃}ñ_{j}x̃_{j} + t ≈ ∑_{i∈Ĩ} m̃_{i}x̃_{i} + s.

• I ∪ K ≠ ∅ and J ∪ L ≠ ∅.

• { x_{i} | i ∈ I } is the set of all eligible variables of [¬] e_{1} that occur in the right hand side of e_{1}; { x_{j} | j ∈ J } is the set of all eligible variables of [¬] e_{1} that occur in the left hand side of e_{1}.

• Ĩ = I \ { i ∈ I ∩ J | n_{i} ≥ m_{i} }, J̃ = J \ { i ∈ I ∩ J | m_{i} ≥ n_{i} }, m̃_{i} = m_{i} if i ∈ I \ J, m̃_{i} = m_{i} − n_{i} if i ∈ I ∩ J and m_{i} > n_{i}, ñ_{i} = n_{i} if i ∈ J \ I, ñ_{i} = n_{i} − m_{i} if i ∈ I ∩ J and n_{i} > m_{i}.

• m′ = ∑_{k∈K} m′_{k} and n′ = ∑_{l∈L} n′_{l}.

• Either J_{−} = J̃, J_{0} = J_{=} = J_{+} = ∅, 0 ≤ λ ≤ n′, and μ = n′ − λ; or J_{0} = {j_{0}} ⊆ J̃, n′ < λ < ñ_{j_{0}}, J_{=} = { j ∈ J̃ | ñ_{j} ≤ n′ + ñ_{j_{0}} − λ }, J_{−} = { j ∈ J̃ | n′ + ñ_{j_{0}} − λ < ñ_{j} < ñ_{j_{0}} ∨ (ñ_{j} = ñ_{j_{0}} ∧ j < j_{0}) }, J_{+} = { j ∈ J̃ | ñ_{j} > ñ_{j_{0}} ∨ (ñ_{j} = ñ_{j_{0}} ∧ j > j_{0}) }, and μ = n′ + ñ_{j_{0}} − λ.

• σ_{1} maps x_{i} to x̂_{i} + x̃_{i} for i ∈ Ĩ ∪ J_{−}, to x̂_{i} + z + x̃_{i} for i ∈ J_{0}, and to x̃_{i} for i ∈ J_{=} ∪ J_{+}; σ_{2} is a most general ACU-unifier of all u_{k}, v_{l}, and z (k ∈ K, l ∈ L); σ_{3} is a most general zσ_{2}-preserving ACU-unifier of ∑_{i∈Ĩ} m̃_{i}x̂_{i} + m′zσ_{2} and ∑_{j∈J_{−}∪J_{0}} ñ_{j}x̂_{j} + λzσ_{2}; and σ = σ_{1}σ_{2}σ_{3}.

• Either ¬ e_{1} is a selected literal, or the premise has no selected literals and [¬] e_{1}σ is a maximal literal in (D ∨ [¬] e_{1})σ.

• zσ ⪯̸ sσ, zσ ⪯̸ tσ, zσ ⪯̸ x̃_{i}σ for i ∈ Ĩ∪ J_{+}, zσ ⊀_{x} x̃_{i}σ for i ∈ J_{=} ∪ J_{−} ∪ J_{0}.

Equality Resolution

\frac{C ∨ ¬ u ≈ v}{Cσ}

if the following conditions are satisfied:

• Either uσ = vσ = 0 or u and v don’t have sort S_{CAM} and σ is a most general ACU-unifier of u and v.

• Either ¬ u ≈ v is a selected literal, or ¬ (u ≈ v)σ is a maximal literal in (C ∨ ¬ u ≈ v)σ.

Standard Superposition

\frac{D ∨ u ≈ v C ∨ [¬] t[w] ≈ t′}{(D ∨ C ∨ [¬] t[v] ≈ t′)σ}

if the following conditions are satisfied: • w is not a variable.

• If t has sort S_{CAM}, then w occurs below a free function symbol in t. If t is a proper sum, then w occurs in a maximal atomic subterm of t.

• σ is a most general ACU-unifier of u and w.

• uσ ⪯̸ vσ and tσ ⪯̸ t′σ.

• The first premise has no selected literals.

• uσ ≈ vσ is a strictly maximal literal in (D ∨ u ≈ v)σ.

• Either ¬ t[w] ≈ t′ is a selected literal, or the second premise has no selected literals and ([¬] t[w] ≈ t′)σ is a maximal literal in (C ∨ [¬] t[w] ≈ t′)σ (strictly maximal, if it is a positive literal).

• (D ∨ u ≈ v)σ ⪰̸_{C} (C ∨ [¬] t[w] ≈ t′)σ.

Cancellative Superposition

\frac{D ∨ e_{1} C ∨ [¬] e_{2}}{(D ∨ C ∨ [¬] e_{0})σ}

if the following conditions are satisfied:

• e_{1} = ∑_{i∈I} m_{i}x_{i} + ∑_{k∈K} m′_{k}u_{k} + s ≈ s′.

• e_{2} = ∑_{j∈J} n_{j}y_{j} + ∑_{l∈L} n′_{l}v_{l} + t ≈ t′.

• e_{0} = μz + ∑_{j∈J} n_{j}ỹ_{j} + t + s′ ≈ ∑_{i∈I} m_{i}x̃_{i} + s + t′.

• I ∪ K ≠ ∅ and J ∪ L ≠ ∅.

• { x_{i} | i ∈ I } is the set of all eligible variables of e_{1} that occur in the left hand side but not in the right hand side of e_{1}; { y_{j} | j ∈ J } is the set of all eligible variables of [¬] e_{2} that occur in the left hand side but not in the right hand side of e_{2}.

• The left hand side of e_{2} is not a variable (i.e., either ∑_{j∈J} n_{j} > 1 or ∑_{l∈L} n′_{l}v_{l} + t ≠ 0).

• m′ = ∑_{k∈K} m′_{k} and n′ = ∑_{l∈L} n′_{l}.

• Either J_{−} = J, J_{0} = J_{=} = J_{+} = ∅, 0 ≤ λ ≤ n′, and μ = n′ − λ; or J_{0} = {j_{0}} ⊆ J, n′ < λ < n_{j_{0}}, J_{=} = { j ∈ J | n_{j} ≤ n′ + n_{j_{0}} − λ }, J_{−} = { j ∈ J | n′ + n_{j_{0}} − λ < n_{j} < n_{j_{0}} ∨ (n_{j} = n_{j_{0}} ∧ j < j_{0}) }, J_{+} = { j ∈ J | n_{j} > n_{j_{0}} ∨ (n_{j} = n_{j_{0}} ∧ j > j_{0}) }, and μ = n′ + n_{j_{0}} − λ.

• σ_{1} maps x_{i} to x̂_{i} + x̃_{i} for i ∈ I and y_{j} to ŷ_{j} + ỹ_{j} for j ∈ J_{−}, to ŷ_{j} + z + ỹ_{j} for j ∈ J_{0}, and to ỹ_{j} for i ∈ J_{=} ∪ J_{+}; σ_{2} is a most general ACU-unifier of all u_{k}, v_{l}, and z (k ∈ K, l ∈ L); σ_{3} is a most general zσ_{2}-preserving ACUunifier of ∑_{i∈I} m_{i}x̂_{i} + m′zσ_{2} and ∑_{j∈J_{−}∪J_{0}} n_{j}ŷ_{j} + λzσ_{2}; and σ = σ_{1}σ_{2}σ_{3}.

• The first premise has no selected literals.

• e_{1}σ is a strictly maximal literal in (D ∨ e_{1})σ.

• Either ¬ e_{2} is a selected literal, or the second premise has no selected literals and [¬] e_{2}σ is a maximal literal in (C ∨ [¬] e_{2})σ (strictly maximal, if e_{2} occurs positively).

• (D ∨ e_{1})σ ⪰̸_{C} (C ∨ [¬] e_{2})σ.

• zσ ⪯̸ sσ, zσ ⪯̸ s′σ, zσ ⪯̸ tσ, zσ ⪯̸ t′σ, zσ ⪯̸ x̃_{i}σ for i ∈ I, zσ ⪯̸ ỹ_{j}σ for j ∈ J_{+}, zσ ⊀_{x} ỹ_{j}σ for j ∈ J_{=} ∪ J_{−} ∪ J_{0}.

Abstraction

\frac{D ∨ e_{1} C ∨ [¬] w[ŵ] ≈ w′}{C ∨ ¬ x ≈ ŵ ∨ [¬] w[x] ≈ w′}

if the following conditions are satisfied:

• e_{1} = ∑_{i∈I} m_{i}x_{i} + ∑_{k∈K} m′_{k}u_{k} + s ≈ s′.

• ŵ = ∑_{j∈J} n_{j}y_{j} + ∑_{l∈L} n′_{l}v_{l} + t.

• I ∪ K ≠ ∅ and J ∪ L ≠ ∅.

• { x_{i} | i ∈ I } is the set of all eligible variables of e_{1} that occur in the left hand side but not in the right hand side of e_{1}.

• None of the variables y_{j} occurs in the non-variable terms v_{l}. (The y_{j} may occur in t, however.)

• ŵ occurs in w immediately below some free function symbol. If w is a proper sum, then ŵ occurs in a maximal atomic subterm of w.

• m′ = ∑_{k∈K} m′_{k} and n′ = ∑_{l∈L} n′_{l}.

• Either J_{−} = J, J_{0} = J_{=} = J_{+} = ∅, and 0 ≤ λ ≤ n′; or J_{0} = {j_{0}} ⊆ J, n′ < λ < n_{j_{0}}, J_{=} = { j ∈ J | n_{j} ≤ n′ + n_{j_{0}} − λ }, J_{−} = { j ∈ J | n′ + n_{j_{0}} − λ < n_{j} < n_{j_{0}} ∨ (n_{j} = n_{j_{0}} ∧ j < j_{0}) }, and J_{+} = { j ∈ J | n_{j} > n_{j_{0}} ∨ (n_{j} = n_{j_{0}} ∧ j > j_{0}) }.

• σ_{1} maps x_{i} to x̂_{i} + x̃_{i} for i ∈ I and y_{j} to ŷ_{j} + ỹ_{j} for j ∈ J_{−}, to ŷ_{j} + z + ỹ_{j} for j ∈ J_{0}, and to ỹ_{j} for i ∈ J_{=} ∪ J_{+}; σ_{2} is a most general ACU-unifier of all u_{k}, v_{l}, and z (k ∈ K, l ∈ L); σ_{3} is a most general zσ_{2}-preserving ACUunifier of ∑_{i∈I} m_{i}x̂_{i} + m′zσ_{2} and ∑_{j∈J_{−}∪J_{0}} n_{j}ŷ_{j} + λzσ_{2}; and σ = σ_{1}σ_{2}σ_{3}.

• The first premise has no selected literals.

• e_{1}σ is a strictly maximal literal in (D ∨ e_{1})σ.

• Either ¬ w[ŵ] ≈ w′ is a selected literal, or the second premise has no selected literals and [¬] (w[ŵ] ≈ w′)σ is a maximal literal in (C ∨ [¬] w[ŵ] ≈ w′)σ (strictly maximal, if it is a positive literal).

• If J = {j_{1}}, n_{j_{1}} = 1, and L = ∅, then t = t_{1} + t_{2}, where t_{1} is non-zero and either t_{1} is a variable or y_{j_{1}}σ ⊀ t_{1}σ.

• If I = ∅, then there exists no t′ such that tσ = sσ + t′.

• (D ∨ e_{1})σ ⪰̸_{C} (C ∨ [¬] w[ŵ] ≈ w′)σ.

• zσ ⪯̸ sσ, zσ ⪯̸ s′σ, (w[ŵ])σ ⪯̸ w′σ.

Standard Equality Factoring

\frac{D ∨ u ≈ v ∨ u′ ≈ v′}{(D ∨ ¬ v ≈ v′ ∨ u′ ≈ v′)σ}

if the following conditions are satisfied: • u, u′, v, and v′ don’t have sort S_{CAM}.

• The premise has no selected literals.

• σ is a most general ACU-unifier of u and u′.

• uσ ⪯̸ vσ and uσ ⪯̸ v′σ.

• uσ ≈ vσ is a maximal literal in (D ∨ u ≈ v ∨ u′ ≈ v′)σ.

• uσ is maximal in (D ∨ u ≈ v ∨ u′ ≈ v′)σ.

Cancellative Equality Factoring

\frac{D ∨ e_{1} ∨ e_{2}}{(D ∨ ¬ e_{0} ∨ e_{2})σ}

if the following conditions are satisfied:

• e_{1} = ∑_{i∈I} m_{i}x_{i} + ∑_{k∈K} m′_{k}u_{k} + s ≈ s′.

• e_{2} = ∑_{j∈J} n_{j}x_{j} + ∑_{l∈L} n′_{l}v_{l} + t ≈ t′.

• e_{0} = ∑_{i∈I} m_{i}x̃_{i} + s + t′ ≈ ∑_{j∈J} n_{j}x̃_{j} + s′ + t.

• I ∪ K ≠ ∅ and J ∪ L ≠ ∅.

• { x_{i} | i ∈ I } is the set of all eligible variables of e_{1} that occur in the left hand side but not in the right hand side of e_{1}; { x_{j} | j ∈ J } is the set of all eligible variables of e_{2} that occur in the left hand side but not in the right hand side of e_{2}.

• m′ = ∑_{k∈K} m′_{k} and n′ = ∑_{l∈L} n′_{l}.

• σ_{1} maps x_{i} to x̂_{i} + x̃_{i} for i ∈ I ∪ J; σ_{2} is a most general ACU-unifier of all u_{k}, v_{l}, and z (k ∈ K, l ∈ L); σ_{3} is a most general zσ_{2}-preserving ACU-unifier of ∑_{i∈I} m_{i}x̂_{i} + m′zσ_{2} and ∑_{j∈J} n_{j}x̂_{j} + n′zσ_{2}.

• The premise has no selected literals.

• e_{1}σ is a maximal literal in (D ∨ e_{1} ∨ e_{2})σ.

• zσ ⪯̸ sσ, zσ ⪯̸ s′σ, zσ ⪯̸ tσ, zσ ⪯̸ t′σ, zσ ⪯̸ x̃_{i}σ for i ∈ I ∪ J.

Theorem 3.16 For every inference rule

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

of the cancellative superposition calculus, we have {C_{1}, …, C_{n}} ⊧ C_{0}.

Proof. By routine computation. □

3.4 Redundancy and Saturation

To make a saturation-based theorem proving technique practically useful, the inference system has to be complemented with a redundancy criterion. Both clauses and inferences may be redundant. A redundant clause can be deleted from the current set of clauses at any point of the saturation process. A redundant inference may be ignored during the saturation process without endangering the fairness of the derivation. (See [4, 6] for a more detailed discussion of these aspects of superposition. Note that “redundancy” is called “compositeness” in [4].)

Definition 3.17 Let N be a set of clauses. A ground clause D is called ACUK-redundant with respect to N, if ground instances D_{1}, …, D_{n} of clauses in N exist such that {D_{1}, …, D_{n}} ⊧ D and D_{i} ≺_{C} D for every i ∈ {1, …, n}. A non-ground clause is called ACUK-redundant with respect to N, if all its ground instances are.

Traditionally, an inference is considered to be redundant, if its conclusion follows from clauses that are smaller than the maximal premise. Since the conclusion of an abstraction inference is non-ground even if the premises are ground, we have to modify this scheme slightly.

Definition 3.18 Let N be a set of clauses. A ground inference with conclusion C_{0} and maximal premise C is called ACUK-redundant with respect to N in the following two cases:

• If it is not an abstraction inference and if there are ground instances D_{1}, …, D_{n} of clauses in N such that {D_{1}, …, D_{n}} ⊧ C_{0} and D_{i} ≺_{C} C for every i ∈ {1, …, n}.

• If it is an abstraction inference

\frac{D′ ∨ mu + s ≈ s′ C′ ∨ [¬] w[nu + t] ≈ w′}{C′ ∨ ¬ x ≈ nu + t ∨ [¬] w[x] ≈ w′}

and if for every substitution ρ that maps x to a ground term r ≺ nu + t there exist ground instances D_{1}, …, D_{n} of clauses in N such that {D_{1}, …, D_{n}} ⊧ C_{0}ρ and D_{i} ≺_{C} C for every i ∈ {1, …, n}.

To extend this definition to non-ground inferences, we need the concept of an instance of an inference.

Definition 3.19 Let C_{1}, …, C_{n} be clauses and let θ be a substitution such that all C_{i}θ are ground. If there are inferences (modulo ACU)

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

and

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

then the former inference is called a ground instance of the latter.

It should be noted that not every inference from C_{1}θ … C_{n}θ is a ground instance of an inference from C_{1} … C_{n}. As in the standard superposition calculus [4], a ground superposition may take place below a variable position of C_{n}. For instance, if C_{1} = a ≈ b and C_{2} = f(x, x) ≈ x, then there is a standard superposition inference from the ground instances C_{1}θ = a ≈ b and C_{2}θ = f(a, a) ≈ a, but not from C_{1} and C_{2} themselves.

Cancellation inferences pose an additional difficulty. If a variable x occurs on both sides of an equation in a clause C, then in a non-ground cancellation inference it is removed completely, whereas a ground inference from Cθ may remove xθ only partially. Consider the following example. Let b, c, d be constants such that b ≻ c ≻ d, and let C be a clause x + c ≈ x + d. Then there is a cancellation inference from C, namely

\frac{x + c ≈ x + d}{c ≈ d}

In a ground instance of C, x might be instantiated with a sum b + d. But

\frac{b + c + d ≈ b + 2d}{c ≈ d}

does not qualify as a cancellation inference. Conversely,

\frac{b + c + d ≈ b + 2d}{c + d ≈ 2d}

qualifies as a cancellation inference, but it is not an instance of the non-ground inference above. The notion of a weak instance will encompass such cases.

Definition 3.20 Let C = C′ ∨ [¬] e be a clause and let θ be a substitution such that Cθ is ground. If there are cancellation inferences (modulo ACU)

\frac{C′θ ∨ [¬] eθ}{C′θ ∨ [¬] s + t ≈ s + t′}

and

\frac{C′ ∨ [¬] e}{D}

and Dθ = C′θ ∨ [¬] t ≈ t′, then the former inference is called a weak ground instance of the latter.

Definition 3.21 A non-ground inference is called ACUK-redundant with respect to N in the following two cases:

• If it is not a cancellation inference and if all its ground instances are ACUK-redundant.

• If it is a cancellation inference and if all its weak ground instances are ACUK-redundant.

One way to make an inference from clauses in N redundant is to add its conclusion to N.

Definition 3.22 We say that a set N of clauses is saturated up to ACUKredundancy, if every inference from non-ACUK-redundant clauses in N is ACUK-redundant.

Under which conditions is an inference from ground clauses C_{i}θ a (weak) ground instance of an inference from C_{i}? This question will be answered by the so-called “lifting lemmas”. To prove them, we need the following technical lemma.

Lemma 3.23 Let J be a finite and linearly ordered set of indices. Suppose that m, n ∈ N, and n_{j} ∈ N^{+}, ν_{j} ∈ N for every j ∈ J. Furthermore, assume that m ≤ ∑_{j∈J} n_{j}ν_{j} + n. Then one of the following two properties holds:

(i) There exist λ ∈ N and κ_{j} ∈ N, such that λ ≤ n, κ_{j} ≤ ν_{j} for j ∈ J, and m = ∑_{j∈J} n_{j}κ_{j} + λ.

(ii) There exist λ ∈ N, κ_{j} ∈ N, and j_{0} ∈ J such that n < λ < n_{j_{0}}, κ_{j} ≤ ν_{j} for j ∈ J, κ_{j_{0}} < ν_{j_{0}}, ν_{j} = 0 whenever n_{j} > n_{j_{0}} ∨ (n_{j} = n_{j_{0}} ∧ j > j_{0}), κ_{j} = 0 whenever n_{j} ≤ n + n_{j_{0}} − λ, and m = ∑_{j∈J} n_{j}κ_{j} + λ.

Proof. Let m_{0} = ∑_{j∈J} n_{j}ν_{j}. Assume that property (i) does not hold. Then obviously n < m < m_{0}, and hence ν_{j} > 0 for some j ∈ J. Let n_{max} be the maximum of { n_{j} | j ∈ J, ν_{j} > 0 }, and let j_{0} be the maximum of { j ∈ J | n_{j} = n_{max}, ν_{j} > 0 }.

Let M denote the set of all μ ∈ N such that there are κ_{j} ∈ N with κ_{j} ≤ ν_{j} for j ∈ J, κ_{j_{0}} < ν_{j_{0}}, and μ = ∑_{j∈J} n_{j}κ_{j}. It is easy to see that {0, m_{0} − n_{j_{0}}} ⊆ M ⊆ {0, 1, …, m_{0} − n_{j_{0}}}. Furthermore, if μ_{1} and μ_{2} are elements of M such that μ_{1} < μ_{2} and { μ ∈ M | μ_{1} < μ < μ_{2} } is empty, then μ_{2} − μ_{1} ≤ n_{j_{0}}. Therefore, there exist μ ∈ M such that μ ≤ m < μ + n_{j_{0}}. Let μ_{0} be the smallest μ ∈ M with this property, and let λ = m − μ_{0}, then m = ∑_{j∈J} n_{j}κ_{j} + λ as required. Obviously, λ = m − μ_{0} < n_{j_{0}}. Besides, λ ≤ n would imply that property (i) holds, so n < λ < n_{j_{0}}.

It remains to show that κ_{j} = 0 whenever n_{j} ≤ n + n_{j_{0}} − λ. Assume there were a j_{1} ∈ J such that n_{j_{1}} ≤ n + n_{j_{0}} − λ and κ_{j_{1}} > 0. Then define κ′_{j} = κ_{j} for j ≠ j_{1} and κ′_{j_{1}} = κ_{j_{1}} − 1. Consequently, m = ∑_{j∈J} n_{j}κ_{j} + λ = ∑_{j∈J} n_{j}κ′_{j} + n_{j_{1}} + λ. If n_{j_{1}} < n_{j_{0}} − λ, then this contradicts the minimality of μ_{0}. Otherwise n_{j_{0}} − λ ≤ n_{j_{1}} ≤ n + n_{j_{0}} − λ. Let λ′ = n_{j_{1}} + λ − n_{j_{0}}, κ′′_{j} = κ′_{j} for j ≠ j_{0}, and κ′′_{j_{0}} = κ′_{j_{0}} + 1, then m = ∑_{j∈J} n_{j}κ′_{j} + n_{j_{0}} + λ′ = ∑_{j∈J} n_{j}κ′′_{j} + λ′. As λ′ ≤ n, this contradicts our assumption that property (i) does not hold.

□

Lemma 3.24 Let C be a clause and let θ be a substitution such that Cθ is ground. Then every cancellation inference from Cθ is a weak ground instance of a cancellation inference from C.

Proof. Suppose that Cθ = C′θ ∨ [¬] e_{1}θ and e_{1}θ = nū + t̄ ≈ mū + s̄, such that ū is an atomic ground term, ū ≻ s̄, ū ≻ t̄, and n ≥ m ≥ 1. If either ¬ e_{1}θ is a selected literal, or Cθ has no selected literals and [¬] e_{1}θ is maximal in Cθ, then this clause allows a cancellation inference

C′θ ∨ [¬] nū + t̄≈ mū + s̄
C′θ ∨ [¬] (n−m)ū + t̄≈ s̄

By maximality, ū may only result from instantiating eligible variables or atomic terms. Let { x_{j} | j ∈ J } and { x_{i} | i ∈ I } be the sets of all eligible variables of [¬] e_{1} that occur in the left or right hand side of e_{1}, respectively. We may assume that

e_{1} = ∑_{j∈J} n_{j}x_{j} + ∑_{l∈L} n′_{l}v_{l} + t ≈ ∑_{i∈I} m_{i}x_{i} + ∑_{k∈K} m′_{k}u_{k} + s

such that

x_{i}θ = ν_{i}ū + s̄_{i} for i ∈ I ∪ J, where ν_{i} ∈ N and ū ≻ s̄_{i},
v_{l}θ = ū for l ∈ L,
u_{k}θ = ū for k ∈ K,
n′ = ∑_{l∈L} n′_{l},
m′ = ∑_{k∈K} m′_{k},
n = ∑_{j∈J} n_{j}ν_{j} + n′,
m = ∑_{i∈I} m_{i}ν_{i} + m′,
t̄= ∑_{j∈J} n_{j}s̄_{j} + tθ,
s̄ = ∑_{i∈I} m_{i}s̄_{i} + sθ.

Let Ĩ = I \ { i ∈ I ∩ J | n_{i} ≥ m_{i} }, J̃ = J \ { i ∈ I ∩ J | m_{i} ≥ n_{i} }, m̃_{i} = m_{i} if i ∈ I \ J, m̃_{i} = m_{i} − n_{i} if i ∈ I ∩ J and m_{i} > n_{i}, ñ_{i} = n_{i} if i ∈ J \ I, ñ_{i} = n_{i} − m_{i} if i ∈ I ∩ J and n_{i} > m_{i}, p_{i} = min{m_{i}, n_{i}} for i ∈ I ∩ J. Note that Ĩ and J̃ are disjoint. Let ñ = ∑_{j∈J̃} ñ_{j}ν_{j} + n′, m̃ = ∑_{i∈Ĩ} m̃_{i}ν_{i} + m′, and p̃ = ∑_{i∈I∩J} p_{i}ν_{i}, then ñ + p̃ = n and m̃ + p̃ = m. As m ≤ n, we obtain

m̃ ≤ ñ = ∑_{j∈J̃}ñ_{j}ν_{j} + n′ .

We have to distinguish two cases. If there exist λ, κ_{j} ∈ N such that λ ≤ n′, κ_{j} ≤ ν_{j} for j ∈ J̃, and m̃ = ∑_{j∈J̃} ñ_{j}κ_{j} + λ, then let μ = n′ − λ, J_{−} = J̃ and J_{0} = J_{=} = J_{+} = ∅.

Otherwise, by Lemma 3.23, there exist λ, κ_{j} ∈ N and j_{0} ∈ J̃ such that n′ < λ < ñ_{j_{0}}, κ_{j_{0}} < ν_{j_{0}}, κ_{j} ≤ ν_{j} for j ∈ J, ν_{j} = 0 for j ∈ J_{+}, κ_{j} = 0 for j ∈ J_{=}, and m̃ = ∑_{j∈J̃} ñ_{j}κ_{j} + λ, where J_{=} = { j ∈ J̃ | ñ_{j} ≤ n′ + ñ_{j_{0}} − λ } and J_{+} = { j ∈ J̃ | ñ_{j} > ñ_{j_{0}} ∨ (ñ_{j} = ñ_{j_{0}} ∧ j > j_{0}) }. Let μ = n′ + ñ_{j_{0}} − λ, J_{0} = {j_{0}}, and J_{−} = { j ∈ J̃ | n′ + ñ_{j_{0}} − λ < ñ_{j} < ñ_{j_{0}} ∨ (ñ_{j} = ñ_{j_{0}} ∧ j < j_{0}) }.

We define two substitutions σ_{1} and ρ_{1} as follows: Let σ_{1} map x_{i} to x̂_{i} + x̃_{i} for i ∈ Ĩ ∪ J_{−}, to x̂_{i} + z + x̃_{i} for i ∈ J_{0}, and to x̃_{i} for i ∈ J_{=} ∪ J_{+}. Let ρ_{1} map x̂_{i} to ν_{i}ū for i ∈ Ĩ and to κ_{i}ū for i ∈ J_{−} ∪ J_{0}, x̃_{i} to s̄_{i} for i ∈ Ĩ ∪ J_{+}, to (ν_{i}−κ_{i})ū + s̄_{i} for i ∈ J_{=} ∪ J_{−}, and to (ν_{i}−κ_{i}−1)ū + s̄_{i} for i ∈ J_{0}, x_{i} to ν_{i}ū + s̄_{i} for i ∈ (I ∪ J) \ (Ĩ∪ J̃), z to ū, and every other variable y ∈ Var(C) to yθ. It is easy to verify that θ equals σ_{1}ρ_{1} over Var(C).

As ρ_{1} equals θ over all variables occurring in u_{k} and v_{l}, ρ_{1} is a unifier of u_{k}, v_{l}, and z (k ∈ K, l ∈ L). Hence there is a most general ACU-unifier σ_{2} of all u_{k}, v_{l}, and z and a substitution ρ_{2} such that ρ_{1} = σ_{2}ρ_{2} over Var(C) ∪ Ran(σ_{1}). We may assume that Dom(σ_{2}) ⊆ Var({ u_{k}, v_{l}, z | k ∈ K, l ∈ L }).

Now consider the terms r = ∑_{i∈Ĩ} m̃_{i}x̂_{i} + m′zσ_{2} and r′ = ∑_{j∈J_{−}∪J_{0}} ñ_{j}x̂_{j} + λzσ_{2}. As x̂_{i}ρ_{2} = x̂_{i}ρ_{1} and zσ_{2}ρ_{2} = zρ_{1} = ū, we obtain rρ_{2} = r′ρ_{2} = m̃ū. Besides, ρ_{2} maps zσ_{2} to the non-zero atomic ground term ū. By Lemma 3.10, there is a most general zσ_{2}-preserving ACU-unifier σ_{3} of r and r′, such that ρ_{2} = σ_{3}ρ_{3} over Var(C) ∪ Ran(σ_{1}) ∪ Ran(σ_{2}). Let σ = σ_{1}σ_{2}σ_{3}.

We define

e_{0} = μz + ∑_{j∈J̃}ñ_{j}x̃_{j} + t ≈ ∑_{i∈Ĩ} m̃_{i}x̃_{i} + s

then

\frac{C′ ∨ [¬] e_{1}}{(C′ ∨ [¬] e_{0})σ}

is a cancellation inference from C that we denote by ι. It is easy to see that the ordering conditions of the inference rule are satisfied.

It remains to show that the cancellation inference ι′ given by

C′θ ∨ [¬] nū + t̄≈ mū + s̄
C′θ ∨ [¬] (n−m)ū + t̄≈ s̄

is a weak ground instance of ι. We apply the substitution σρ_{3} to the premise and the conclusion of ι. First, σρ_{3} equals θ over Var(C) and σ is idempotent, so C′σσρ_{3} = C′σρ_{3} = C′θ and e_{1}σρ_{3} = nū + t̄≈ mū + s̄.

Second, σσρ_{3} equals ρ_{1} over Var(e_{0}). Thus, after some computation, e_{0}σσρ_{3} = e_{0}ρ_{1} turns out to be (ñ−m̃)ū + ∑_{j∈J̃} ñ_{j}s̄_{j} + tθ ≈ ∑_{i∈Ĩ} m̃_{i}s̄_{i} + sθ.

Now n − m = (ñ+p̃) − (m̃+p̃) = ñ − m̃. Furthermore, if w = ∑_{i∈I∪J} p_{i}s̄_{i}, then t̄ = ∑_{j∈J̃} ñ_{j}s̄_{j} + tθ + w and s̄ = ∑_{i∈Ĩ} m̃_{i}s̄_{i} + sθ + w, hence ι′ is a weak ground instance of ι. □

Lemma 3.25 Let C be a clause and let θ be a substitution such that Cθ is ground. Then every equality resolution, standard equality factoring, or cancellative equality factoring inference from Cθ is a ground instance of a cancellation inference from C.

Proof. For equality resolution and standard equality factoring inferences, this is proved as in the classical case. The proof for cancellative equality factoring inferences is similar to the proof of Lemma 3.24. The main differences are that we can work directly with I and J (so there is no need to compute Ĩ and J̃ first), and that m and n in the proof of Lemma 3.24 are now identical (so every variable x_{i} is mapped to x̂_{i} + x̃_{i}). □

Lemma 3.26 Let C_{1} = C′_{1} ∨ s ≈ s′ and C_{2} = C′_{2} ∨ [¬] t ≈ t′ be two clauses (without common variables) and let θ be a substitution such that C_{1}θ and C_{2}θ are ground.

If there is a cancellative superposition inference

\frac{C′_{1}θ ∨ sθ ≈ s′θ C′_{2}θ ∨ [¬] tθ ≈ t′θ}{D}

(where the maximal atomic subterms of sθ and tθ are overlapped), and t is not a variable, then the inference is a ground instance of a cancellative superposition inference from C_{1} and C_{2}.

If there is a standard superposition inference

\frac{C′_{1}θ ∨ sθ ≈ s′θ C′_{2}θ ∨ [¬] tθ[sθ] ≈ t′θ}{D}

and sθ does not occur in tθ at or below a variable position of t (i.e., xθ = w[sθ] for some x ∈ Var(t)), then the inference is a ground instance of a standard superposition inference from C_{1} and C_{2}.

If there is an abstraction inference

\frac{C′_{1}θ ∨ sθ ≈ s′θ C′_{2}θ ∨ [¬] tθ[ŵθ] ≈ t′θ}{C′_{2}θ ∨ ¬ x ≈ ŵθ ∨ [¬] tθ[x] ≈ t′θ}

where ŵθ = t_{0} + t_{1} doesn’t occur below a variable position of t, the maximal atomic subterms of sθ overlap with t_{0}, and if ŵ = z + t̂ and t_{0} occurs below z, then t̂ = t̂′ + t̂′′ and t̂′ is a variable or 0 ≺ t̂′θ ⪯ t_{0}, then the inference is a ground instance of an abstraction inference from C_{1} and C_{2}.

Proof. For standard superposition inferences, this is proved as in the classical case. For cancellative superposition and abstraction inferences, the proof is again similar to the proof of Lemma 3.24. The main difference is that we can work directly with I and J (so there is no need to compute Ĩ and J̃ first).

□

4 Refutational Completeness

4.1 Rewriting on Equations

To show that the inference system described so far is refutationally complete we have to demonstrate that every saturated clause set that doesn’t contain the empty clause has a model. The traditional approach to construct such a model is rewrite-based: First an ordering is imposed on the set of all ground instances of clauses in the set. Starting with an empty interpretation all such instances are inspected in ascending order. If a reductive clause is false and irreducible in the partial interpretation constructed so far, its maximal equation is turned into a rewrite rule and added to the interpretation. If the original clause set is saturated and doesn’t contain the empty clause, then the final interpretation is a model of all ground instances, and thus of the original clause set (Bachmair and Ganzinger [4]).

In our case, we have to modify this scheme. For an adequate treatment of cancellative superposition it is not sufficient to be able to replace equals by equals inside a term. Rather, we need a rewrite relation on equations.

Definition 4.1 A ground equation e is called a rewrite rule if mt(e) doesn’t occur on both sides of e.

Every rewrite rule has either the form nv + s ≈ s′, where v is an atomic term, n ∈ N^{+}, v ≻ s, and v ≻ s′, or the form v ≈ s′, where v (and thus s′) does not have sort S_{CAM}. This is an easy consequence of the multiset property of ≻.

At the top of a term, we will use rewrite rules in a specific way: Application of a rule nv + s ≈ s′ to an equation nv + t ≈ t′ means to replace nv by s′ and simultaneously to add s to the other side, obtaining s′ + t ≈ t′ + s.^{7} However, this is only possible at the top of an equation, not below a free symbol. Consequently, there may be equations t ≈ t′ that can be reduced to 0 ≈ 0, whereas f(t) ≈ f(t′) is irreducible. To compensate for this fact our rewrite relation takes two sets of rewrite rules as parameters: one set of rules generated directly from the clause set, and a second set of “derived” rules, which are applied only below a free symbol and will fix the problem above.

Definition 4.2 Given a pair (R, R′) of sets of rewrite rules, the three relations →_{γ,(R,R′)}, →_{δ,(R,R′)}, and →_{κ} are defined (modulo ACU) as follows:

• nv + t ≈ t′ →_{γ,(R,R′)} s′ + t ≈ t′ + s,

if nv + s ≈ s′ is a rule in R.

• t[s] ≈ t′ →_{δ,(R,R′)} t[s′] ≈ t′,

if (i) s ≈ s′ is a rule in R ∪ R′ and (ii) s doesn’t have sort S_{CAM} or s occurs in t below some free function symbol.

• u + t ≈ u + t′ →_{κ} t ≈ t′, u ≈ u →_{κ} 0 ≈ 0,

if u is different from 0.

The union of →_{γ,(R,R′)}, →_{δ,(R,R′)}, and →_{κ} is denoted by →_{(R,R′)}.

We say that an equation e is γ-reducible, if e →_{γ} e′ (analogously for δ and κ). It is called reducible, if it is γ-, δ-, or κ-reducible.

Unlike κ-reducibility, γ- and δ-reducibility can be extended to terms: A term t is called γ-reducible, if t ≈ t′ →_{γ} e′, where the rewrite step takes place at the left hand side (analogously for δ). It is called reducible, if it is γ- or δ-reducible.

7While we have the restriction v ≻ s, v ≻ s′ for the rewrite rules, there is no such restriction for the equations to which rules are applied.

Lemma 4.3 The relation →_{(R,R′)} is contained in ≻_{L} and thus noetherian.

Definition 4.4 Given a pair (R, R′) of sets of rewrite rules, the truth set tr(R, R′) of (R, R′) is the set of all equations t ≈ t′ for which there exists a derivation t ≈ t′ →_{(R,R′)}^{∗} 0 ≈ 0.

4.2 Model Construction

Definition 4.5 A ground clause C ∨ e is called reductive for e, if e is a rewrite rule and strictly maximal in C ∨ e.

Definition 4.6 Let N be a set of (possibly non-ground) clauses and let \overline{N} be the set of all ground instances of clauses in N. Using induction on the clause ordering we define sets of rules R_{C}, R_{C}^{K}, E_{C}, and E_{C}^{K}, for all clauses C ∈ \overline{N}. Let C be such a clause and assume that R_{D}, R_{D}^{K}, E_{D}, and E_{D}^{K} have already been defined for all D ∈ \overline{N} such that C ≻_{C} D. Then

R_{C} = ⋃_{D≺_{C}C} E_{D}  and  R_{C}^{K} = ⋃_{D≺_{C}C} E_{D}^{K} .

E_{C} is the singleton set {e}, if C is a clause C′ ∨ e such that (i) C is reductive for e, (ii) C is false in tr(R_{C}, R_{C}^{K}), (iii) C′ is false in tr(R_{C} ∪ {e}, R_{C}^{K}), and (iv) mt_{#}(e) is irreducible with respect to (R_{C}, R_{C}^{K}). Otherwise, E_{C} is empty.

The set E_{C}^{K} is non-empty only if E_{C} contains a rule nv + s ≈ s′. In this case, E_{C}^{K} is the set of all knv + r ≈ r′ ∈ tr(R_{C} ∪ E_{C}, R_{C}^{K}) such that v ≻ r, v ≻ r′, and knv + r ≈ r′ is δκ-irreducible with respect to (R_{C}, R_{C}^{K}).

Finally, the sets R_{∞} and R_{∞}^{K} are defined by

R_{∞} = ⋃_{D∈\overline{N}} E_{D}  and  R_{∞}^{K} = ⋃_{D∈\overline{N}} E_{D}^{K} .

Our goal is to show that tr(R_{∞}, R_{∞}^{K}) is a model of the axioms of cancellative abelian monoids, and, for certain clause sets N, also a model of N. To this end, we will first put together some basic properties of R_{C} and R_{C}^{K}. In Section 4.3 we prove that the rewrite relation associated with (R_{C}, R_{C}^{K}) satisfies a restricted confluence property. The equality axioms and the laws of cancellative abelian monoids follow as easy corollaries. Then we show in Section 4.4 that tr(R_{∞}, R_{∞}^{K}) is in fact a model of N, provided that N is saturated and does not contain the empty clause.

Lemma 4.7 Let C and D be two clauses from \overline{N} such that C ≻_{C} D. If E_{C} = {e_{1}} and E_{D} = {e_{2}}, then mt(e_{1}) ≻ mt(e_{2}).

Proof. Suppose that mt(e_{1}) ⪯ mt(e_{2}). Then either mt_{#}(e_{1}) ≺ mt_{#}(e_{2}), so by the definition of the clause ordering, we would have C ≺_{C} D. Or mt(e_{1}) = mt(e_{2}) and mt_{#}(e_{1}) ⪰ mt_{#}(e_{2}), then mt_{#}(e_{1}) could be γ- or δ-reduced using e_{2}. This is impossible, however. □

Lemma 4.8 For every C ∈ \overline{N}, R_{C} ∪ R_{C}^{K} ⊆ tr(R_{C}, R_{C}^{K}) and R_{∞} ∪ R_{∞}^{K} ⊆ tr(R_{∞}, R_{∞}^{K}).

Lemma 4.9 If the rewrite rule e is contained in tr(R_{C}, R_{C}^{K}), then mt_{#}(e) is reducible by (R_{C}, R_{C}^{K}).

Proof. Suppose that e = nv + s ≈ s′, where v = mt(e), n ∈ N^{+}, v ≻ s, and v ≻ s′. Then there is a derivation

nv + s ≈ s′ →_{(R_{C},R_{C}^{K})}^{∗} 0 ≈ 0 .

During this derivation, all occurrences of v are deleted eventually. As s and s′ are smaller than v, it is impossible to derive an occurrence of v on the righthand side. Therefore, the occurrences of v cannot be deleted by κ-steps, but only by γ- or δ-steps, so nv is reducible.

The case that e = v ≈ s′ and v doesn’t have sort S_{CAM} is proved in the same way. □

Lemma 4.10 If nv + s = s′ is a rewrite rule from E_{C}, then for every knv + r ≈ r′ ∈ E_{C} ∪ E_{C}^{K} there is an (R_{C} ∪ E_{C}, R_{C}^{K})-derivation

knv + r ≈ r′ →_{γ}^{+} r + ks′ ≈ r′ + ks →^{∗} 0 ≈ 0

starting with k-fold application of nv + s = s′.

Proof. If knv + r ≈ r′ ∈ E_{C}, then this is obvious, as E_{C} is a singleton. If knv + r ≈ r′ ∈ E_{C}^{K}, then by definition, there is a derivation

knv + r ≈ r′ →_{(R_{C}∪E_{C},R_{C}^{K})}^{∗} 0 ≈ 0 .

During this derivation, all occurrences of v are deleted eventually. As knv + r ≈ r′ is δκ-irreducible with respect to (R_{C}, R_{C}^{K}), this can only happen by k-fold γ-application of nv + s = s′. These γ-steps are independent of any preceding rewrite steps, hence we can shift them to the front of the derivation. □

Lemma 4.11 Let v be an atomic term, n ∈ N^{+}. If nv is γ-reducible by (R_{∞}, R_{∞}^{K}) or (R_{C}, R_{C}^{K}) for some C ∈ \overline{N} then nv is δ-irreducible by (R_{∞}, R_{∞}^{K}) and (R_{D}, R_{D}^{K}) for every D ∈ \overline{N}.

Proof. If nv is γ-reducible, then there exists a rule kv + s ≈ s′ ∈ E_{C′}, where k ≤ n. Suppose that nv were δ-reducible using a rule t ≈ t′ ∈ E_{D′} ∪ E_{D′}^{K}. We distinguish between three cases:

If D′ ≺_{C} C′, then t would have to be a subterm of v. Consequently, kv would be reducible with respect to (R_{C′}, R_{C′}^{K}), which is impossible by the definition of E_{C′}.

If D′ ≻_{C} C′, then t is strictly larger than k′v for any k′ ∈ N^{+}, hence nv cannot be δ-reduced by t ≈ t′.

If D′ = C′ then t has the form k′kv + r, and a δ-reduction using t ≈ t′ may take place only below a free function symbol. Again, it is impossible to δ-reduce nv by t ≈ t′. □

Lemma 4.12 If C ∈ \overline{N} and if e ∈ tr(R_{C} ∪ E_{C}, R_{C}^{K}) is δκ-irreducible with respect to (R_{C} ∪ E_{C}, R_{C}^{K}), then e ∈ R_{C}^{K} ∪ E_{C}^{K} ∪ {0 ≈ 0}.

If C ∈ \overline{N} and if e ∈ tr(R_{C}, R_{C}^{K}) is δκ-irreducible with respect to (R_{C}, R_{C}^{K}), then e ∈ R_{C}^{K} ∪ {0 ≈ 0}. Similarly, if e ∈ tr(R_{∞}, R_{∞}^{K}) is δκ-irreducible with respect to (R_{∞}, R_{∞}^{K}), then e ∈ R_{∞}^{K} ∪ {0 ≈ 0}.

Proof. Suppose that e is different from 0 ≈ 0 and let v = mt(e). Without loss of generality we may assume that e = nv + s ≈ s′, v ≻ s, and v ≻ s′. During the derivation

nv + s ≈ s′ →_{(R_{C}∪E_{C},R_{C}^{K})}^{∗} 0 ≈ 0 ,

all occurrences of v are deleted eventually. This can be done only by (possibly several) γ-rewriting steps. Therefore, R_{C} ∪ E_{C} contains (exactly!) one rule kv + t = t′ ∈ E_{D} for some D ⪯_{C} C. Since nv is deleted completely, n must be equal to k′k where k′ is the number of γ-rewriting steps. The remaining subterms in the equation are smaller than v, so all further reduction steps can use only rules from (R_{D}, R_{D}^{K}). Thus e ∈ E_{D}^{K} ⊆ R_{C}^{K} ∪ E_{C}^{K}.

The second part of the lemma is proved analogously. □

4.3 Confluence

It is easy to see that the relation →_{(R_{C},R_{C}^{K})} is in general not confluent:

Example 4.13 Let N = \overline{N} = \{C\} where C is the clause 2c ≈ d. Then R_{∞} = {2c ≈ d} and R_{∞}^{K} = ∅. Now the equation 2c ≈ c can be rewritten to d ≈ c, using an γ-step, and also to c ≈ 0, using a κ-step. Both equations are irreducible.

We can merely show that →_{(R_{C},R_{C}^{K})} is confluent on tr(R_{C}, R_{C}^{K}), that is, that any two derivations starting from an equation e can be joined, provided that there is a derivation e →^{+} 0 ≈ 0. In fact, this will be sufficient for our purposes.

Theorem 4.14 The relation →_{(R_{C},R_{C}^{K})} is confluent on tr(R_{C}, R_{C}^{K}) for every C ∈ \overline{N}. The relation →_{(R_{∞},R_{∞}^{K})} is confluent on tr(R_{∞}, R_{∞}^{K}).

Proof. Let us consider the relation →_{(R_{C},R_{C}^{K})}. (The case of →_{(R_{∞},R_{∞}^{K})} is similar.) We have to prove that for any two (R_{C}, R_{C}^{K})-derivations e →^{+} 0 ≈ 0 and e →^{+} e′ there exists a derivation e′ →^{∗} 0 ≈ 0. As usual, this is done by analyzing critical pairs and by noetherian induction over the size of e. However, we need the induction hypothesis not only to show that local confluence implies global confluence, but even to prove local confluence (in particular in Case 2 below). Let us consider a peak

[figure: e_{0}; (R_{C},R_{C}^{K}); (R_{C},R_{C}^{K}); e_{1}; e_{2}]

where either e_{1} or e_{2} can be reduced to 0 ≈ 0.

Case 1: Trivial peaks.

As in the traditional term rewriting framework, every peak converges if the two rewrite steps take place at disjoint redexes. Furthermore, local confluence is obvious, if both steps are κ-steps, if both steps are γ-steps (since there is at most one rule that can be applied in an γ-step at some nv), or if there is one δ- and one κ-step. Finally, Lemma 4.11 shows that γ- and δ-steps can only take place at disjoint redexes. It remains thus to consider γ/κ-peaks and δ/δ-peaks.

Case 2: γ/κ-peaks.

Closing a peak between a κ-step and an γ-step is trivial if the latter takes place at some free function symbol. It suffices therefore to consider the situation where a rewrite rule nv + s ≈ s′ ∈ E_{D} ⊆ R_{C} with n ≥ 2 is applied at the top of an equation nv + t ≈ v + t′. This yields a peak

[figure: nv + t ≈ v + t′; γ; ◯^{1}; κ; ◯^{2}; s′ + t ≈ v + s + t′; (n − 1)v + t ≈ t′]

where either s′ + t ≈ v + s + t′ or (n − 1)v + t ≈ t′ can be rewritten to 0 ≈ 0 by (R_{C}, R_{C}^{K}).

Case 2.1: s′ + t ≈ v + s + t′ →^{∗} 0 ≈ 0.

At some step of the (R_{C}, R_{C}^{K})-derivation s′ + t ≈ v + s + t′ →^{∗} 0 ≈ 0 the term v must be eventually deleted. Suppose that the deletion happens by another application of nv + s ≈ s′. Such a step requires the presence of n − 1 further occurrences of v. As these occurrences cannot be derived from s or s′, we may assume without loss of generality that the derivation has the form ◯^{3}-◯^{4}-◯^{5}:

[figure: nv + t ≈ v + t′; γ; ◯^{1}; κ; ◯^{2}; s′ + t ≈ v + s + t′; ∗; ◯^{3}; (n − 1)v + t ≈ t′; ∗; ◯^{8}; s′ + w ≈ v + s + (n − 1)v + w′; γ; ◯^{4}; (n − 1)v + w ≈ (n − 1)v + w′; κ; +; ◯^{9}; s + s′ + w ≈ s′ + s + w′; ∗; ◯^{5}; κ; ∗; ◯^{6}; w ≈ w′; ∗; ◯^{7}; 0 ≈ 0]

On the other hand, we can use κ-steps ◯^{6} to rewrite s + s′ + w ≈ s′ + s + w′ to w ≈ w′. By the induction hypothesis, the peak between ◯^{5} and ◯^{6} can be joined, hence there is a derivation ◯^{7}. As the steps ◯^{3} take place only at t and t′, we can simulate them by ◯^{8}. Finally, the diagram is closed by using n − 1

κ-steps ◯^{9}.

If v is not deleted by another application of nv + s ≈ s′, then it must be deleted by a κ-step. Again, this requires the existence of another occurrence of v, which cannot be derived from s or s′. We may thus assume that the derivation has the form ◯^{10}-◯^{11}-◯^{12}:

[figure: nv + t ≈ v + t′; γ; ◯^{1}; κ; ◯^{2}; s′ + t ≈ v + s + t′; ∗; ◯^{10}; (n − 1)v + t ≈ t′; ∗; ◯^{13}; s′ + w + v ≈ v + s + w′; κ; ◯^{11}; (n − 1)v + w + v ≈ w′; γ; ◯^{14}; s′ + w ≈ s + w′; ∗; ◯^{12}; 0 ≈ 0]

As the steps ◯^{10} take place only at t and t′, we can simulate them by ◯^{13}. Finally, we can close the diagram using γ-rewriting ◯^{14} by nv + s ≈ s′.

Case 2.2: (n − 1)v + t ≈ t′ →^{∗} 0 ≈ 0.

This is proved in nearly the same way as Case 2.1.

Case 3: δ/δ-peaks.

It remains to show that every δ/δ-peak converges. Suppose that the first rewrite step uses a rule from some E_{D} or E_{D}^{K}, and that the second rewrite step uses a rule from some E_{D′} or E_{D′}^{K}, where D ⪰_{C} D′. We have to distinguish two cases: Either the two steps rewrite overlapping parts of a sum, or they take place one below the other.

Case 3.1: Overlaps below a free symbol.

Suppose that there are two rules s[t] ≈ s′ ∈ E_{D} ∪ E_{D}^{K} and t ≈ t′ ∈ E_{D′} ∪ E_{D′}^{K}, such that t occurs in s below a free function symbol. Obviously, D′ must be smaller than D. As all rules from E_{D}^{K} and the maximal terms of rules from E_{D} are δ-irreducible with respect to (R_{D}, R_{D}^{K}), s[t] ≈ s′ must be a rule nv + u[t] ≈ s′ ∈ E_{D} and the peak has the form

[figure: e[nv + u[t]]; δ; ◯^{1}; δ; ◯^{2}; e[nv + u[t′]]; e[s′]]

where nv + u[t] occurs in e below a free function symbol.

Starting from the equation nv + u[t′] ≈ s′ we construct a derivation as follows:

[figure: nv + u[t′] ≈ s′; δ; ∗; ◯^{3}; nv + w + w_{0} ≈ w′ + w_{0}; κ; ∗; ◯^{4}; nv + w ≈ w′; γ; ◯^{5}; s′ + w ≈ w′ + u[t]; δ; ◯^{6}; s′ + w ≈ w′ + u[t′]; δ; ∗; ◯^{7}; w′ + w_{0} + w ≈ w′ + w + w_{0}; κ; ∗; ◯^{8}; 0 ≈ 0]

First we δ-normalize the equation with respect to (R_{D}, R_{D}^{K}) by rewriting u[t′] to w + w_{0} and s′ to w′ + w_{0} ◯^{3}. Then we use κ-steps ◯^{4} to cancel the common part w_{0} (if any) on both sides of the equation. Using an γ-step by nv + u[t] ≈ s′ ◯^{5} and a δ-step by t ≈ t′ ◯^{6} we obtain s′ + w ≈ w′ + u[t′], As the steps ◯^{3} take place only at u[t′] and s′, we can simulate them by ◯^{7}. Finally, we can use κ-rewriting ◯^{8} to reduce the equation to 0 ≈ 0.

By the construction of w and w′ and by Lemma 4.11, the equation nv + w ≈ w′ is δκ-irreducible with respect to (R_{D} ∪ E_{D}, R_{D}^{K}). By Lemma 4.12, it is contained in E_{D}^{K}. Hence we can join the peak between ◯^{1} and ◯^{2} as follows:

[figure: e[nv + u[t]]; δ; ◯^{1}; δ; ◯^{2}; e[nv + u[t′]]; δ; ∗; ◯^{9}; e[s′]; δ; ∗; ◯^{10}; e[nv + w + w_{0}]; δ; ◯^{11}; e[w′ + w_{0}]]

where steps ◯^{9} and ◯^{10} simulate ◯^{3}, and step ◯^{11} uses nv + w ≈ w′.

Case 3.2: Overlaps at the top.

Suppose that two rules u ≈ u′ ∈ E_{D} ∪ E_{D}^{K} and s ≈ s′ ∈ E_{D′} ∪ E_{D′}^{K} are used in δ-steps to rewrite the same redex or overlapping parts of a sum in an equation e. Without loss of generality let D ⪰_{C} D′. If u or s doesn’t have sort S_{CAM}, then D and D′ and thus s ≈ s′ and u ≈ u′ must be identical, so the peak converges trivially. We can therefore assume without loss of generality that u = mnv + r_{0} + r_{1} and s = knv + r_{0} + r_{2}, where E_{D} contains the rule nv + t ≈ t′. Deviating from our standard notational convention we allow k = 0 (if and only if D ≻_{C} D′) so that we can handle the cases D ≻_{C} D′ and D = D′ simultaneously. If D = D′, we assume by symmetry that m ≥ k. The peak has the form

[figure: e[mnv + r_{0} + r_{2} + r_{1}]; δ; ◯^{1}; δ; ◯^{2}; e[(m−k)nv + s′ + r_{1}]; e[u′ + r_{2}]]

As s ≈ s′ and u ≈ u′ are contained in E_{D} ∪ R_{D} ∪ E_{D}^{K} ∪ R_{D}^{K}, there exist (R_{D} ∪ E_{D}, R_{D}^{K})-derivations ◯^{3}-◯^{4} and ◯^{5}-◯^{6} starting with k- or m-fold γ-application of nv + t ≈ t′.

[figure: s′ ≈ knv + r_{0} + r_{2}; γ; ∗; ◯^{3}; mnv + r_{0} + r_{1} ≈ u′; γ; +; ◯^{5}; s′ + kt ≈ kt′ + r_{0} + r_{2}; ∗; ◯^{4}; mt′ + r_{0} + r_{1} ≈ u′ + mt; ∗; ◯^{6}; 0 ≈ 0; 0 ≈ 0]

Consider the two equations s′ + kt ≈ kt′ + r_{0} + r_{2} and mt′ + r_{0} + r_{1} ≈ u′ + mt. If we add the left-hand sides and right-hand sides, respectively, we obtain a new equation that can be rewritten to 0 ≈ 0 using a combination ◯^{7} of ◯^{4}

and ◯^{6}:

[figure: s′ + kt + mt′ + r_{0} + r_{1} ≈ kt′ + r_{0} + r_{2} + u′ + mt; ∗; ◯^{7}; κ; ∗; ◯^{8}; (m−k)t′ + s′ + r_{1} ≈ r_{2} + u′ + (m−k)t; δ; ∗; ◯^{9}; (m−k)t′ + w + w_{0} ≈ w′ + w_{0} + (m−k)t; κ; ∗; ◯^{10}; (m−k)t′ + w ≈ w′ + (m−k)t; ∗; ◯^{11}; 0 ≈ 0]

We will now show how to construct an alternative derivation starting from s′ + kt + mt′ + r_{0} + r_{1} ≈ kt′ + r_{0} + r_{2} + u′ + mt. First we use κ-steps ◯^{8} to cancel kt, kt′ and r_{0} on both sides of the equation. Then the resulting equation is partially δκ-normalized, first by δ-rewriting s′ + r_{1} to w + w_{0} and r_{2} + u′ to w′ + w_{0} ◯^{9}, then by cancelling ◯^{10} the common part w_{0} (if different from 0). Using the induction hypothesis, we see that the peak between ◯^{7} and ◯^{8}-◯^{9}-◯^{10} can be joined, thus there is a derivation ◯^{11} which closes the diagram.

Consider now the equation (m−k)nv + w ≈ w′. Using (m−k)-fold γrewriting by nv + t ≈ t′ and continuing as in ◯^{11}, we obtain a derivation

[figure: (m−k)nv + w ≈ w′; γ; ∗; ◯^{12}; (m−k)t′ + w ≈ w′ + (m−k)t; ∗; ◯^{13}; 0 ≈ 0]

Furthermore, by the construction of w and w′ and by Lemma 4.11, the equation (m−k)nv + w ≈ w′ is δκ-irreducible with respect to (R_{D} ∪ E_{D}, R_{D}^{K}).

By Lemma 4.12, (m−k)nv + w ≈ w′ is contained in R_{D}^{K} ∪ E_{D}^{K} ∪ {0 ≈ 0}. Therefore, we can join the peak between ◯^{1} and ◯^{2} as follows:

[figure: e[mnv + r_{0} + r_{2} + r_{1}]; δ; ◯^{1}; δ; ◯^{2}; e[(m−k)nv + s′ + r_{1}]; δ; ∗; ◯^{14}; e[u′ + r_{2}]; δ; ∗; ◯^{15}; e[(m−k)nv + w + w_{0}]; δ; ∗; ◯^{16}; e[w′ + w_{0}]]

where steps ◯^{14} and ◯^{15} simulate ◯^{9}, and step ◯^{16} uses (m−k)nv + w ≈ w′. □

Corollary 4.15 For every C ∈ \overline{N}, tr(R_{C}, R_{C}^{K}) and tr(R_{∞}, R_{∞}^{K}) are models of the equality axioms.

Proof. We consider only tr(R_{C}, R_{C}^{K}); the proof for tr(R_{∞}, R_{∞}^{K}) is similar. It is obvious that u ≈ u ∈ tr(R_{C}, R_{C}^{K}) for every term u, and that u ≈ v ∈ tr(R_{C}, R_{C}^{K}) implies v ≈ u ∈ tr(R_{C}, R_{C}^{K}). For the transitivity axiom, consider two equations u ≈ v and v ≈ w ∈ tr(R_{C}, R_{C}^{K}).

[figure: u ≈ v; ∗; ◯^{1}; v ≈ w; ∗; ◯^{2}; 0 ≈ 0; 0 ≈ 0]

If u, v and w have sort S_{CAM}, we can combine the derivations ◯^{1} and ◯^{2} and obtain a derivation ◯^{3}:

[figure: u + v ≈ v + w; ∗; ◯^{3}; κ; +; ◯^{4}; u ≈ w; ∗; ◯^{5}; 0 ≈ 0]

On the other hand, we can use κ-steps ◯^{4} to cancel v on both sides of the equation. By Theorem 4.14, there is a derivation ◯^{5}, hence u ≈ w ∈ tr(R_{C}, R_{C}^{K}).

If u, v and w don’t have sort S_{CAM}, the derivations ◯^{1} and ◯^{2} must have the form ◯^{6}-◯^{7} and ◯^{8}-◯^{9}:

[figure: u ≈ v; δ; ∗; ◯^{6}; v ≈ w; δ; ∗; ◯^{8}; s ≈ s; κ; ◯^{7}; t ≈ t; κ; ◯^{9}; 0 ≈ 0; 0 ≈ 0]

As the δ-steps in ◯^{6} and ◯^{8} rewrite each side of the equations separately, we can use the same rules to rewrite v ≈ v ◯^{10} and u ≈ w ◯^{11}.

[figure: v ≈ v; κ; ◯^{12}; δ; ∗; ◯^{10}; u ≈ w; δ; ∗; ◯^{11}; s ≈ t; +; ◯^{13}; 0 ≈ 0]

On the other hand, we can rewrite v ≈ v immediately to 0 ≈ 0 ◯^{12}. By confluence, there is a derivation ◯^{13} and u ≈ w ∈ tr(R_{C}, R_{C}^{K}).

It remains to show that u ≈ v ∈ tr(R_{C}, R_{C}^{K}) entails t[u] ≈ t[v] ∈ tr(R_{C}, R_{C}^{K}). If there is no free symbol in t above u, this is trivial, so let us assume that u occurs in t below a free symbol. Consider the derivation ◯^{1}:

[figure: u ≈ v; ∗; ◯^{1}; δ; ∗; ◯^{2}; w + w_{0} ≈ w′ + w_{0}; κ; ∗; ◯^{3}; w ≈ w′; ∗; ◯^{4}; 0 ≈ 0]

We can δκ-normalize u ≈ v, first by δ-rewriting u to w + w_{0} and v to w′ + w_{0} ◯^{2}, then by cancelling ◯^{3} the common part w_{0}. (If u and v don’t have sort S_{CAM}, ◯^{2} yields w ≈ w′ directly.) According to Theorem 4.14, there exists a derivation ◯^{4}. The equation w ≈ w′ is δκ-irreducible with respect to (R_{C}, R_{C}^{K}), hence it is contained in R_{C}^{K} ∪ {0 ≈ 0} by Lemma 4.12. Without loss of generality we assume w ⪰ w′. This allows us to construct the following derivation:

[figure: t[u] ≈ t[v]; δ; ∗; ◯^{5}; t[w + w_{0}] ≈ t[w′ + w_{0}]; δ; ∗; ◯^{6}; t[w′ + w_{0}] ≈ t[w′ + w_{0}]; κ; +; ◯^{7}; 0 ≈ 0]

where step ◯^{5} simulates ◯^{2} and step ◯^{6} uses w ≈ w′ (if different from 0 ≈ 0). Summarizing we get t[u] ≈ t[v] ∈ tr(R_{C}, R_{C}^{K}). □

Corollary 4.16 For every C ∈ \overline{N}, tr(R_{C}, R_{C}^{K}) and tr(R_{∞}, R_{∞}^{K}) are models of ACUK.

Proof. The cancellation axiom is proved in the same way as the transitivity axiom (Corollary 4.15). The associative, commutative, and identity axioms are obvious. □

4.4 Completeness

Lemma 4.17 Let C be a clause from \overline{N}. If C is true in tr(R_{C}, R_{C}^{K}), then it is also true in tr(R_{∞}, R_{∞}^{K}) and tr(R_{D}, R_{D}^{K}) for any D ≻_{C} C.

Lemma 4.18 Let C = C′ ∨ e be a clause from \overline{N} such that E_{C} = \{e\}. Then C is true and C′ is false in tr(R_{∞}, R_{∞}^{K}) and tr(R_{D}, R_{D}^{K}) for any D ⪰_{C} C.

Lemma 4.19 Let N be a set of clauses that is saturated up to ACUK-redun-dancy and doesn’t contain the empty clause. Then for every ground clause C ∈ \overline{N} we have:

(i) If C is an instance of a clause in N with selected literals, then C is true in tr(R_{C}, R_{C}^{K}).

(ii) If C is redundant, then it is true in tr(R_{C}, R_{C}^{K}).

(iii) E_{C} = ∅ if and only if C is true in tr(R_{C}, R_{C}^{K}).

(iv) C is true in tr(R_{∞}, R_{∞}^{K}) and in tr(R_{D}, R_{D}^{K}) for every D ≻_{C} C.

Proof. We use induction on the clause ordering ≻_{C} and assume that (i)–(iv) are already satisfied for all C′ ∈ \overline{N} with C ≻_{C} C′. Note that the “if” part of (iii) is obvious from the model construction and that condition (iv) follows immediately from (iii), Lemma 4.18, and Lemma 4.17. Let C = Ĉθ for some Ĉ ∈ N.

Case 1: C is redundant.

If C is redundant, then there are clauses C_{1}, …, C_{n} ∈ \overline{N} such that C_{i} ≺_{C} C for every i ∈ {1, …, n} and {C_{1}, …, C_{n}} ⊧ C. By part (iv) of the induction hypothesis, all C_{i} are true in tr(R_{C}, R_{C}^{K}). As tr(R_{C}, R_{C}^{K}) satisfies ACUK, C is true in tr(R_{C}, R_{C}^{K}).

Case 2: xθ equals some smaller term.

Suppose there is a variable x in Ĉ and a ground term w such that xθ ≻ w and xθ ≈ w ∈ tr(R_{C}, R_{C}^{K}). Let the substitution ρ be defined by xρ = w and yρ = yθ for every variable x ≠ y. The clause Ĉρ is smaller than C. By part (iv) of the induction hypothesis, it is true in tr(R_{C}, R_{C}^{K}). As tr(R_{C}, R_{C}^{K}) satisfies the equality axioms, every literal of Ĉθ is true in tr(R_{C}, R_{C}^{K}) if and only if the corresponding literal of Ĉρ is true; hence C is true in tr(R_{C}, R_{C}^{K}).

Case 3: C contains a selected or maximal negative literal.

Suppose that C = C′ ∨ ¬ e doesn’t fall into the preceding two categories and that the literal ¬ e is either an instance of a selected literal in Ĉ or or that Ĉ contains no selected literal and ¬ e is maximal in C. If e ∉ tr(R_{C}, R_{C}^{K}), there is nothing to show, so assume that there is a (R_{C}, R_{C}^{K})-derivation from e to 0 ≈ 0. Let v = mt(e).

Case 3.1: v occurs on both sides of e.

If e equals v ≈ v where v either doesn’t have sort S_{CAM} or equals 0, then there is an equality resolution inference from C = C′ ∨ ¬ e yielding C′. This inference is a ground instance of an equality resolution inference from Ĉ. By saturation up to ACUK-redundancy, it is redundant, hence there are clauses C′_{1}, …, C′_{n} ∈ \overline{N} such that C′_{i} ≺_{C} C and \{C′_{1}, …, C′_{n}\} ⊧ C′. By the induction hypothesis, all C′_{i} and thus C′ and C are true in tr(R_{C}, R_{C}^{K}).

If e equals nv + t ≈ mv + t′ with n ≥ m ≥ 1 then there is a cancellation inference from C = C′ ∨ ¬ e yielding C′ ∨ ¬ (n−m)v + t ≈ t′. This inference is a weak ground instance of a cancellation inference from Ĉ. As above, we deduce that C′ ∨ ¬ (n−m)v + t ≈ t′ and C are true in tr(R_{C}, R_{C}^{K}).

Case 3.2: v occurs on only one side of e.

If v occurs only on one side of e, then e has either the form nv + s ≈ s′ or v ≈ s′ and v doesn’t have sort S_{CAM}. We write e[v] if the distinction between these two cases is irrelevant.^{8} By Lemma 4.9 we may assume that the reduction from e to 0 ≈ 0 starts with an γ- or δ-step at nv or v.

Case 3.2.1: Reduction by R_{C}.

Suppose that the reduction from e to 0 ≈ 0 starts with the application of a rule e′ ∈ E_{D} ⊆ R_{C}, where D = D̂θ = D′ ∨ e′ for some D̂ ∈ N. By part (i)-(iii) of the induction hypothesis and Lemma 4.18, D is not redundant, D̂ has no selected literals, and D′ is false in tr(R_{C}, R_{C}^{K}).

Case 3.2.1.1: Reduction at the top and v has sort S_{CAM}.

If v has sort S_{CAM} and the reduction takes place at the top, then e′ is a rewrite rule mv + t ≈ t′. Consider the cancellative superposition inference

\frac{D′ ∨ mv + t ≈ t′ C′ ∨ ¬ nv + s ≈ s′}{D′ ∨ C′ ∨ ¬ (n−m)v + s + t′ ≈ s′ + t}

If nv + s were equal to xθ for some variable x occurring in Ĉ, then xθ ≈ s′ ∈ tr(R_{C}, R_{C}^{K}), so C would be subject to Case 2 above. By Lemma 3.26 the inference is therefore a ground instance of a cancellative superposition inference from D̂ and Ĉ. As N is saturated, it is redundant, thus its conclusion is true in tr(R_{C}, R_{C}^{K}). Both D′ and ¬ (m−n)v + s + t′ ≈ s′ + t are false in tr(R_{C}, R_{C}^{K}), so C′ and C must be true in tr(R_{C}, R_{C}^{K}).

Case 3.2.1.2: Reduction below a free function symbol or v doesn’t have sort S_{CAM}.

If v does not have sort S_{CAM} or if the reduction takes place below a free function symbol, then e′ is a rewrite rule t ≈ t′ and e = e[v[t]]. If t occurred in e at or below a variable position of Ĉ, say, xθ = w[t], then xθ ≈ w[t′] ∈ tr(R_{C}, R_{C}^{K}), so C would be subject to Case 2 above. Consequently, the standard superposition inference

\frac{D′ ∨ t ≈ t′ C′ ∨ ¬ e[v[t]]}{D′ ∨ C′ ∨ ¬ e[v[t′]]}

is a ground instance of a standard superposition inference from D̂ and Ĉ. Again, by saturation, its conclusion is true in tr(R_{C}, R_{C}^{K}); and since D′ and ¬ e[v[t′]] are false in tr(R_{C}, R_{C}^{K}), both C′ and C must be true.

8Recall that nv is merely an abbreviation for the n-fold sum v + ⋯ + v. If e = nv + s ≈ s′, then the hole in e[ ] is the position of one of the n v’s.

Case 3.2.2: Reduction by R_{C}^{K}.

Suppose that e can be reduced using a rule e′′ = kmu + r ≈ r′ from R_{C}^{K}, but not using a rule from R_{C}. Let D = D̂θ = D′ ∨ e′ such that e′ = mu + s ≈ s′, E_{D} = {e′}, and e′′ ∈ E_{D}^{K}. We may assume that some sum kmu + r + r′′ occurs in v immediately below a free function symbol. As e can’t be reduced using e′, there is no s′′ such that r + r′′ = s + s′′, hence there is an abstraction inference

\frac{D′ ∨ mu + s ≈ s′ C′ ∨ ¬ e[v[kmu + r + r′′]]}{C′ ∨ ¬ y ≈ kmu + r + r′′ ∨ ¬ e[v[y]]}

If kmu + r occurred in e at or below a variable position of Ĉ, then C would be subject to Case 2 above. Hence let Ĉ = Ĉ′ ∨ ¬ ê[v̂[t̂]], where ê[ ]θ = e[ ], v̂[ ]θ = v[ ], and t̂θ = kmu + r + r′′. Assume that t̂ had the form z + ∑_{j∈J} t̂_{j}, where zθ ⪰ mu and all t̂_{j} are atomic terms and are either zero or t̂_{j}θ ≻ zθ. Then zθ could be written as kmu + r + r′′′, since u ≻ r. This is impossible, though, as kmu + r must not occur at or below a variable position. By Lemma 3.26, the inference is therefore a ground instance of an abstraction inference from D̂ and Ĉ. By saturation,

C′ ∨ ¬ r′ + r′′ ≈ kmu + r + r′′ ∨ ¬ e[v[r′ + r′′]]

is true in tr(R_{C}, R_{C}^{K}); and since r′ + r′′ ≈ kmu + r + r′′ ∈ tr(R_{C}, R_{C}^{K}), C must be true likewise.

Case 4: C doesn’t contain a selected or maximal negative literal.

Suppose that C doesn’t fall into one of the cases 1–3. Then C can be written as C′ ∨ e, where e is a maximal literal of C. If E_{C} = {e} or C′ is true in tr(R_{C}, R_{C}^{K}), then there is nothing to show, so assume that E_{C} = ∅ and that C′ is false in tr(R_{C}, R_{C}^{K}). Let v = mt(e).

Case 4.1: v occurs on both sides of e.

Obviously e cannot have the form v ≈ v, since then C would be a tautology and thus redundant. If e equals mv + t ≈ nv + t′ with n ≥ m ≥ 1, then there is a cancellation inference from C. As in case 3.1, we can show that C is true in tr(R_{C}, R_{C}^{K}).

Case 4.2: v occurs on only one side of e.

If v occurs only on one side of e, then either e = nv + s ≈ s′, or e = v ≈ s′ and v doesn’t have sort S_{CAM}.

Case 4.2.1: C′ is true in tr(R_{C} ∪ {e}, R_{C}^{K}).

Suppose that C′ is false in tr(R_{C}, R_{C}^{K}), but true in tr(R_{C} ∪ {e}, R_{C}^{K}). (This includes in particular the case that e is maximal, but not strictly maximal in C.) Then C′ = C′′ ∨ e_{1}, where the literal e_{1} in C′ is not larger than e and has an (R_{C} ∪ {e}, R_{C}^{K})-derivation to 0 ≈ 0 in which e is used. Since the latter condition implies mt_{#}(e_{1}) ⪰ mt_{#}(e), e_{1} must be a rewrite rule and mt_{#}(e_{1}) = mt_{#}(e).

Case 4.2.1.1: v has sort S_{CAM}.

If v has sort S_{CAM}, let e = nv + s ≈ s′ and e_{1} = nv + t ≈ t′. Without loss of generality, the (R_{C} ∪ {e}, R_{C}^{K})-derivation of e_{1} starts with an γ-application of e and has the form

nv + t ≈ t′ → s′ + t ≈ s + t′ →_{(R_{C},R_{C}^{K})}^{∗} 0 ≈ 0

The cancellative equality factoring inference

\frac{C′′ ∨ nv + s ≈ s′ ∨ nv + t ≈ t′}{C′′ ∨ ¬ s + t′ ≈ s′ + t ∨ nv + t ≈ t′}

is a ground instance of a cancellative equality factoring inference from Ĉ. By saturation, its conclusion is true in tr(R_{C}, R_{C}^{K}). As s + t′ ≈ s′ + t ∈ tr(R_{C}, R_{C}^{K}), C′′ ∨ s′ + t ∨ nv + t ≈ t′ and thus C must be true in tr(R_{C}, R_{C}^{K}).

Case 4.2.1.2: v doesn’t have sort S_{CAM}.

If v doesn’t have sort S_{CAM}, then let e = v ≈ s′ and e_{1} = v ≈ t′. Analogously to case 4.2.1.1 we can show that the conclusion of the standard equality factoring inference

\frac{C′′ ∨ v ≈ s′ ∨ v ≈ t′}{C′′ ∨ ¬ s′ ≈ t′ ∨ v ≈ t′}

is true in tr(R_{C}, R_{C}^{K}) and that s′ ≈ t′ ∈ tr(R_{C}, R_{C}^{K}). Again, C must be true in tr(R_{C}, R_{C}^{K}).

Case 4.2.2: C′ is false in tr(R_{C} ∪ {e}, R_{C}^{K}).

So far we have considered the cases that C is not reductive for e, or that C is true in tr(R_{C}, R_{C}^{K}), or that C′ is true in tr(R_{C} ∪ {e}, R_{C}^{K}). If none of these conditions applies but E_{C} is empty, then mt_{#}(e) must be reducible with respect to (R_{C}, R_{C}^{K}). We can then show that C is true in tr(R_{C}, R_{C}^{K}), using essentially the same techniques as in case 3.2. This concludes the proof of this lemma. □

Theorem 4.20 Let N be a set of clauses that is saturated up to ACUKredundancy. Then N ∪ ACUK is equality unsatisfiable if and only if N contains the empty clause.

Proof. If N contains the empty clause, then it is unsatisfiable. Otherwise, tr(R_{∞}, R_{∞}^{K}) is a model of the equality axioms (by Corollary 4.15), of ACUK (by Corollary 4.16), and of N (by part (iv) of Lemma 4.19). □

5 Simplification Techniques

Let N be a set of clauses. We say that M ⊆ N is simplified to another set of clauses M′, if N ⊧ M′ (so that we may add M′, once we have got N), and if M is ACUK-redundant with respect to N ∪ M′ (so that we may delete M, once we have added M′).

For example, every clause

C_{1} = C ∨ [¬] s + t ≈ s + t′

can be simplified to

C_{0} = C ∨ [¬] t ≈ t′

(independently of N). We can also extend the classical simplification by demodulation to cancellative superposition, so that a clause

C_{1} = C ∨ C′ ∨ [¬] s + t ≈ t′

can be simplified to

C_{0} = C ∨ C′ ∨ [¬] w′ + t ≈ t′ + w

provided that N contains a clause D such that

Dσ = C′ ∨ s + w ≈ w′

where s ≻_{x} w, s ≻_{x} w′, and C_{1} ≻_{C} Dσ. For instance, every inference in Example 3.13 is a simplification of the maximal premise. In particular, this technique can in nearly all cases be used to eliminate any remaining occurrences of the redex in the conclusion of a cancellative superposition inference.

Bachmair and Ganzinger [4] list a number of general simplification techniques such as case analysis or contextual rewriting. These methods can easily be extended to our framework. In this section, we will concentrate on techniques that help to reduce the number of clauses with eligible variables.

Whereas the ordering conditions of our inference rules make cancellative superposition inferences into shielded variables superfluous, cancellative superposition inferences into unshielded variables cannot generally be avoided. As an example, consider the clauses b + c ≈ d and x + c ≉ d with the ordering b ≻ c ≻ d. Since unification is not an effective filter, clauses with eligible variables are extremely prolific. Simplification techniques offer the possibility to remove certain clauses with eligible variables from the clause set, or at least to render inferences with them redundant.

Lemma 5.1 Let C ∈ N be a clause

⋁_{i∈I} n_{i}x + s_{i} ≈ t_{i}

where x occurs in neither of the t_{i}. Then every model of ACK ∪ N can be extended to a model of x + 0 ≈ x and x + (−x) ≈ 0, where 0 and − are new function symbols.

Proof. Let θ be a substitution that maps all variables in C except x to constants. Let M be an arbitrary model of ACK ∪ N, where M_{CAM} is the carrier set of the sort S_{CAM}. Then t_{i} corresponds to a constant in M_{CAM} and (n_{i}−1)x + s_{i} to a (possibly constant) function from M_{CAM} to M_{CAM}. By Lemma 2.2, M_{CAM} is a group. Hence we can interpret 0 and − appropriately in M so that M becomes a model of x + 0 ≈ x and x + (−x) ≈ 0. □

Lemma 5.2 Let C be a clause

C′ ∨ ⋁_{i∈I} n_{i}x + s_{i} ≈ t_{i}

where x occurs neither in C′ nor in the t_{i}. Let N be a set of clauses and 0 and − be new function symbols. Then every model of {C} ∪ ACK is either a model of C′ or it can be extended to a model of x + 0 ≈ x and x + (−x) ≈ 0. In particular, N ∪ {C} ∪ ACK is satisfiable if and only if N ∪ {C′} ∪ ACK or N ∪ {C} ∪ {x + (−x) ≈ 0} ∪ ACUK is.

Proof. Suppose that there is a model M of {C} ∪ ACK that is not a model of C′. Let θ be a substitution with domain Var(C′) such that the ground clause C′θ is false in M. Consequently,

⋁_{i∈I} n_{i}x + s_{i}θ ≈ t_{i}θ

must be true in M. By Lemma 5.1, M can be extended to a model of x + 0 ≈ x and x + (−x) ≈ 0. □

In its most general form, we can use this lemma to split one theorem proving derivation into two branches in a tableaux-like manner (cf. [5]). It is particularly useful if one of the two branches can immediately be seen to fail. This happens in two situations: First, if C′ is empty, the first branch can be closed immediately. In this case C implies the identity and inverse axioms, and, although it not required by fairness, it may be wise to add them to find an easier proof.^{9} Second, if N contains some subset N′ that implies that S_{CAM} is not a group, the second branch can be closed immediately. (For instance, N′ might consist of the single clause y + a ≉ b.) In this case, C can be simplified to C′. In “non-groups” it is thus always possible to get rid of unshielded variables that occur only positively.

Unshielded variables occurring negatively are somewhat harder to handle. There is a variant of “rewriting with equations of conditions” which can sometimes be applied if an unshielded variable occurs in two different literals. A clause

C_{1} = C ∨ ¬ mx + s ≈ s′ ∨ [¬] nx + t ≈ t′

with n ≥ m ≥ 1 is equivalent to

C_{0} = C ∨ ¬ mx + s ≈ s′ ∨ [¬] (n−m)x + t + s′ ≈ t′ + s .

Repeated use of this inference leads to a clause in which x occurs only in one negative literal kx + w ≈ w′ and possibly in some positive literals (with coefficients smaller than k). Unfortunately, this is not a simplification for all instances of C_{1}θ, but just for those that satisfy xθ ≻_{x} sθ and xθ ≻_{x} s′θ.^{10} Hence adding C_{0} makes it unnecessary to consider inferences with C_{1} that involve only x but no subterm of s or s′. Inferences that involve both x and a subterm of s or s′ are still necessary, though.

If an unshielded variable occurs only in one negative literal (and no positive one), we can eliminate it, provided that the inverse axiom has been derived and that the coefficient of the variable is 1. In a group, every clause of the form

C ∨ ¬ x + s ≈ s′ ,

where x doesn’t occur in C, can be simplified to C.

What can be done to eliminate unshielded variables that occur negatively with a coefficient k larger than 1, and possibly also positively with coefficients smaller than k? A clause like 2x ≉ a is true in some groups and some nongroups (take the integers or the naturals and a = 1), and false in others. To remove such a literal, additional properties of the model class are required, namely, that for every k ∈ N^{+} and u there is a v such that kv ≈ u.

9The reader might try to refute ACUK ∪ { 2x ≈ a ∨ x ≈ b, 2b ≉ a } without first deducing the inverse axiom.

10It is not possible to weaken this condition to xθ ⊀_{x} sθ and xθ ⊀_{x} s′θ. For instance, if C_{1} is the clause 2x + 4b ≉ c ∨ 3x ≉ d and b ≻ c ≻ d, then C_{0} is 2x + 4b ≉ c ∨ x + c ≉ d + 4b, and C_{0}θ is larger than C_{1}θ if θ maps x to b.

If a clause has the form

C ∨ ¬ kx + s ≈ s′ ∨ nx + t ≈ t′

with n < k, then it is possible to derive

C ∨ ¬ kx + s ≈ s′ ∨ kt + ns′ ≈ kt′ + ns .

In general, this is not a simplification, since the second clause does not imply the first one. To show the equivalence of the two clauses, one needs that ky ≈ kz implies y ≈ z. This property does not hold in Z/4, for instance. On the other hand, it does hold in totally ordered cancellative abelian monoids, if the ordering is compatible with addition. It is still to be investigated to which degree we can exploit this.

6 Conclusions

We have presented a calculus for first-order equational theorem proving in the presence of the axioms of cancellative abelian monoids. The calculus is refutationally complete without requiring extended clauses or explicit inferences with the theory clauses. Compared with the conventional superposition calculus, on which it is based, the ordering constraints are strengthened in such a way that we may not only restrict to inferences that involve the maximal side of the maximal literal, but even to inferences that involve the maximal atomic terms. The calculus may further be furnished with selection functions.

In traditional AC-superposition, extended rules show a rather prolific behaviour. In our approach, AC-unification is replaced by ACU-unification. Furthermore, cancellative superposition makes extended rules superfluous, and the ordering constraints mentioned above allow to exclude inferences involving shielded variables altogether. Many occurrences of unshielded variables can be eliminated by appropriate simplification techniques. Unfortunately cancellative superpositions into variables in sums cannot be completely avoided. More ways to eliminate unshielded variables are possible in the presence of further algebraic structure. This is still a matter of further investigation.

At the time of writing this paper, we cannot yet report about practical experiences with our calculus. An implementation in the Saturate system [13] is under way.

References

[1] Jürgen Avenhaus and Klaus Becker. Conditional rewriting modulo a builtin algebra. SEKI Report SR-92-11, Fachbereich Informatik, Universität Kaiserslautern, 1992.

[2] Leo Bachmair and Harald Ganzinger. Associative-commutative superposition. In Nachum Dershowitz and Naomi Lindenstrauss, editors, Conditional and Typed Rewrite Systems, 4th International Workshop, CTRS-94, LNCS 968, pages 1–14, Jerusalem, Israel, July 13–15, 1994. Springer-Verlag.

[3] Leo Bachmair and Harald Ganzinger. Ordered chaining for total orderings. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, LNAI 814, pages 435–450, Nancy, France, June 26–July 1, 1994. Springer-Verlag.

[4] Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

[5] Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, LNCS 713, pages 83–96, Brno, Czech Republic, August 24–27, 1993. Springer-Verlag.

[6] Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing, 5(3/4):193–212, April 1994.

[7] Leo Bachmair and David A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1:329–349, 1985.

[8] W. W. Bledsoe, K. Kunen, and R. Shostak. Completeness results for inequality provers. Artificial Intelligence, 27:255–288, 1985.

[9] R[obert] S. Boyer and J S[trother] Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In Jean E. Hayes, Donald Michie, and Judith Richards, editors, Machine Intelligence 11: Logic and the acquisition of knowledge, chapter 5, pages 83–124. Oxford University Press, 1988.

[10] Hans-Jürgen Bürckert. A resolution principle for clauses with constraints. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, LNAI 449, pages 178–192, Kaiserslautern, FRG, July 24–27, 1990. Springer-Verlag.

[11] Hans-Jürgen Bürckert. A Resolution Principle for a Logic with Restricted Quantifiers. LNAI 568. Springer-Verlag, Berlin, Heidelberg, New York, 1991.

[12] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6, pages 243–320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo, 1990.

[13] Harald Ganzinger. The Saturate system. Available on the world-wide web under URL http://www.mpi-sb.mpg.de/SATURATE/Saturate.html, 1994.

[14] Alexander Herold and Jörg H. Siekmann. Unification in Abelian semigroups. Journal of Automated Reasoning, 3(3):247–283, 1987.

[15] Larry M. Hines. Completeness of a prover for dense linear logics. Journal of Automated Reasoning, 8:45–75, 1992.

[16] Larry M. Hines. Str ˙+ve and integers. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, LNAI 814, pages 416– 430, Nancy, France, June 26–July 1, 1994. Springer-Verlag.

[17] Jieh Hsiang, Michaël Rusinowitch, and Ko Sakai. Complete inference rules for the cancellation laws (extended abstract). In John McDermott, editor, Proceedings of the Tenth International Joint Conference on Artificial Intelligence, volume 2, pages 990–992, Milan, Italy, August 23–28 1987. Morgan Kaufmann Publishers, Inc.

[18] Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104(1):29–51, October 1992.

[19] Claude Kirchner, Hélène Kirchner, and Michaël Rusinowitch. Deduction with symbolic constraints. Revue Française d’Intelligence Artificielle, 4(3):9–52, 1990. Special issue on automatic deduction.

[20] Claude Marché. Normalised narrowing and normalised completion. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 394–403, Paris, France, July 4–7, 1994. IEEE Computer Society Press, Los Alamitos, CA, USA.

[21] Robert Nieuwenhuis and Albert Rubio. AC-superposition with constraints: no AC-unifiers needed. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, LNAI 814, pages 545–559, Nancy, France, June 26–July 1, 1994. Springer-Verlag.

[22] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, LNAI 607, pages 748–752, Saratoga Springs, New York, USA, June 15–18, 1992. Springer-Verlag.

[23] Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233–264, April 1981.

[24] M. M. Richter. Some reordering properties for inequality proof trees. In E. Börger, G. Hasenjäger, and D. Rödding, editors, Logic and Machines: Decision Problems and Complexity, LNCS 171, pages 183–197. Springer-Verlag, 1984.

[25] Albert Rubio and Robert Nieuwenhuis. A precedence-based total ACcompatible ordering. In Claude Kirchner, editor, Rewriting Techniques and Applications, 5th International Conference, RTA-93, LNCS 690, pages 374–388, Montreal, Canada, June 16–18, 1993. Springer-Verlag.

[26] Michaël Rusinowitch. Démonstration Automatique: Techniques de Réécriture, chapitre 7: Ensembles complets de règles d’inférence pour les axiomes de régularité, pages 111–127. InterEditions, Paris, 1989.

[27] Jürgen Stuber. Superposition theorem proving for integer modules. To be submitted, 1996.

[28] Laurent Vigneron. Associative-commutative deduction with constraints. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, LNAI 814, pages 530–544, Nancy, France, June 26–July 1, 1994. Springer-Verlag.

[29] Ulrich Wertz. First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max-Planck-Institut für Informatik, Saarbrücken, Germany, April 1992.

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

Below you find a list of the most recent technical reports of the research group Logic of Programming at the Max-Planck-Institut für Informatik. They are available by anonymous ftp from our ftp server ftp.mpi-sb.mpg.de under the directory pub/papers/reports. Most of the reports are also accessible via WWW using the URL http://www.mpi-sb.mpg.de. If you have any questions concerning ftp or WWW access, please contact reports@mpi-sb.mpg.de. Paper copies (which are not necessarily free of charge) can be ordered either by regular mail or by e-mail at the address below.

Max-Planck-Institut für Informatik Library attn. Birgit Hofmann Im Stadtwald D-66123 Saarbrücken GERMANY

e-mail: library@mpi-sb.mpg.de

MPI-I-96-2-001 H. Ganzinger, U. Waldmann  Theorem Proving in Cancellative Abelian Monoids

MPI-I-95-2-011 P. Barth, A. Bockmayr Modelling Mixed-Integer Optimisation Problems in Constraint Logic Programming

MPI-I-95-2-010 D. A. Plaisted Special Cases and Substitutes for Rigid E-Unification

MPI-I-95-2-009 L. Bachmair, H. Ganzinger Ordered Chaining Calculi for First-Order Theories of Binary Relations

MPI-I-95-2-008 H. J. Ohlbach, R. A.Schmidt, U. Hustadt

Translating Graded Modalities into Predicate Logic

MPI-I-95-2-007 A. Nonnengart, A. Szalas A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory

MPI-I-95-2-006 D. Basin, H. Ganzinger Automated Complexity Analysis Based on Ordered Resolution

MPI-I-95-2-005 F. Baader, H. J. Ohlbach A Multi-Dimensional Terminological Knowledge Representation Language

MPI-I-95-2-003 P. Barth A Davis-Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization

MPI-I-95-2-002 H. J. Ohlbach, R. A. Schmidt Functional Translation and Second-Order Frame Properties of Modal Logics

MPI-I-95-2-001 S. Vorobyov Proof normalization and subject reduction in extensions of Fsub

MPI-I-94-261 P. Barth, A. Bockmayr Finite Domain and Cutting Plane Techniques in CLP(PB)

MPI-I-94-257 S. Vorobyov Structural Decidable Extensions of Bounded Quantification

MPI-I-94-254  P. Madden  Report and abstract not published

MPI-I-94-252 P. Madden A Survey of Program Transformation With Special Reference to Unfold/Fold Style Program Development

MPI-I-94-251  P. Graf  Substitution Tree Indexing

MPI-I-94-246 M. Hanus On Extra Variables in (Equational) Logic Programming