Elimination of Equality via Transformation with Ordering

Constraints

Leo Bachmair Harald Ganzinger Andrei Voronkov

MPI–I–97–2–012 December 1997

Authors’ Addresses

Leo Bachmair Department of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794, U.S.A.

email: leo@cs.sunysb.edu, web: www.cs.sunysb.edu/~leo

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

email: hg@mpi-sb.mpg.de, web: www.mpi-sb.mpg.de/~hg

Andrei Voronkov Computing Science Department, Uppsala University, Box 311, S 751 05 Uppsala, Sweden

email: voronkov@csd.uu.se, web: www.csd.uu.se/~voronkov

Publication Notes

A shorter version of this report has been submitted for publication elsewhere.

Acknowledgements

This research was supported in part by the National Science Foundation under grants INT-9314412 and CCR-9510072, by the German Science Foundation (Deutsche Forschungsgemeinschaft) under grants Ga 261/7-1 and Ga 261/8-1, and by the ESPRIT Basic Research Working Group 22457 (Construction of Computational Logics II).

Abstract

We refine Brand’s method for eliminating equality axioms by (i) imposing ordering constraints on auxiliary variables introduced during the transformation process and (ii) avoiding certain transformations of positive equations with a variable on the right-hand side. The refinements are both of theoretical and practical interest. For instance, the second refinement is implemented in Setheo and appears to be critical for that prover’s performance on equational problems. The correctness of this variant of Brand’s method was an open problem that is solved by the more general results in the present paper. The experimental results we obtained from a prototype implementation of our proposed method for the model elimination prover Protein also show some dramatic improvements of the proof search. Ordering constraints have already been widely used in equational theorem provers based on paramodulation. We prove the correctness of our refinements of Brand’s method by establishing a suitable connection to basic paramodulation calculi and thereby shed new light on the connection between different approaches to equational theorem proving.

Keywords

Automated Theorem Proving, Equality Handling, Ordering Constraints, Model Elimination

Contents

1 Introduction 1 2 Preliminaries 2 3 Transformations 3

3.1 Elimination of Monotonicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3.2 Partial Elimination of Reflexivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.3 Elimination of Symmetry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.4 Elimination of Transitivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

4 Preservation of Satisfiablity 6 5 Variations 12 6 Experiments 13 7 Conclusions 15 A Basic Superposition 17

1 Introduction

Efficient techniques for handling equality are a key component of automated reasoning systems. The most successful approaches to date are based on refinements of paramodulation, such as the superposition calculus, but these are unfortunately not fully compatible with tableau-based provers or model elimination methods. Various attempts have been made recently to improve the handling of equality in such provers (Moser, Lynch & Steinbach 1995, Degtyarev & Voronkov 1996b, Degtyarev & Voronkov 1996a), but they usually require subtle interactions between paramodulation-based and model elimination-based subcomponents and therefore are difficult to integrate into existing provers. Most current model elimination provers rely instead on preprocessing steps that transform formulas from logic with equality into logic without equality, see the survey (Schumann 1994).

The best-known transformation method is Brand’s modification method (Brand 1975), which consists of three steps. First, terms are flattened by introducing new auxiliary variables, so that only variables occur as arguments of functions symbols. The axioms expressing the monotonicity properties of equality are not needed for the resulting flat clauses. Second, all symmetric variants of a clause (which are obtained by switching the arguments of equations) are added to the given set of clauses, so that the symmetry axioms of equality may be dispensed with. Third, the transitivity axioms are internalized by splitting positive equations s≈t into (clauses that represent) implications t ≈ x → s ≈ x with a new auxiliary variable x, called a “link” variable.

In this article, we improve Brand’s modification in various ways. We systematically add ordering constraints during the transformation process, so as to be able to better control the theorem proving process on the transformed clauses. For example, a link variable x will be constrained via s ≻ x and t ⪰ x to terms smaller than s and smaller than or equal to t. Ordering constraints intuitively reflect assumptions about the form of equational proofs of s≈t and are related to rewrite techniques as used in paramodulation and superposition calculi. The rationale for transitivity elimination is that a sequence of equational replacements

s = s_{0} ≈ s_{1} ≈ … ≈ s_{n} = t

(using equations s_{i} ≈ s_{i+1}) can be simulated by a sequence of resolution inferences from the goal clause s ≉ z ∨ t ≉ z and (clauses representing the) equivalences s_{i} ≈ x_{i} ↔ s_{i+1} ≈ x_{i}, plus a final resolution step with the reflexivity axiom x ≈ x that instantiates the link variables. The ordering constraints ensure that the variables x_{i} can only be instantiated by minimal terms among the s_{i} and block the search for alternative equational proofs that apply the same equations but differ in the instantiation of the link variables.

Aside from the ordering constraints, we also propose more subtle changes to the transformation process. In particular, we never split a positive equation t ≈ x where the right-hand side is already a variable. This may seem to be a minor technical aspect, but the optimization (Moser & Steinbach 1997) has been implemented in the Setheo model elimination theorem prover and is crucial for that prover’s successful performance on many equational problems (Ibens & Letz 1997).^{1} The completeness of this optimization (without any ordering constraints) had been an open problem^{2} that follows from the more general results in the present paper. Our completeness proof is comparatively simple, but draws on rather non-trivial results about basic superposition, some of which have been obtained only very recently (Bachmair & Ganzinger 1997b). In essence, we show how refutational proofs by strict basic superposition with flat clauses can be simulated by resolution with the corresponding transformed clauses. In addition to the theoretical results, we also report on experiments with model elimination theorem proving that provide encouraging evidence for the practical usefulness of the proposed constrained equality elimination method.

1The optimized transformation avoids the generation of negative equations x ≉ y between two variables. Model elimination or resolution inferences with such literals correspond to paramodulation inferences into or from variables, most of which are redundant and ought to be avoided.

2The proof in (Moser & Steinbach 1997) contains a non-trivial gap which this paper closes.

The structure of the paper is as follows. The next section contains preliminary material. The transformations are described in Section 3 and the main results about them in Section 4. In Section 5 we discuss the connection with other transformation methods, while in Section 6 we report on experiments with our method.

2 Preliminaries

The transformations described below will be applied to clauses with equality. We use the the symbol ≈ to denote the equality predicate and assume, for simplicity, that this is the only predicate in the original language.^{3} A different symbol ≃ is used to denote the predicate that replaces equality as part of the transformation process. Semantically, the difference between the two symbols is that ≈ is interpreted as a congruence relation, whereas no restrictions are imposed on the interpretation of ≃. In other words, the original formulas with ≈ are interpreted in a logic with equality, whereas the transformed formulas with ≃ are interpreted in a logic without equality. The aim is to design transformations so that the original clause set is satisfiable in an equality interpretation if, and only if, the transformed clause set is satisfiable in general.

