# Axioms vs. rewrite rules: from completeness to cut elimination

Gilles Dowek

► To cite this version:

Gilles Dowek. Axioms vs. rewrite rules: from completeness to cut elimination. 2000. hal-04112760

HAL Id: hal-04112760

https://inria.hal.science/hal-04112760

Preprint submitted on 1 Jun 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Axioms vs. rewrite rules:
from completeness to cut elimination

Gilles Dowek *

## Abstract

Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may require in particular to prove cut elimination for an extended notion of proof that combines deductions and computations. This suggests new interactions between automated theorem proving and proof theory.

When we search for a proof of the proposition 2+2=4, we can use the axioms of addition and equality to transform this proposition into 4=4 and conclude with the reflexivity axiom. We could also use these axioms to transform this proposition into 2+2 = 2+2 and conclude, but this proof is redundant with the first, that is in many ways better. Indeed, the axioms of addition are better used in one direction only: to compute values. In automated proof search systems, we often suppress axioms, such as the axioms of addition, and replace them by rewrite rules. This permits to cut off search space while keeping completeness.

The rules of addition apply to terms, but rules applying to propositions may also be considered. For instance, the axiom

$$ \forall xy ((x \times y) = 0 \Leftrightarrow (x = 0 \lor y = 0)) $$

can be replaced by the rule

$$ x \times y = 0 \rightarrow x = 0 \lor y = 0 $$

that rewrites an atomic proposition into a disjunction. Such rules are of special interest in set theory, e.g.

$$ x \in \{y, z\} \rightarrow x = y \lor x = z $$

<footnote>*INRIA-Rocquencourt, B.P. 105, 78153 Le Chesnay Cedex, France.
Gilles.Dowek@inria.fr, http://coq.inria.fr/~dowek</footnote>
and in type theory [?, ?], e.g.

$$ \varepsilon(x \Rightarrow y) \rightarrow \varepsilon(x) \Rightarrow \varepsilon(y) $$

When we orient an axiom, we want to cut off search space, but we do not want to loose completeness. In this note, we discuss the properties that the rewrite system must fulfill, so that orientation does not jeopardize completeness.

# 1 Orientation

## 1.1 From replacement to rewriting

We consider a set $A$ and a binary relation $\rightarrow$ defined on $A$. We write $\rightarrow^*$ for its reflexive-transitive closure and $\equiv$ for its reflexive-symmetrical-transitive closure.

If $t$ and $t'$ are two elements of $A$, we have $t \equiv t'$ if and only if there is a sequence of terms $t_1, ..., t_n$ such that $t = t_1, t' = t_n$ and for each $i$, either $t_i \rightarrow t_{i+1}$ or $t_i \leftarrow t_{i+1}$.

For instance, if $A$ is a set of terms built with a binary operator $+$ and a finite number of constants and $\rightarrow$ is the relation such that $t \rightarrow u$ if and only if $u$ is obtained from $t$ by replacing a subterm of the form $(x + y) + z$ by $x + (y + z)$. We can establish that

$$ (a + (b + c)) + (d + e) \equiv (a + b) + ((c + d) + e) $$

with the sequence

<figure><img src="image_2.png" /></figure>

To establish that $t \equiv t'$, we search for such a sequence. We can apply the following replacement method: we start with the equality $t = t'$ and we derive more equalities with two rules. The first permits to derive $v = v'$ from $u = u'$ if $u = u' \rightarrow v = v'$ and the second permits to derive $v = v'$ from $u = u'$ if $u = u' \leftarrow v = v'$. When reach an equality of the form $u = u$, we are done.

Search is more efficient if we restrict to rewriting sequences, i.e. sequences of the form

$$ t = t_1 \rightarrow \dots \rightarrow t_n = u_1 \leftarrow \dots \leftarrow u_p = t' $$

For instance
<figure><img src="image_3.png" /></figure>

Indeed, to establish that $t \equiv t'$, we can restrict the replacement method, to the first rule and rewrite the equality $t = t'$ to an equality of the form $u = u$.

Such a restriction may be incomplete. Consider, for instance, the relation defined by $p \to' q$ and $p \to' r$. We have $q \leftarrow' p \to' r$ but there is no rewriting sequence relating $q$ to $r$ and the equality $q = r$ cannot be rewritten.

A relation is said to be confluent if whenever $t \to^* t_1$ and $t \to^* t_2$ there is a object $u$ such that $t_1 \to^* u$ and $t_2 \to^* u$.

For instance, the relation $\to$ above is confluent, but the relation $\to'$ is not. It is easy to prove that when a relation is confluent, two objects are related if and only if they are related by a rewriting sequence and thus that rewriting is a complete search method.

## 1.2 From paramodulation to narrowing

Let us now turn to proof search in predicate calculus with equality. We assume that we have an equality predicate and the associated axioms. Paramodulation [?] is an extension of resolution that allows to replace equals by equals in clauses.

For instance, if we want to refute the clauses

$$ \begin{align*} (X + Y) + Z &= X + (Y + Z) \\ P((a + (b + c)) + (d + e)) \\ \neg P((a + b) + ((c + d) + e)) \end{align*} $$

we use the associativity to rearrange brackets in the other clauses until we can resolve them.

Exactly as above, we can restrict the method and use of some equalities in one direction only. We suppress these equalities from the set of clauses to refute, we orient them as rewrite rules and we use them with a narrowing (or oriented paramodulation) rule that permits to unify a subterm of a clause with the left-hand side of a rewrite rule, and replace the instantiated subterm with the right-hand side of this rule (see, for instance, [?, ?]). Notice that since clauses may contain variables, we need to use unification (and not matching as in rewriting).

The completeness of this method mostly rests on confluence of the rewrite system<fnref n="1" />: instead of using the rewrite rules in both directions to unfold and fold terms, we can use them in one direction only and meet on a common reduct.

<footnote n="1">¹Actually, although confluence plays the major rôle in completeness proofs, termination</footnote>
## 1.3 Equational resolution

Equational resolution [?, ?] is another proof search method for predicate calculus with equality. In this method, like in narrowing, we suppress some equalities from the set of clauses to refute and we orient them as rewrite rules. We write $t \to t'$ if $t'$ is obtained by rewriting a subterm in $t$. We write $\to^*$ for the reflexive-transitive closure of this relation and $\equiv$ for its reflexive-symmetrical-transitive closure.

Morally, we identify equivalent propositions and we work on equivalence classes. Hence, we use an extended resolution rules where unification is replaced by equational unification [?, ?]: a unifier of two-terms $t$ and $u$ is a substitution $\sigma$ such that $\sigma t \equiv \sigma u$ (and not $\sigma t = \sigma u$). For instance the terms $(a+(b+c))+(d+e)$ and $(a+b)+((c+d)+e)$ are trivially unifiable because they are equivalent and hence with the clauses

$$P((a + (b + c)) + (d + e))$$

$$\neg P((a + b) + ((c + d) + e))$$

we can apply the resolution rule and get the empty clause.

To solve equational unification problems, we can use narrowing. But, in contrast with the previous method, the narrowing rule is applied to the unification problems and not to the clauses.

# 2 Completeness

We focus now on the completeness of equational resolution. We first recall a completeness proof of resolution and then discuss how it can be adapted.

## 2.1 Completeness of resolution

**Cut elimination** A way to prove completeness of resolution is to prove that whenever a sequent $A_1, ..., A_p \vdash B_1, ..., B_q$ has a proof in sequent calculus (see, for instance, [?, ?]), the empty clause can be derived from the clausal form of the propositions $A_1, ..., A_p, \neg B_1, ..., \neg B_q$.

Usually this proof proceeds in two steps: we first prove that if a sequent $\Gamma \vdash \Delta$ has a proof, then it has also a proof that does not use the cut rule of sequent calculus (cut elimination theorem). Then we prove, by induction over proof structure, that if $\Gamma \vdash \Delta$ has a cut free proof, then the empty clause can be derived from clausal form $cl(\Gamma, \neg \Delta)$ of the propositions $\Gamma, \neg \Delta$.

**A variant** A variant of this proof isolates the clausification step. A first lemma proves that if the sequent $\Gamma \vdash \Delta$ has a proof and $cl(\Gamma, \neg \Delta) = \{P_1, ..., P_n\}$, then