Formally, a clause is a disjunction of literals; a literal being either an atomic formula or the negation thereof. Disjunction is associative and commutative, and hence clauses may be viewed as multisets of literals. The empty clause is denoted by □. By an equational clause we mean a clause that contains only ≈, but not ≃. Satisfiability and logical consequence (denoted by ⊧) are defined in the usual way, with the proviso that the interpretation of ≈ has to be a congruence (while ≃ may be interpreted as an arbitrary binary relation).^{4}

Substitutions will be denoted by the letters σ, τ and ρ. The result of applying a substitution σ to an expression (e.g., a clause or term) E is denoted Eσ. We write E[s] to indicate that s is a subterm of E and write E[t] to denote the expression obtained from E by replacing one specified occurrence of s by t. We also write E(s) to indicate that s occurs in E and denote by E(t) the result of simultaneously replacing all occurrences of s in E by t.

A constraint is a, possibly empty, conjunction of atomic formulas s = t (called an atomic equality constraint) or s ≻ t or s ⪰ t (called atomic ordering constraints). The empty conjunction is denoted by ⊤. The letters γ and δ are used to denote constraints. A constrained clause is a pair of a clause C and a constraint γ, written as C · γ. We call C the clause part and γ the constraint part of C · γ.

A substitution σ is said to be a solution of an atomic equality constraint s = t if sσ and tσ are syntactically identical. It is a solution of an atomic ordering constraint s ≻ t (with respect to a reduction ordering > that is total on ground terms) if sσ > tσ; and a solution of s ⪰ t if it is a solution of s = t or s ≻ t. Finally, we say that σ is a solution of a general constraint γ if it is a solution of all atomic constraints in γ. A constraint is satisfiable if it has a solution.

A ground instance of a constrained clause C ·γ is any ground clause Cσ such that the constraint γσ is satisfiable. A constrained clause C is more general than a constrained clause D, denoted D ⊆ C, if every ground instance of D is also a ground instance of C. We call two constrained clauses C and D equivalent if C ⊆ D and D ⊆ C, i.e. when C and D have the same ground instances. A variable renaming is a (not necessarily injective) subsitution mapping variables to variables. Two syntactic expressions E and E′ are said to have the same skeleton written E ≡ E′ whenever E′ρ = Eρ, for some renaming ρ.

3The extension of the various transformation steps to non-equality literals is straightforward.

4On one or two occasions we will explicitly relax the restriction on the interpretation of ≈.

Constraints γ_{1} and γ_{2} are equivalent with respect to a set V of variables if for every solution σ_{1} of γ_{1} there exists a solution σ_{2} of γ_{2} such that σ_{1} and σ_{2} agree on the variables in V, and vice versa. We shall identify constrained clauses C · γ_{1} and C · γ_{2} when the constraints γ_{1} and γ_{2} are equivalent with respect to the variables in C. In this case C · γ_{1} and C · γ_{2} are equivalent. We identify a constrained clause C · ⊤ with the unconstrained clause C. A contradiction is a constrained clause □ · γ with an empty clause part such that the constraint γ is satisfiable. A clause is called void if its constraint is unsatisfiable. A void clause has no ground instances and therefore is redundant.

A set S of constrained clauses is satisfiable if the set of all its ground instances is satisfiable. Evidently, removal of void clauses and replacement of clauses by equivalent ones preserves the (un)satisfiability of S.

If I is an inference system and N is a set of clauses then I(N) denotes the set of clauses that can be derived by applying an inference rule in I to premises in N. Likewise, I^{∗}(N) denotes the set of clauses that can be derived from N by repeated application of inferences in I. In all calculi of this paper the premises of inference rules are assumed to have disjoint variables, which can be achieved by renaming.

3 Transformations

Given a set of equational clauses N, we apply various transformation rules and replace the equality predicate ≈ by the predicate ≃ to obtain a modified clause set N′, such that the transformed set N′ is satisfiable if, and only if, the original set N is equationally satisfiable. Each part of the transformation process is designed to eliminate certain equality axioms and can be described by a set of (schematic) transformation rules to be applied to clauses. If R is a set of such transformation rules, we say that a (constrained) clause is in R-normal form if no rule in R can be applied to it. Most of the transformations described below define normal forms that are unique up to renaming of variables. If N is a set of (constrained) clauses, we denote by R(N) the set of all R-normal forms of clauses in N.

3.1 Elimination of Monotonicity

A clause is said to be flat if variables are the only proper subterms of terms. Thus, f(x)≉y ∨ h(x)≈a is flat, but f(f(x)) ≈ x and f(a) ≈ x are not. A constrained clause C · γ is called flat if its clause part C is flat (but the constraint part γ may contain non-flat terms).

It is fairly straightforward to flatten clauses by abstracting subterms via introduction of new variables. This can be described by a set M of (schematic) transformation rules

C(s) · γ ⇒ (s ≉ x ∨ C(x)) · γ

where x is a variable not occurring in C and s is a non-variable term that occurs at least once as an argument of a function symbol in C. The rules in M are called subterm abstraction rules.

For example, the unit clause i(x) ∗ x ≈ e contains one nested non-variable subterm, namely i(x). Subterm abstraction yields a clause i(x) ≉ z ∨ z ∗ x ≈ e that is unique up to renaming of the new variable z. The unit clause i(x) ∗ i(x) ≈ i(x ∗ x) contains two nested non-variable terms, i(x) and x ∗ x, which are eliminated in two steps to yield a transformed clause

x ∗ x ≉ x_{1} ∨ i(x) ≉ x_{2} ∨ x_{2} ∗ x_{2} ≈ i(x_{1}).

A (constrained) clause is flat if, and only if, it is in M-normal form. The M-normal forms of a clause are unique up to renaming of the newly introduced variables (and hence we will speak of the M-normal form). Our interest in flat clauses stems from the following result:

Proposition 3.1 (Brand 1975) Let N be a set of equational clauses and N′ be obtained from N by replacing each clause by its M-normal form. Then N has an equality model if, and only if, N′ has a model in which the predicate ≈ is interpreted as an equivalence (but not necessarily a congruence) relation.

In other words, the monotonicity axioms are not needed for testing satisfiability of flat equational clauses.

Note. We need not abstract all occurrences of a subterm at once. For instance, the multiple occurrences of the nested term g(x) in

f(g(x)) ≉ h(x) ∨ h(g(x)) ≈ x

are eliminated all at once to yield the M-normal form

g(x) ≉ z ∨ f(z) ≉ h(x) ∨ h(z) ≈ x.

We may instead abstract the different occurrences separately to obtain a different flat clause,

g(x) ≉ z_{1} ∨ g(x) ≉ z_{2} ∨ f(z_{1}) ≉ h(x) ∨ h(z_{2}) ≈ x.

3.2 Partial Elimination of Reflexivity

We may use equality constraints to get rid of certain undesirable negative equality literals:

(x ≉ y ∨ C) · γ ⇒ C · (γ ∧ x = y)

where x and y are variables. This transformation is called reflexivity resolution as it represents an instance of resolution with the reflexivity axiom. We denote the corresponding set of transformation rules by R.

3.3 Elimination of Symmetry

Next we replace the equality predicate ≈ by the predicate ≃ and eliminate the need for the symmetry axioms. Positive equality literals are eliminated by positive symmetry elimination rules:

\begin{aligned}(C ∨ s ≈ t) · γ & ⇒ & (C ∨ s ≃ t) · γ \\ (C ∨ s ≈ t) · γ & ⇒ & (C ∨ t ≃ s) · γ \end{aligned}

If a clause C contains n positive equality literals, then clearly n transformation steps will eliminate all positive occurrences of equality. There are 2^{n} different normal forms, all of which need to be retained to eliminate symmetry. For example, from the clause

g(x) ≉ z ∨ f(z) ≉ h(x) ∨ h(z) ≈ x

we obtain both

g(x) ≉ z ∨ f(z) ≉ h(x) ∨ h(z) ≃ x

and

g(x) ≉ z ∨ f(z) ≉ h(x) ∨ x ≃ h(z).

Negative occurrences of ≈ can in principle be simply replaced by ≃, but we prefer a slightly refined transformation that moves variables to the right-hand side.^{5} The following negative symmetry elimination rules achieve this purpose:

(s ≉ t ∨ C) · γ ⇒ (s ≄ t ∨ C) · γ  if s is not a variable
(s ≉ t ∨ C) · γ ⇒ (t ≄ s ∨ C) · γ  if s is a variable, but t is not

The normal forms produced by these additional transformation rules are unique, as at most one rule can be applied to any negative equality literal.^{6}

We denote by S the set of all positive and negative symmetry elimination rules. If a clause contains n positive equality literals, then 2^{n} different S-normal forms can be derived from it. Two S-normal forms that can be derived from the same clause are said to be symmetric variants of each other.

3.4 Elimination of Transitivity

The transitivity axioms are eliminated by splitting positive and negative equality literals via introduction of so-called “link variables.” The idea is the same as in Brand’s method, but we also introduce constraints on variables, which necessitates slightly different transformations from Brand’s, as will be explained below.

We have both positive and negative splitting rules of the form:

\begin{aligned}(C ∨ s ≃ t) · γ & ⇒ & (C ∨ t ≄ z ∨ s ≃ z) · (γ ∧ t ⪰ z ∧ s ≻ z) \\ (C ∨ s ≄ t) · γ & ⇒ & (C ∨ t ≄ z ∨ s ≄ z) · (γ ∧ t ⪰ z ∧ s ⪰ z) \end{aligned}

where t is not a variable and z is a variable not occurring in C, s or t. The variable z is called a link variable (between s and t) and the corresponding constraints are called link constraints.

We emphasize that equality literals are not split if the right-hand side is already a variable. This is different from Brand’s method, where literals are split regardless of whether the right-hand side is a variable or not.

We do not split equality literals with a variable on the right-hand side, but still may add corresponding ordering constraints, as expressed by the following positive and negative link constraint rules:

\begin{aligned}(C ∨ s ≃ x) · γ & ⇒ & (C ∨ s ≃ x) · (γ ∧ s ≻ x) \\ (C ∨ s ≄ x) · γ & ⇒ & (C ∨ s ≄ x) · (γ ∧ s ⪰ x) \end{aligned}

where the constraints s ≻ x and s ⪰ x, respectively, must not be contained in γ already.^{7}

By T we denote the set of all splitting and link constraint rules. The T-normal form of a clause is unique up to renaming of link variables.

The flat clause (with empty constraint)

i(x) ≄ x_{1} ∨ x_{1} ∗ x ≃ e

5The advantage is that fewer splitting rules (described below) will be applicable.

6Negative literals x ≉ y, with variables x and y, are not eliminated by symmetry elimination, but by reflexivity resolution.

7There is no point in introducing the same constraint repeatedly.

is transformed by T to the constrained clause

(i(x) ≄ x_{1} ∨ e ≄ y ∨ x_{1} ∗ x ≃ y) · (i(x) ⪰ x_{1} ∧ e ⪰ y ∧ x_{1} ∗ x ≻ y),

whereas its symmetric variant

i(x) ≄ x_{1} ∨ e ≃ x_{1} ∗ x

is transformed to

(i(x) ≄ x_{1} ∨ x_{1} ∗ x ≄ y ∨ e ≃ y) · (i(x) ⪰ x_{1} ∧ x_{1} ∗ x ⪰ y ∧ e ≻ y).

Observe that the constraint of the last clause is unsatisfiable if e is a minimal ground term with respect to the given ordering ≻. In other words, the clause is void in that case, and the constraint e ⪰ y in the other clause can be simplified to e = y.

Note. The example indicates that it is not necessary to apply subterm abstraction to a minimal constant c, as the corresponding constraint c ⪰ x associated with the abstraction of c can be simplified to x = c. Also, Skolem constants that occur only negatively need not be abstracted.

4 Preservation of Satisfiablity