<footnote>also is used. Whether or not completeness fails for non terminating systems in unknown to the author.</footnote>
the sequent $\overline{\forall}P_1...\overline{\forall}P_n \vdash$ also has a proof, where $\overline{\forall}P$ is the universal closure of the proposition $P$.

Then, by the cut elimination theorem, if the sequent $\overline{\forall}P_1...\overline{\forall}P_n \vdash$ has a proof, it has also a cut free proof. At last, we prove by induction over proof structure that if $\overline{\forall}P_1...\overline{\forall}P_n \vdash$ has a cut free proof then the empty clause can be derived from $\{P_1, ..., P_n\} = cl(\Gamma, \neg\Delta)$.

**Herbrand theorem** Instead of using the cut elimination theorem some authors prefer to use Herbrand theorem that is a variant of it.

According to Herbrand theorem, if $P_1, ..., P_n$ are quantifier free propositions then the sequent $\overline{\forall}P_1...\overline{\forall}P_n \vdash$ has a proof if and only if there are instances $\sigma_1^1 P_1, ..., \sigma_{k_1}^1 P_1, ..., \sigma_1^n P_n, ..., \sigma_{k_n}^n P_n$ of the propositions $P_1, ..., P_n$ such that the quantifier free proposition $\neg(\sigma_1^1 P_1 \wedge ... \wedge \sigma_{k_1}^1 P_1 \wedge ... \wedge \sigma_1^n P_n \wedge ... \wedge \sigma_{k_n}^n P_n)$ is tautologous.

As above, a first lemma proves that if the sequent $\Gamma \vdash \Delta$ has a proof and $cl(\Gamma, \neg\Delta) = \{P_1, ..., P_n\}$, then the sequent $\overline{\forall}P_1...\overline{\forall}P_n \vdash$ also has a proof. By Herbrand theorem, if the sequent $\overline{\forall}P_1...\overline{\forall}P_n \vdash$ has a proof, then there are instances $\sigma_1^1 P_1, ..., \sigma_{k_1}^1 P_1, ..., \sigma_1^n P_n, ..., \sigma_{k_n}^n P_n$ of the propositions $P_1, ..., P_n$ such that the quantifier free proposition $\neg(\sigma_1^1 P_1 \wedge ... \wedge \sigma_{k_1}^1 P_1 \wedge ... \wedge \sigma_1^n P_n \wedge ... \wedge \sigma_{k_n}^n P_n)$ is tautologous. At last, we prove that if the proposition $\neg(\sigma_1^1 P_1 \wedge ... \wedge \sigma_{k_1}^1 P_1 \wedge ... \wedge \sigma_1^n P_n \wedge ... \wedge \sigma_{k_n}^n P_n)$ is tautologous then the empty clause can be derived from $\{P_1, ..., P_n\} = cl(\Gamma, \neg\Delta)$.

## 2.2 Completeness of equational resolution

This proof can be adapted to equational resolution. First, the identification of equivalent propositions used in proof search can be used in sequent calculus also. This leads to the *sequent calculus modulo* [?]. For instance, the axiom rule

$$ \overline{A \vdash A} \text{ axiom} $$

is transformed into the rule

$$ \overline{A \vdash\equiv B} \text{ axiom if } A \equiv B $$

and the left rule of disjunction

$$ \frac{\Gamma A \vdash \Delta \quad \Gamma B \vdash \Delta}{\Gamma A \vee B \vdash \Delta} \quad \forall\text{-left} $$

is transformed into the rule

$$ \frac{\Gamma A \vdash\equiv \Delta \quad \Gamma B \vdash\equiv \Delta}{\Gamma C \vdash\equiv \Delta} \quad \forall\text{-left if } C \equiv A \vee B $$
In sequent calculus modulo the rules of addition and multiplication, we have a
very short proof that the number 4 is even

$$
\begin{array}{c}
\begin{array}{c}
\overline{4 = 4 \vdash \equiv 4 = 2 \times 2} \text{ axiom} \\
\frac{\forall x (x = x) \vdash \equiv 4 = 2 \times 2}{\forall x (x = x) \vdash \equiv \exists y (4 = 2 \times y)} \forall\text{-left} \\
\exists\text{-right}
\end{array} \\
\text{while proving this proposition would be much more cumbersome in sequent}
\end{array}
$$

while proving this proposition would be much more cumbersome in sequent
calculus with the axioms of addition and multiplication.

Using sequent calculus modulo, we can prove the completeness of equational
resolution. First, we prove the equivalence lemma: if the rewrite system encodes
a theory *T* then the sequent Γ*T* ⊢ Δ has a proof in sequent calculus if and only
if the sequent Γ ⊢equiv Δ has a proof in sequent calculus modulo. Then, the
cut elimination theorem extends trivially to sequent calculus modulo when the
equivalence is generated by rewrite rules applying to terms. At last, we prove
by induction over proof structure, that if Γ ⊢equiv Δ has a cut free proof in sequent
calculus modulo, then the empty clause can be derived from *cl*(Γ, ¬Δ) with
the rules of equational resolution. The confluence of the rewrite system is only
needed to prove that narrowing is a complete equational unification method.

2.3 Equational resolution as narrowing

Equational resolution can be seen as a formulation of narrowing. This suggests
another completeness proof, reducing the completeness of equational resolution
to that of narrowing.

Indeed, instead of resolving two clauses and narrowing the unification problem, as we do in equational unification, we could first narrow the clauses and apply the usual resolution rule to get the same result.

For instance, instead of resolving

$$
P((a + (b + c)) + (d + e))
$$

$$
\neg P((a + b) + ((c + d) + e))
$$

and narrowing the unification problem

$$
(a + (b + c)) + (d + e) = (a + b) + ((c + d) + e)
$$

we could take an option on these two clauses, and narrow them until they can
be resolved.

So, narrowing a unification problem is just a way to narrow the clauses it
comes from. Hence, equational resolution can be seen as a formulation of nar-
rowing and thus as an implementation of paramodulation with the restriction
that some equations should be used in one direction only. Hence, the complete-
ness of equational resolution rests on confluence.
### 3 Rewriting proposition

So far, we have considered methods where axioms are replaced by rewrite rules applying to terms. We have seen that the proof search methods obtained this way could be seen as restrictions of paramodulation and that their completeness rested on confluence. We consider now more powerful rewrite rules applying to propositions. For instance, the axiom

$$ \forall xy (x \times y = 0 \Leftrightarrow (x = 0 \lor y = 0)) $$

can be replaced by the rule

$$ x \times y = 0 \rightarrow x = 0 \lor y = 0 $$

that applies directly to propositions. For technical reasons, we restrict to rules, such as this one, whose left-hand side is an atomic proposition.

For example, with this rule, we can prove the proposition

$$ \exists z (a \times a = z \Rightarrow a = z) $$

in sequent calculus modulo

$$ \frac{\begin{array}{c} a = 0 \vdash_{\equiv} a = 0 \\ \frac{a \times a = 0 \vdash_{\equiv} a = 0}{\vdash_{\equiv} a \times a = 0 \Rightarrow a = 0} \end{array}}{\begin{array}{c} a = 0 \vdash_{\equiv} a = 0 \\ \frac{\vdash_{\equiv} a \times a = z \Rightarrow a = z}{\vdash_{\equiv} \exists z (a \times a = z \Rightarrow a = z)} \end{array}} \quad \begin{array}{l} \text{axiom} \\ \text{axiom} \\ \text{\textasciitilde;-left} \\ \text{\textasciitilde;-right} \end{array} $$

#### 3.1 Resolution modulo

In this case, equational resolution can be extended to resolution modulo [?]. In resolution modulo, like in equational resolution, the rewrite rules applying to terms are used to narrow unification problems, but, like in narrowing, the rules applying to propositions are used to narrow the clauses directly.

For instance, if we take the clausal form of the negation of the proposition

$$ \exists z (a \times a = z \Rightarrow a = z) $$

i.e. the clauses

$$ a \times a = Z $$

$$ \neg a = Z $$

we can narrow the first clause with the rule