The sets M, R, S, and T contain all the transformation rules we need. They eliminate all equality axioms, except reflexivity. Thus, for any set of clauses N, let CEE(N) be the clause set T(S(R(M(N))) ∪ {x ≃ x}. Our main result can then be stated as follows:

Theorem 4.1 A set N of unconstrained equational clauses is equationally unsatisfiable if and only if the transformed set CEE(N) is unsatisfiable.

It is not difficult to prove that if N is equationally satisfiable, then the transformed set CEE(N) is satisfiable. (In other words, the transformations are all sound.) The difficult part is to show that CEE(N) is unsatisfiable, whenever N is equationally unsatisfiable.

It suffices to establish this property for M(N) or, generally, for sets of flat (unconstrained) clauses. For that purpose we introduce a refutationally complete calculus for flat equational clauses (the “flat basic superposition calculus”) and show that all inferences in this calculus are reflected by logical consequences on the transformed clauses. This will imply, in particular, that a transformed set of clauses is unsatisfiable whenever a contradiction can be derived from the original clauses by flat basic superposition.

The inference rules of the flat basic superposition calculus are depicted in Figure 1. We should point out that in the presentation of superposition calculi, one usually identifies (as we have done here) a literal s ≈ t with t ≈ s (and similarly for negative literals s ≉ t).

This calculus is a slimmed-down version of a strict basic superposition calculus restricted to flat clauses, and the following theorem is a direct consequence of the results in (Bachmair & Ganzinger 1997a); see the appendix.

Theorem 4.2 Let N be a set of flat unconstrained equational clauses. The following statements are equivalent:

1. N is equationally unsatisfiable;

2. FBS^{∗}(N) contains a contradiction;

3. (R ∘ FBS)^{∗}(R(N)) contains a contradiction. Moreover, if N is a set of flat clauses, then so are the sets FBS^{∗}(N) and (R ∘ FBS)^{∗}(R(N)).

Positive flat basic superposition

\begin{matrix}(C ∨ s ≈ t) · γ & (D ∨ u ≈ v) · δ \\ (C ∨ D ∨ t ≈ v) & · & (γ ∧ δ ∧ s = u ∧ s ≻ v ≻ t) \end{matrix} ,

where neither s nor u is a variable.

Negative flat basic superposition

\begin{matrix}(C ∨ s ≈ t) · γ & (D ∨ u ≉ v) · δ \\ (C ∨ D ∨ t ≉ v) & · & (γ ∧ δ ∧ s = u ∧ s ≻ t ∧ s ≻ v) \end{matrix} ,

where u is not a variable.

Reflexivity resolution

{(C ∨ s ≉ t) · γ \atop C · (γ ∧ s = t)} .

Factoring

\begin{matrix}(C ∨ s ≈ t ∨ u ≈ v) · γ \\ (C ∨ s ≈ t) & · & (γ ∧ s = u ∧ t = v) \end{matrix} ,
where s ≡ u and t ≡ v.

Figure 1: Flat Basic Superposition FBS

The crucial advantage over previous formulations of basic superposition is that FBS has no equality factoring inferences and no positive (top-level) superposition inferences from variables. Positive top-level superposition inferences from variables can be avoided if the reduction ordering on terms is lifted to literals in a way such that unshielded, maximal variables make a literal larger than literals in which the same maximal term appears, but does not occur entirely within the substitution part of the clause.^{8} Also note that factoring is applied only when the terms which are unified by the inference have the same skeleton. In particular, if s is a variable, so is u, and vice versa, and the same is true for the pair t and v. Since transitivity elimination is sensitive to variables this uniformity will be helpful.

In the Lemma below we state a direct connection between flat basic superposition and the transformation system CEE, forming the core of our completeness proof.

Lemma 4.3 Let N be a set of flat constrained equational clauses simplified with respect to reflexivity resolution (so that R(N) = N). If D is a clause in R ∘ FBS(N), then any T ∘ S-normal form of D is a logical consequence of T ∘ S(N) ∪ {x ≃ x} (see the diagram).^{9}

8With this specific class of literal orderings, it should be possible to also close the main gap in the proof in (Moser & Steinbach 1997). There are some more details that need to be checked as the latter paper assumes a slightly different calculus and analyses superposition inferences on clauses as they are obtained after transitivity elimination.

This causes additional problems which we avoid.

9We use the symbol ∘ to denote composition of operators. Thus, T ∘ S(N) = T(S(N)).

\xymatrix{· \ar[r]^{T∘S} \ar[d]_{R∘FBS} & · \ar[d]^{⊧} \\ · \ar[r]^{T∘S} & ·}

Proof. Let D be the simplified (by R) conclusion of an inference in FBS from premises in N and let C be in T ∘ S(D). For demonstrating that C is logically implied by T ∘ S(N) ∪ {x ≃ x} we will usually apply resolution-based reasoning, followed by some strengthening of the constraint.

We prove the assertion by a case analysis over the inferences in FBS. Let

\begin{matrix}(C ∨ s ≈ t) · γ & (D ∨ u ≈ v) · δ \\ (C ∨ D ∨ t ≈ v) & · & (γ ∧ δ ∧ s = u ∧ s ≻ t ∧ u ≻ v ≻ t) \end{matrix}

be an inference by positive flat basic superposition from premises in N. Then neither s nor u is a variable. Also, the conclusion D is already simplified by R as any clause in N has this property by assumption. Any T ∘ S-normalform of D has the form

C = (C′ ∨ D′ ∨ E) · (γ ∧ δ ∧ λ_{C′} ∧ λ_{D′} ∧ s = u ∧ s ≻ t ∧ u ≻ v ≻ t ∧ ε).

where (i) C′ · (γ ∧ λ_{C′}) and D′ · (δ ∧ λ_{D′}) are T ∘ S-normalforms of C · γ and D · δ, respectively; (ii) the subclause E and the link constraints ε for the literals in E depend on (a) whether the the new equation t≈v has been oriented into t≃v or v ≃t during S normalization; and (b) on the result of T normalization, depending on whether or not t or v are variables. In this structuring of the constraint, we assume matching modulo associativity, commutativity, and idempotence of conjunction. That is, we allow for an implicit duplication of atomic constraints to bring the constraint into the form (γ ∧ δ ∧ λ_{C′} ∧ λ_{D′} ∧ s = u ∧ s ≻ t ∧ u ≻ v ≻ t ∧ ε) with conjuncts λ_{C′} and λ_{D′} as they would be introduced during a separate T ∘ S normalization of the subclauses C · γ and D · δ. We proceed with an analysis of the variants of E.

(i) Variant t ≃ v, and v is a variable. Then C has the form

(C′ ∨ D′ ∨ t ≃ v) · (γ ∧ δ ∧ λ_{C′} ∧ λ_{D′} ∧ s = u ∧ s ≻ t ∧ u ≻ v ≻ t ∧ t ≻ v)

Evidently, the constraint part of C is unsatisfiable, that is, C is void, hence trivially follows from T ∘ S(N).

From now on, to simplify notation, we shall omit the “side-literals” C′ and D′ as well as the respective “standard constraints” γ ∧ δ ∧ λ_{C′} ∧ λ_{D′} which are inherited from the C and D subclauses of the respective premises and their T ∘ S normalforms.

(ii) Variant t ≃ v, and v is not a variable. Here, C has the form

(v ≄ x ∨ t ≃ x) · (s = u ∧ s ≻ t ∧ u ≻ v ≻ t ∧ v ⪰ x ∧ t ≻ x),

or, equivalently,

(v ≄ x ∨ t ≃ x) · (s = u ∧ u ≻ v ≻ t ≻ x)  (1)

with x a fresh link variable. As neither s nor u is a variable, T ∘ S(N) contains the clauses (u ≄ x ∨ v ≃ x) · (u ⪰ x ∧ v ≻ x) and (s ≄ y ∨ t ≃ y) · (s ⪰ y ∧ t ≻ y), with link variables x and y. Consider the resolution inference

\begin{matrix}(u ≄ x ∨ v ≃ x) · (u ⪰ x ∧ v ≻ x) & (s ≄ y ∨ t ≃ y) · (s ⪰ y ∧ t ≻ y) \\ (v ≄ y ∨ t ≃ y) & · & (s ⪰ y ∧ t ≻ y ∧ u ⪰ x ∧ v ≻ x ∧ s = u ∧ y = x) \end{matrix}.

Since x and y are variables not occuring in s, t, u, v, the conclusion of this inference is equivalent to

(v ≄ x ∨ t ≃ x) · (t, v ≻ x ∧ s, u ⪰ x ∧ s = u)  (2)

The clause (2) is more general than (1) since the constraint s = u ∧ u ≻ v ≻ t ≻ x implies the constraint t, v ≻ x ∧ s, u ⪰ x. We have shown, as was required, that (1) is a logical consequence of T ∘ S(N).

(iii) Variant v ≃ t, t is a variable. After simplifying the constraint, C has the form

(v ≃ t) · (s = u ∧ s ≻ t ∧ u ≻ v ≻ t).  (3)

In this case, consider the resolution inference

\begin{matrix}(s ≃ t) · (s ≻ t) & (u ≄ x ∨ v ≃ x) · (u ⪰ x ∧ v ≻ x) \\ (v ≃ x) & · & (s ≻ t ∧ u ⪰ x ∧ v ≻ x ∧ s = u ∧ t = x) \end{matrix}

from premises in T ∘ S(N). Since x does not occur in s, t, u, v, the conclusion of this inference is equivalent to

(v ≃ t) · (u ⪰ t ∧ s, v ≻ t ∧ s = u)  (4)

which is more general than (3).

(iv) Variant v ≃ t, t is not a variable. In this case, C is equivalent to

(t ≄ x ∨ v ≃ x) · (s = u ∧ s ≻ t ∧ u ≻ v ≻ t ⪰ x),  (5)

with a fresh variable x. C can be derived from T ∘ S(N) via the inference

\begin{matrix}(t ≄ y ∨ s ≃ y) · (t ⪰ y ∧ s ≻ y) & (u ≄ x ∨ v ≃ x) · (u ⪰ x ∧ v ≻ x) \\ (t ≄ y ∨ v ≃ x) & · & (t ⪰ y ∧ s ≻ y ∧ u ⪰ x ∧ v ≻ x ∧ s = u ∧ y = x) \end{matrix} .

Since x and y are variables not occuring in s, t, u, v, the conclusion of this inference is equivalent to

(t ≄ x ∨ v ≃ x) · (t, u ⪰ x ∧ s, v ≻ x ∧ s = u)  (6)

which is more general than (5).

Next we prove the assertion for inferences by negative flat basic superposition

\begin{matrix}(C ∨ s ≈ t) · γ & (D ∨ u ≉ v) · δ \\ (C ∨ D ∨ t ≉ v) & · & (γ ∧ δ ∧ s = u ∧ s ≻ t ∧ u ≻ v) \end{matrix}

from premises in N. Let D denote the conclusion of the inference. Then u is not a variable. Again we need to conduct a case analysis according to whether or not one of the v and t are variables. Here the various cases also determine as to whether the conclusion of the inference can be further simplified by reflexivity resolution. Without loss of generality we assume that t ≥ v such that symmetry elimination transforms t ≉ v into t ≄ v. Under this assumption, if t is a variable, so must be v. We will again simplify the technical presentation by disregarding the side literals in C and D and their associated constraints.

(i) Suppose v is a variable, but t is not. Then D is in normalform with respect to R and the (unique) T ∘ S-normalform of D has the form

(t ≄ v) · (s = u ∧ s ≻ t ∧ u ≻ v ∧ t ⪰ v).  (7)

Consider the resolution inference

\begin{matrix}(t ≄ x ∨ s ≃ x) & · & (t ⪰ x ∧ s ≻ x) & (u ≄ v) & · & (u ⪰ v) \\ (t ≄ x) & · & (t ⪰ x ∧ s ≻ x ∧ u ⪰ v ∧ s = u ∧ x = v). \end{matrix}

Both premises are in T ∘ S(N). Since x is a variable not occuring in s, t, u, v, the conclusion of this inference is equivalent to

(t ≄ v) · (t ⪰ v ∧ s ≻ v ∧ u ⪰ v ∧ s = u)

which is more general than (7).

(ii) If both v and t are variables then D is normalized by the R-step in R ∘ FBS to

□ · (s = u ∧ t = v ∧ s ≻ t ∧ u ≻ v)  (8)

which is in T ∘ S-normalforms. A more general clause can also be derived from T ∘ S(N) by

\begin{matrix}(s ≃ t) & · & (s ≻ t) & (u ≄ v) & · & (u ⪰ v) \\ □ · (s ≻ t ∧ u ⪰ v ∧ s = u ∧ t = v) \end{matrix}.

(iii) Suppose that neither v nor t is a variable. Then D is in normalform with respect to R and the (unique) T ∘ S-normalform of D has the form

(t ≄ x ∨ v ≄ x) · (s = u ∧ s ≻ t ∧ u ≻ v ∧ t, v ⪰ x),  (9)

where x is a fresh variable. Consider the resolution inference

\begin{matrix}(t ≄ x ∨ s ≃ x) & · & (t ⪰ x ∧ s ≻ x) & (u ≄ y ∨ v ≄ y) & · & (u, v ⪰ y) \\ (t ≄ x ∨ v ≄ y) & · & (t ⪰ x ∧ s ≻ x ∧ u, v ⪰ y ∧ s = u ∧ x = y) \end{matrix}

from premises in T ∘ S(N). Since x is a variable not occuring in s, t, u, v, the conclusion of this inference is equivalent to

(t ≄ x ∨ v ≄ x) · (t, u, v ⪰ x ∧ s ≻ x ∧ s = u)

which is more general than (9).

Next we treat reflexivity resolution

{(C ∨ s ≉ t) · γ \atop C · (γ ∧ s = t)}

from a clause in N. Its conclusion C is in normalform with respect to R. As N is simplified with respect to R not both s and t can be variables. Let us assume, without loss of generality, that s is not a variable. Any T ∘ S-normalform D of C has the form

C′ · (γ ∧ λ_{C′} ∧ s = t),  (10)

where C′ · (γ ∧ λ_{C′}) is a T ∘ S-normalform of C · γ. We need to distinguish two cases:

(i) t is not a variable: Consider the following derivation in T ∘ S(N)

\begin{matrix}z ≃ z & \begin{matrix}y ≃ y & (C′ ∨ t ≄ x ∨ s ≄ x) · (γ ∧ λ_{C′} ∧ s, t ⪰ x) \\ (C′ ∨ s ≄ x) & · & (γ ∧ λ_{C′} ∧ s, t ⪰ x ∧ y = t ∧ y = x) \end{matrix} \\ C′ & · & (γ ∧ λ_{C′} ∧ s, t ⪰ x ∧ y = t ∧ y = x ∧ z = s ∧ z = x) \end{matrix}

by two resolution steps with (variants of) x ≃ x. Since x, y and z are variables not appearing elsewhere, the conclusion of this inference is equivalent to

C′ · (γ ∧ λ_{C′} ∧ s ≄ t)

which is precisely (10).

(ii) t is a variable: This case is similar, considering the following single-step derivation from T ∘ S(N) by resolution with a variant of x ≃ x

\begin{matrix}y ≃ y & (C′ ∨ s ≄ t) · (γ ∧ λ_{C′} ∧ s ⪰ t) \\ C′ & · & (γ ∧ λ_{C′} ∧ s ⪰ t ∧ y = s ∧ y = t) \end{matrix}

yielding a clause which is equivalent to (10).

Factoring inferences take the form

\begin{matrix}(C ∨ s ≈ t ∨ u ≈ v) · γ \\ (C ∨ s ≈ t) & · & (γ ∧ s = u ∧ t = v) \end{matrix}

where s ≡ u and t ≡ v. Let again D denote the conclusion of the inference. We have to consider four possible cases, depending on whether or not s and t (and, hence, u and v) are variables. In the analysis we again omit side-literals and their constraints.

(i) Neither s nor t is a variable. Then none of the four terms s, t, u, v is a variable. Therefore, any T ∘ S normalform of D has the form

(v ≄ x ∨ u ≃ x) · (s = u ∧ t = v ∧ v ⪰ x ∧ u ≻ x),  (11)

where x is a fresh variable. By applying positive and negative factoring to the T ∘ S normalform

(v ≄ x ∨ t ≄ y ∨ u ≃ x ∨ s ≃ y) · (t ⪰ y ∧ s ≻ y ∧ v ⪰ x ∧ u ≻ x)

of the premise of the factoring inference, we obtain the clause

(v ≄ x ∨ u ≃ x) · (v = t ∧ x = y ∧ u = s ∧ t ⪰ y ∧ s ≻ y ∧ v ⪰ x ∧ u ≻ x)

which (y does not occur elsewhere) is equivalent to

(v ≄ x ∨ u ≃ x) · (v = t ∧ u = s ∧ v ⪰ x ∧ u ≻ x)

which is precisely (11). For the variant u ≄ x ∨ v ≃ x we may construct a similar derivation.

(ii) s is a variable, and t is not a variable. Then also v is not a variable. We need to derive clauses of the form t ≄ x ∨ s ≃ x and t ≃ s with the appropriate constraints. This can be achieved by applying appropriate factoring inferences to t ≄ x ∨ v ≄ y ∨ s ≃ x ∨ u ≃ y and t ≃ s ∨ v ≃ u, respectively, where the latter, since u is not a variable, can be obtained by a resolution step with reflexivity from t ≃ s ∨ u ≄ x ∨ v ≃ x. The case in which s is not a variable, but t is, is similar.

(iii) Both s and t are variables. Then we may derive clauses of the form s ≃ t and t ≃ s with the required constraints by factoring from s ≃ t ∨ u ≃ v and t ≃ s ∨ v ≃ u, respectively. These clauses, in turn, are either T-modifications of symmetric variants of the premise of the factoring inference, or else may be obtained from these by reflexivity resolution.

□

By inductive application of this lemma we obtain the desired property for flat clauses:

Theorem 4.4 Let N be a set of flat equational clauses without constraints. Then N is equationally satisfiable if and only if T ∘ S ∘ R(N) ∪ {x ≃ x} is satisfiable.

Proof. It can easily be shown that T ∘ S ∘ R(N) ∪ {x ≃ x} is satisfiable whenever N is equationally satisfiable. Suppose that N is equationally unsatisfiable, and let N′ denote R(N). By the completeness of flat basic superposition, we may infer that (R ∘ FBS)^{∗}(N′) contains a contradiction. The set N′, and all sets (R ∘ FBS)^{k}(N′) are simplified (with respect to R) flat equational clauses to which we may (inductively) apply the above lemma. Therefore, all clauses in T ∘ S((R ∘ FBS)^{∗}(N′)) are logical consequences of T ∘ S ∘ R(N) ∪ {x ≃ x}. As the T ∘ S normal form of a contradiction is also a contradiction, T ∘ S ∘ R(N) ∪ {x ≃ x} must be unsatisfiable. □

5 Variations

Let us now briefly discuss the connection of our method to other transformation methods. Brand’s original method is not directly comparable to our method. The main difference (aside from the fact that we use constraints) is that Brand uses only a positive splitting rule,

(C ∨ u ≃ v) ⇒ (C ∨ v ≄ z ∨ u ≃ z),

but no negative splitting rule. However, the positive splitting rule is applied even if the right-hand side v of an equality literal is a variable. With Brand’s method the clause

f(g(x)) ≉ h(x) ∨ h(g(x)) ≈ x

is transformed into two clauses

g(x) ≄ z ∨ f(z) ≄ h(x) ∨ x ≄ y ∨ h(z) ≃ y

and

g(x) ≄ z ∨ f(z) ≄ h(x) ∨ h(z) ≄ y ∨ x ≃ y,

whereas our transformation would result in different (constrained) clauses

(g(x) ≄ z ∨ f(z) ≄ z_{1} ∨ h(x) ≄ z_{1} ∨ h(z) ≃ x) · (g(x) ⪰ z ∧ f(z), h(x) ⪰ z_{1} ∧ h(z) ≻ x)

and

(g(x) ≄ z ∨ f(z) ≄ z_{1} ∨ h(x) ≄ z_{1} ∨ h(z) ≄ y ∨ x ≃ y) · \begin{matrix}(g(x) ⪰ z ∧ f(z), h(x) ⪰ z_{1} ∧ \\ h(z) ⪰ y ∧ x ≻ y). \end{matrix}

It is not possible, though, to simply add link constraints to Brand’s original transitivity elimination rule.

For example, Brand’s transitivity elimination with link constraints, when applied to the unsatisfiable set of unit clauses a ≈ b, a ≈ c and b ≉ c (with an ordering in which c ≻ b ≻ a) yields a set of constrained clauses

(b ≄ x ∨ a ≃ x) · (b ⪰ x ∧ a ≻ x)
(a ≄ x ∨ b ≃ x) · (a ⪰ x ∧ b ≻ x)
(c ≄ x ∨ a ≃ x) · (c ⪰ x ∧ a ≻ x)
(a ≄ x ∨ c ≃ x) · (a ⪰ x ∧ c ≻ x)
b ≄ c

that is satisfiable (in combination with the reflexivity axiom x ≃ x)! (The first and third clause contain the unsatisfiable constraint a ≻ x and hence are void. The remaining clauses, along with x≃x, are satisfiable even without the constraints.) In short, ordering constraints are not compatible with Brand’s original transformations.

The method implemented in the Setheo prover (Moser & Steinbach 1997) can be described with our transformation rules, except that no link constraints are introduced. Positive equations with a variable on the right-hand side are not split, and hence negative equations with a non-variable right-hand side must be split also.

For example, the three unit clauses f(x)≈x, g(x)≈x and f(x)≉g(x) are unsatisfiable. However, if negative equality literals are not split, we obtain a satisfiable set of clauses f(x)≃x, f(x)≄y ∨ x≃y, g(x) ≃ x, g(x) ≄ y ∨ x ≃ y, f(x) ≄ g(x), and x ≃ x.

Let us conclude this section with an example. The presentation of group theory by three equations, x ∗ e ≈ x, x ∗ i(x) ≈ e, and (x ∗ y) ∗ z ≈ x ∗ (y ∗ z), is transformed with our method into the following set of constrained clauses:

x ∗ e ≃ x
x ∗ e ≄ u ∨ x ≃ u  · x ≻ u
i(x) ≄ u ∨ x ∗ u ≃ e · i(x) ⪰ u
x ∗ y ≄ u ∨ y ∗ z ≄ v ∨ u ∗ z ≄ w ∨ x ∗ v ≃ w · u ∗ z ⪰ w ∧ x ∗ v ≻ w ∧ x ∗ y ⪰ u ∧ y ∗ z ⪰ v
x ∗ y ≄ u ∨ y ∗ z ≄ v ∨ x ∗ v ≄ w ∨ u ∗ z ≃ w · x ∗ v ⪰ w ∧ u ∗ z ≻ w ∧ x ∗ y ⪰ u ∧ y ∗ z ⪰ v

where ≻ refers to a lexicographic path ordering induced by the precedence relation i > ∗ > e and constraints have been simplified accordingly. Note that with Brand’s modification or with equality elimination as used in Setheo one gets an additional clause,

i(x) ≄ z ∨ x ∗ z ≄ w ∨ e ≃ w.

This clause can be omitted, as its associated constraint e ≻ w is unsatisfiable in the given ordering.

6 Experiments

In Figure 6 we show some experimental results with the Protein prover (Baumgartner & Furbach 1994) on certain simple problems in group theory. “L” means that the goal was attempted in the presence a previously proved lemma. In the table we list runtimes and number of computed inferences (“K” denotes kilo, and “M” denotes mega inferences) for four kinds of transformation. The “B” column depicts the results for Brand’s original modification. “S” refers to the method that is implemented in Setheo with splitting of both positive and negative equations that have no variable right-hand side, without attaching ordering constraints. “Ss” is like “S” except that Skolem constants in the goals have not been abstracted. Compared with Brand’s method, the Setheo

number of inferences  time [sec]
Problem  ord  B  S  Ss  C  B  S  Ss  C
x ∗ e ≈ x  – 1.3M 21.4K 1.5K  578 123 2.1 0.16  0.1
i(i(x)) ≈ x  1 4.7M  ∞ 83.6M 15.5K 508  ∞ 10191  4.8
i(i(x)) ≈ x  2  ∞  ∞  ∞ 178K ∞  ∞  ∞  84
i(i(x)) ≈ x  3 4.7M  ∞ 83.6M 15.5K 502  ∞ 10191  4.8
x ∗ i(x) ≈ e  1 4.1K 288K 288K  461 0.4  30 30.4  0.1
x ∗ i(x) ≈ e  2 2.4M 17.5M 17.6M  671 272 2204 2204  0.2
i(x) ∗ (x ∗ y) ≈ y L  1 19.5K 267K 267M 3.8K 1.9  28 28.3  0.9
i(x) ∗ (x ∗ y) ≈ y L  2  ∞  ∞  ∞ 12.2M ∞  ∞  ∞ 3235
i(x) ∗ (x ∗ y) ≈ y  1 9.1M  ∞  ∞  24M 950  ∞  ∞ 10574
i(x) ∗ (x ∗ y) ≈ y  2  ∞  ∞  ∞  ∞ ∞  ∞  ∞  ∞

Figure 2: Experimental results on a 167MHz UltraSparc for simple problems in group theory

method avoids more of those inferences which correspond to superposition into or from variables. However, it comes at the expense of also splitting negative equations. The experiments show that the price to pay is indeed very high so that in some of our experiments, “S” performs much worse than Brand’s original method. However, if disequations s ≃ t in which t is a Skolem constant of the goal are not split we obtain a uniform and more significant improvement. This variant is denoted by “Ss” below. Finally, “C” is CEE transformation, using the presentation of group theory as presented in Section 5. We implemented constraint inheritance and checking in a straightforward manner. Ordering constraints are collected through additional arguments of predicate symbols. (As to what extent the additional predicates affect Protein’s proof strategy, we do not know.) The first subgoal of any (non-unit) clause first calls upon a satisfiability check (implemented in Prolog) for the accumulated constraint at this point. Constraint solving was implemented incompletely by simply checking independent satisfiability of each inequality in any conjunction of inequalities. A complete constraint solving which is available for large classes of lexicographic path orderings, is very expensive and does not seem to reduce the number of inferences by another order of magnitude.

Protein is extremely sensitive to how the clauses and the literals in a clause, respectively, are ordered. In the examples we have experimented with three different orderings of the subgoals in the goal clause. In ordering 1 the variable definitions for inner subterm positions precede those of the outer positions. This ordering seems to work better with Protein most of the time. Ordering 2 is the inverse of ordering 1. Ordering 3 is some mixture of orderings 1 and 2. Orderings 2 and 3 coincide for the CEE transformation. For ordering 2, the speedups obtained from the optimization are much more dramatic. This seems to indicate that with the constraints the performance of model elimination is somewhat less dependent on subgoal selection strategies. In particular upon backtracking, ordering constraints prevent one from searching redundant alternative proofs of subgoals.

Although these experiments are far from being conclusive, it appears as if the CEE transformation can have a dramatic effect on proof search. Except for one case, proofs using CEE transformation were found much faster, usually by several orders of magnitude. With the rather incomplete method of constraint satisfiability checking, the price paid on each single inference seems affordable.

As said before, Protein proof search is too much dependent on the ordering of clauses and of subgoals within clauses. It would be interesting to see the effect of our improvements on Setheo where dynamic goal selection strategies result in a more predictable behavior and find proofs more often, also for less trivial problems than the ones studied in our experiments (Ibens & Letz 1997).

7 Conclusions

We have described a refined variant of Brand’s modification method via ordering constraints that also improves equality elimination as implemented in the prover Setheo. Our theoretical results imply that equality handling in Setheo is indeed refutationally complete (which was an open problem). The completeness proof draws on recent results about basic superposition and thus establishes a connection between the theory underlying local saturation-based methods, such as paramodulation and superposition, and optimizations of equality handling in global theorem proving methods, such as model elimination and semantic tableau-methods.

Our experiments seem to indicate that with the ordering constraints the search space is indeed drastically reduced. However, our results in this regards are not conclusive yet. An implementation of the method in a more advanced model elimination prover, like Setheo, should allow one to draw more definite conclusions in this regard.

References

Bachmair, L. & Ganzinger, H. (1997a), Strict basic superposition and chaining, Research report MPI-I-97-2-011, Max-Planck Institut für Informatik, Saarbrücken, Germany. *www.mpi-sb.mpg.de/˜ hg/papers/reports/MPI-I-97-2-011.ps.gz

Bachmair, L. & Ganzinger, H. (1997b), A theory of resolution, Research report MPI-I-97-2-005, Max-Planck Institut für Informatik, Saarbrücken, Germany. To appear in Handbook of Automated Reasoning, edited by A. Robinson and A. Voronkov.

Baumgartner, P. & Furbach, U. (1994), PROTEIN: A PROver with a Theory Extension INterface, in A. Bundy, ed., ‘Automated Deduction — CADE-12. 12th International Conference on Automated Deduction.’, Vol. 814 of Lecture Notes in Artificial Intelligence, Nancy, France, pp. 769–773.

Brand, D. (1975), ‘Proving theorems with the modification method’, SIAM Journal of Computing 4, 412–430.

Degtyarev, A. & Voronkov, A. (1996a), Equality elimination for the tableau method, in J. Calmet & C. Limongelli, eds, ‘Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO’96’, Vol. 1128 of Lecture Notes in Computer Science, Karlsruhe, Germany, pp. 46–60.

Degtyarev, A. & Voronkov, A. (1996b), What you always wanted to know about rigid E-unification, in J. Alferes, L. Pereira & E. Orlowska, eds, ‘Logics in Artificial Intelligence. European Workshop, JELIA’96’, Vol. 1126 of Lecture Notes in Artificial Intelligence, Évora, Portugal, pp. 50– 69.

Ibens, O. & Letz, R. (1997), Subgoal alternation in model elimination, in D. Galmiche, ed., ‘Automated Reasoning with Analytic Tableaux and Related Methods’, Vol. 1227 of Lecture Notes in Artificial Intelligence, Springer Verlag, pp. 201–215.

Moser, M., Lynch, C. & Steinbach, J. (1995), Model elimination with basic ordered paramodulation, Technical Report AR-95-11, Fakultät für Informatik, Technische Universität München, München.

Moser, M. & Steinbach, J. (1997), STE-modification revisited, Technical Report AR-97-03, Fakultät für Informatik, Technische Universität München, München.

Schumann, J. (1994), ‘Tableau-based theorem provers: Systems and implementations’, Journal of Automated Reasoning 13(3), 409–421.

Positive basic superposition

\begin{matrix}(C ∨ s ≈ t) · γ & (D ∨ w[u] ≈ v) · δ \\ (C ∨ D ∨ w[t] ≈ v) & · & (γ ∧ δ ∧ s = u ∧ s ≻ t ∧ w ≻ v ∧ (w, v) ⪰_{lex} (s, t) ∧ ζ) \end{matrix}

where (i) u is not a variable and (ii) either s is not a variable or else u is a proper subterm of w.

Negative basic superposition

\begin{matrix}(C ∨ s ≈ t) · γ & (D ∨ w[u] ≉ v) · δ \\ (C ∨ D ∨ w[t] ≉ v) & · & (γ ∧ δ ∧ s = u ∧ s ≻ t ∧ w ≻ v ∧ ζ) \end{matrix}

where u is not a variable.

Reflexivity resolution

{(C ∨ s ≉ t) · γ \atop C · (γ ∧ s = t ∧ ζ)}

Factoring

\begin{matrix}(C ∨ s ≈ t ∨ u ≈ v) · γ \\ (C ∨ s′ ≈ t′) & · & (γ ∧ s = u ∧ t = v ∧ ζ) \end{matrix}

where s ≡ u and t ≡ v.

Figure 3: Strict Basic Superposition BS

A Basic Superposition

The flat basic superposition calculus is derived from one of the strict basic superposition calculi described in (Bachmair & Ganzinger 1997a), see Figure 3.

In all cases, ζ refers to inference-specific ordering constraints that are irrelevant for our purposes and hence have been deleted in the flat versions of the inference rules. (Such constraints may always be deleted without impairing the soundness or refutational completeness of the calculus.)

Moreover, the remaining constraints in the flat inference rules have been simplified. For instance, if the second premise of a (positive or negative) basic superposition rule is a flat clause, then the two terms w and u must be identical, as any proper subterm in a flat clause is a variable, yet u is required to be a non-variable subterm of w. Using the facts that w = u and s = u, one may then simplify the ordering constraints as indicated. In particular, the constraint (w, v) ⪰_{lex} (s, t) in positive superpositions reduces to s ≻ v ⪰ t in the flat case. The instance v = t can also be ignored. In that case the conclusion contains t≈t positively, hence, is a direct tautology which is redundant. Direct tautologies are a strict subclass of all tautologies, cf. (Bachmair & Ganzinger 1997a) for the exact definition.

Basic superposition calculi are also compatible with other various mechanisms for eliminating redundancies and simplifying clauses. For the present paper it suffices to point out that, in addition to direct tautologies, void clauses are redundant, as are inferences with a void conclusion. The former can be deleted, while the latter may be ignored. Furthermore, the special case of reflexivity resolution as represented by the transformation R is a simplification rule. That is, a clause (x ≉ y ∨ C) · γ with variables x and y, is redundant in the presence of a clause C · (γ ∧ x = y) and, hence, can be deleted. Summarizing these observations, we obtain the Theorem 4.2 stated above.

[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-97-2-011 L. Bachmair, H. Ganzinger  Strict Basic Superposition and Chaining

MPI-I-97-2-010 S. Vorobyov, A. Voronkov Complexity of Nonrecursive Logic Programs with Complex Values

MPI-I-97-2-009 A. Bockmayr, F. Eisenbrand  On the Chvátal Rank of Polytopes in the 0/1 Cube

MPI-I-97-2-008 A. Bockmayr, T. Kasper A Unifying Framework for Integer and Finite Domain Constraint Programming

MPI-I-97-2-007 P. Blackburn, M. Tzakova  Two Hybrid Logics
MPI-I-97-2-006 S. Vorobyov  Third-order matching in λ →-Curry is undecidable
MPI-I-97-2-005 L. Bachmair, H. Ganzinger  A Theory of Resolution
MPI-I-97-2-004 W. Charatonik, A. Podelski  Solving set constraints for greatest models
MPI-I-97-2-003 U. Hustadt, R.A. Schmidt  On evaluating decision procedures for modal logic

MPI-I-97-2-002 R.A. Schmidt Resolution is a decision procedure for many propositional modal logics

MPI-I-97-2-001 D.A. Basin, S. Matthews, L. Viganò  Labelled modal logics: quantifiers
MPI-I-96-2-010 A. Nonnengart  Strong Skolemization

MPI-I-96-2-009 D.A. Basin, N. Klarlund Beyond the Finite in Automatic Hardware Verification

MPI-I-96-2-008 S. Vorobyov On the decision complexity of the bounded theories of trees

MPI-I-96-2-007 A. Herzig  SCAN and Systems of Conditional Logic
MPI-I-96-2-006 D.A. Basin, S. Matthews, L. Viganò  Natural Deduction for Non-Classical Logics