$$ x \times y = 0 \rightarrow x = 0 \lor y = 0 $$

yielding the clause

$$ a = 0 $$

Then, we resolve this clause with $\neg a = Z$ and get the empty clause.
## 3.2 Resolution with axioms

An alternative is to keep the axiom

$$ \forall xy (x \times y = 0 \Leftrightarrow (x = 0 \lor y = 0)) $$

and to use resolution. In this case, we have to refute the clauses

$$ \neg X \times Y = 0, X = 0, Y = 0 $$

$$ X \times Y = 0, \neg X = 0 $$

$$ X \times Y = 0, \neg Y = 0 $$

$$ a \times a = Z $$

$$ \neg a = Z $$

We resolve the clause $a \times a = Z$ with the clause $\neg X \times Y = 0, X = 0, Y = 0$ yielding the clause $a = 0$. Then, we resolve this clause with $\neg a = Z$ and get the empty clause.

An above, resolution modulo can be seen as a restriction of resolution, where some clauses can be used in one direction only. As above we could think that resolution modulo is complete as soon as the rewrite system is confluent. Unfortunately this is not the case.

## 3.3 A counter example to completeness

The axiom

$$ A \Leftrightarrow (B \land \neg A) $$

can be transformed into a rewrite rule (Crabbé's rule)

$$ A \rightarrow B \land \neg A $$

Resolution modulo cannot prove the proposition $\neg B$, because from the clause $B$, neither the resolution rule nor the narrowing rule can be applied.

But, surprisingly, with the axiom $A \Leftrightarrow (B \land \neg A)$, we can prove the proposition $\neg B$. Indeed, the clausal form of the proposition $A \Rightarrow (B \land \neg A)$ yields the clauses

$$ \neg A, B \quad \neg A $$

the clausal form of the proposition $(B \land \neg A) \Rightarrow A$ yields

$$ A, \neg B $$

and the clausal form of the negation of the proposition $\neg B$ yields

$$ B $$

From $B$ and $A, \neg B$, we derive $A$ and then from this clause and $\neg A$ we get the empty clause. Hence, a resolution proof with axioms cannot always be
transformed into a resolution modulo proof. Resolution modulo cannot be seen
as a restriction of resolution where some clauses can be used in one direction
only and completeness may be lost even if the rewrite system is confluent.

Notice that, in the resolution proof, clauses coming from both propositions
$A \Rightarrow (B \land \neg A)$ and $(B \land \neg A) \Rightarrow A$ are used. Hence, although the rewrite system
is confluent, we need both to unfold $A$ to $B \land \neg A$ and to fold $B \land \neg A$ to $A$.
Moreover, when we resolve $B$ with $\neg B$, $A$ we fold $B \land \neg A$ to $A$ although we have
proved the proposition $B$, but not the proposition $\neg A$ yet. This *partial folding*
that resolution allows but resolution modulo disallows is the reason why some
resolution proofs cannot be transformed into resolution modulo proofs.

Hence, orientation cuts off search space more dramatically when we have
rules rewriting propositions that when we have only rules rewriting terms. It
can cut off search space so dramatically that completeness may be lost.

3.4 Completeness of resolution modulo

Since resolution can prove the proposition $\neg B$ with the axiom $A \Leftrightarrow (B \land \neg A)$,
the sequent $A \Leftrightarrow (B \land \neg A) \vdash \neg B$ can be proved in sequent calculus and hence
the sequent $\vdash \neg B$ can be proved in sequent calculus modulo. For instance, it
has the proof

<figure><img src="image_4.png" /></figure>

The proposition $\neg B$ has a proof in sequent calculus modulo but not in resolution
modulo and thus resolution modulo is incomplete.

The completeness theorem of resolution modulo does not prove that each
time a proposition has a proof in sequent calculus modulo, it has a proof in
resolution modulo (because this is false), but it proves, using techniques similar
to those developed in section ?? and ??, that if a proposition has a cut free
proof in sequent calculus modulo, it has a proof in resolution modulo.

The proposition $\neg B$ has proof in sequent calculus modulo, but no cut free
proof and sequent calculus modulo the rule $A \rightarrow B \land \neg A$ does not have the cut
elimination property.

Modulo some rewrite systems such as

$$
x \times y = 0 \rightarrow x = 0 \lor y = 0
$$

or

$A \rightarrow B \land A$
sequent calculus modulo has the cut elimination property and thus resolution modulo is complete. Hence modulo these rewrite systems there is no occurrence of the phenomenon we have observed above, where a resolution proof could not be transformed into a resolution modulo proof because it used partial folding. Still the translation of resolution proofs to resolutions modulo proofs is non trivial because it involves cut elimination.

In [?] we present cut elimination proofs for large classes of rewrite systems (including various presentations of type theory, all confluent and terminating quantifier free rewrite systems, ...) and we conjecture that cut elimination holds for all terminating and confluent rewrite system, although we know that such a conjecture cannot be proved in type theory or in large fragments of set theory because it implies their consistency. Cut elimination also holds for sequent calculus modulo some non terminating rewrite systems such as

$$A \to B \land A$$

Notice that when resolution modulo is complete (for instance for type theory), this completeness result cannot be proved in the theory itself (because it implies its consistency), while confluence usually can. So, it is not surprising that tools more powerful than confluence, such as cut elimination, are required.

## 3.5 Towards a new kind of completion

Completion [?] transforms a rewrite system into a confluent one. We can imagine a similar process that transforms a rewrite system into one modulo which sequent calculus has the cut elimination property.

For instance, the rule $A \to B \land \neg A$ is equivalent to the axiom $A \Leftrightarrow (B \land \neg A)$ whose clausal form is

$$A, \neg B \quad B, \neg A \quad \neg A$$

like that of the axioms $A \Leftrightarrow \bot$ and $B \Leftrightarrow A$ that are equivalent to the rewrite system $A \to \bot$, $B \to A$ modulo which sequent calculus has the cut elimination property and resolution is complete.

So we could imagine to transform the rewrite system

$$A \to (B \land \neg A)$$

into

$$A \to \bot$$

$$B \to A$$

or even into

$$A \to \bot$$

$$B \to \bot$$

in order to recover completeness.
# Acknowledgements

Thanks to Th. Hardin, C. Kirchner, Ch. Lynch and B. Werner for many helpful
discussions on this subject.

# References

[1] G. Dowek, Th. Hardin, and C. Kirchner, Theorem proving modulo, Rapport de Recherche INRIA 3400 (1998).

[2] G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an intentional first-order expression of higher-order logic, *Rewriting Techniques and applications*, P. Narendran and M. Rusinowitch (Eds.), Lecture Notes in Computer Science 1631, Springer-Verlag (1999), pp. 317-331.

[3] G. Dowek and B. Werner. Proof normalization modulo. *Types for proofs and programs* 98, T. Altenkirch, W. Naraschewski, B. Rues (Eds.), Lecture Notes in Computer Science 1657, Springer-Verlag (1999), pp. 62-77. Rapport de Recherche 3542, INRIA (1998)

[4] M.J. Fay, First-order unification in an equational theory, Fourth Workshop on Automated Deduction (1979), pp. 161-167.

[5] J. Gallier, Logic in computer science, *Harper and Row* (1986).

[6] J.Y. Girard, Y. Lafont, and P. Taylor. Types and proofs, *Cambridge University Press* (1989).

[7] J.-M. Hullot, Canonical forms and unification, W. Bibel and R. Kowalski (Eds.) *Conference on Automated Deduction*, Lecture Notes in Computer Science 87, Springer-Verlag (1980), pp. 318-334.

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

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

[10] G. Peterson, A Technique for establishing completeness results in theorem proving with equality, *Siam J. Comput.*, 12, 1 (1983) pp. 82-100.

[11] G. Plotkin, Building-in equational theories Machine Intelligence, 7 (1972), pp. 73-90

[12] G.A. Robinson and L. Wos, Paramodulation and theorem proving in first-order theories with equality, *Machine Intelligence*, 4, B. Meltzer and D. Michie (Eds.), American Elsevier (1969) pp. 135-150.

[13] M. Stickel, Automated deduction by theory resolution, *Journal of Automated Reasoning*, 4, 1 (1985), pp. 285-289.