What You Always Wanted to Know about Rigid E-Unification.
This paper solves an open problem posed by a number of researchers: the construction of a complete calculus for matrix-based methods with rigid E-unification. The use of rigid E-unification and simultaneous rigid E-unification for such methods was proposed by Gallier et al., in 1987. After our proof of the undecidability of simultaneous rigid E-unification in 1995. (Degtyarev and Voronkov, 1996d), it became clear that one should look for more refined techniques to deal with equality in matrix-based methods. In this article, we define a complete proof procedure for first-order logic with equality based on an incomplete but terminating procedure for rigid E-unification. Our approach is applicable to the connection method and the tableau method and is illustrated on the tableau method.
Introduction
Algorithms for theorem-proving based on matings or tableaux in first-order logic
without equality comprise two kinds of rules. Rules of the first kind construct
matrices or tableaux from a given formula using a suitable amplification. Rules
of the second kind try to close paths or branches using substitutions making the
paths or branches inconsistent. These substitutions are unifiers of some atoms
laying on a path or branch. Until recently, most approaches to introducing equality
in such matrix-based methods tried to generalize such algorithms by a suitable
modification of the notion of a unifier.
Such a modification using simultaneous rigid E-unification was introduced in
(Gallier et al., 1987) for the method of matings (Andrews, 1981) or the connection
method (Bibel, 1981). It can be easily represented in the tableau formalism. The
method of matings interleaves two steps: amplification by quantifier duplication
and search for mating for a given amplification. For formulas in disjunctive normal
form this method was formulated earlier in (Prawitz, 1983). In this case amplification
is represented by a matrix and mating is represented by a set of simultaneously
satisfiable substitution conditions (mated pairs). Prawitz proposed a procedure for
constructing substitution conditions one by one, closing the corresponding paths
in the matrix through search with backtracking. Procedures of this kind were used
in later formalizations and implementations of the tableau method, the method
of matings or the connection method for formulas without equality. For example,
in (Fitting, 1990) the search for mating consists of repeated applications of MGU
atomic closure rule.
Supported by grants from INTAS, TFR and the Swedish Royal Academy of Sciences
y Partially supported by a TFR grant
(Gallier et al., 1987) tried to describe a similar procedure for logic with equality.
For example, (Gallier et al., 1992) describe such a procedure in which a substitution
condition is formalized via rigid E-unification, and the set of substitution
conditions via simultaneous rigid E-unification.
Simultaneous rigid E-unification can be formulated as follows. Given equations
finite sets of equations find a substitution oe such
that
means provability in first-order logic
with equality). The corresponding instance of the simultaneous rigid E-unification
problem is denoted by the system of rigid equations
EXAMPLE 1.1. In this and further examples we shall often omit parentheses in
terms with unary function symbols, for example we write ffb instead of f(f(b)).
Assume that we want to prove the formula
several applications of
tableau expansion rules to the negation normal form of :' (ff-, fi- and fl-rules in
the terminology of (Smullyan, 1968; Fitting, 1990) we obtain the following tableau
(we only consider the part of the tableau containing literals, omitting non-literal
a ' b c ' d
Collecting formulas lying on the two branches in this tableau we obtain the
following two rigid equations expressing inconsistency of this tableau:
This system of rigid equations has one solution ffa=x; fb=y; fc=u; fd=vg. This
substitution can be found by applying the functional reflexivity rule and MGU
replacement rule of (Fitting, 1990) (in fact, the reformulation of the paramodulation
rule for tableaux). Obviously, this tableau cannot be closed without the use
of the functional reflexivity. 1
1 The system of clauses corresponding to this example improves a result proved in (Plaisted,
1995) by using a more complicated example. In this system of clauses
a
a
there is no refutation even by unrestricted rigid paramodulation (i.e. using non-ordered rigid
paramodulation and paramodulation into variables), while (Plaisted, 1995) gives an example
showing incompleteness of ordered rigid paramodulation only.
What You Always Wanted to Know About Rigid E-Unification 3
Since the invention of simultaneous rigid E-unification by (Gallier et al., 1987),
there have been a number of publications on simultaneous rigid E-unification itself
and its use in theorem proving, for example (Gallier et al., 1988; Gallier et al., 1989;
Gallier et al., 1990; Gallier et al., 1992; Baumgartner, 1992; Beckert and H-ahnle,
1992; Becher and Petermann, 1994; Beckert, 1994; Goubault, 1994; Petermann,
1994). Some of these articles were based on the conjecture that simultaneous rigid
E-unification is decidable. There were several faulty proofs of the decidability of
this problem (Gallier et al., 1988; Gallier et al., 1990; Goubault, 1994).
The refutation procedure for first-order logic with equality using simultaneous
rigid E-unification (Gallier et al., 1992) was based on a faulty assumption that
solutions to simultaneous rigid E-unification can be found by consecutive combination
of finite complete sets of solutions for (non-simultaneous) rigid E-unification
(Gallier et al., 1990; Gallier et al., 1988). Later, (Degtyarev and Voronkov, 1996d;
Degtyarev and Voronkov, 1996e) proved that simultaneous rigid E-unification is
undecidable, which implied that Gallier et.al.'s procedure cannot, in general, find
solutions to simultaneous rigid E-unification. However, it is not clear whether this
implies incompleteness of their procedure for first-order logic with equality: there
are examples when the procedure cannot find a solution for a given amplification in
spite that such a solution exists, but can find a solution for a bigger amplification.
Completeness of Gallier et.al.'s procedure or existence of a procedure complete for
first-order logic with equality based on some set of solutions to rigid E-unification
was an open problem (Petermann, 1994; Beckert, 1995). Our paper gives a positive
solution to this problem.
An advantage of Gallier et.al.'s procedure is that it allows one to extend the
proof-search technology developed for tableaux without equality to the case with
equality, using solutions to rigid E-unification instead of most general unifiers. In
particular, for a given amplification Gallier et.al.'s procedure always terminates.
A procedure of this kind is used in the theorem prover 3 T A P (H-ahnle et al., 1994,
R.H-ahnle, private communication).
In this paper we define a procedure extending the tableau method to logic with
equality based on an incomplete procedure for rigid E-unification. Nevertheless,
our procedure is complete for first-order logic with equality. Hence, we rehabilitate
Gallier et.al.'s program for adding equality to semantic tableaux. Moreover, our
procedure solves rigid equations laying on different tableau branches independent-
ly. This strongly improves Gallier et.al.'s procedure which uses solutions of some
rigid equations to solve rigid equations on other branches.
A similar approach has already been defined in (Kanger, 1983) based on a more
straightforward way of variable instantiation. As a method for finding a closing
substitution, Kanger proposed an algorithm which can now be characterized as
an incomplete (but terminating) algorithm for simultaneous rigid E-unifiability.
Variables in a matrix (or a tableau) could be consecutively substituted by ground
terms already occurring in the matrix. This procedure does not solve simultaneous
rigid E-unifiability, but it gives a procedure complete for first-order logic with
total.tex - Date: June 3, 1997
4 Anatoli Degtyarev and Andrei Voronkov
equality. In the terminology of (Fitting, 1990) it means that a closing substitution
can be found after a sufficiently high (but not necessarily minimal) number of
applications of the fl-rule. The approach to substitutions based on this idea has
been characterized as minus-normalization in (Matulis, 1963; Maslov, 1967).
However, for a language with function symbols minus-normalization is interesting
mostly theoretically. Even in simplest cases, minus-normalization requires
a huge number of instantiations. For example, in the tableau of Example 1.1, we
have to consider 8 4 possible instantiations of variables x; by terms in the
set fa; b; c; d; fa; f b; f c; fdg. Moreover, it has been proved that the use of minus-
normalization can lead to considerable growth of derivations. Some results on
minus-normalization are proved by (Norgela, 1974).
In this paper we describe a logical calculus BSE for rigid E-unification based
on the rigid basic superposition rule that is an adaptation of basic superposition
of (Bachmair et al., 1992; Nieuwenhuis and Rubio, 1992), for "rigid" variables. For
a given rigid E-unification problem (called rigid equation in this paper), there is
only a finite number of BSE-derivations for this problem. Thus, BSE gives us an
algorithm returning a finite set of solutions to this rigid equation. We use these
solutions to close a tableau branch in the same way as most general unifiers are
used to close a branch in the MGU atomic closure rule of (Fitting, 1990).
Preliminaries
We present here a brief overview of notions and preliminary definitions necessary
for understanding the paper. We assume basic knowledge of substitutions and
unification.
Let \Sigma be a signature, and X be a set of variables. T (\Sigma; X) denotes the set of
all terms in the signature \Sigma with variables from X. The set of all ground terms
in the signature \Sigma is denoted by T (\Sigma).
A literal is either an atomic formula or a negation of an atomic formula. An
equation is a literal s ' t, where s; t 2 T (\Sigma; X). We do not distinguish equations
Literals of the form :(s ' t) are denoted by s 6' t and called
disequations. For simplicity, we assume that ' is the only predicate symbol of our
first-order language. As usual, arbitrary first-order languages can be represented in
such language by introducing a sort bool and replacing any non-equational atom
A by A ' true (for details see e.g. Bachmair et al., 1995).
By a ground expression (i.e. term or literal) we mean an expression containing
no variables. For any expression E, var(E) denotes the set of all variables occurring
in E. For a sequence of variables -
x, we shall sometimes denote - x also the corresponding
set of variables. We write A[s] to indicate that an expression A contains
s as a subexpression and denote by A[t] the result of replacing this occurrence of
s in A by t. By Aoe we denote the result of applying the substitution oe to A. If A
is a formula, we can as usual rename bound variables in A before applying oe. We
total.tex - Date: June 3, 1997
What You Always Wanted to Know About Rigid E-Unification 5
shall denote '(x) a formula ' with zero or more free occurrences of a variable x
and write '(t) to denote the formula 'ft=xg.
A substitution ' whose domain is a subset of fx is denoted
A substitution oe is called grounding for a set of variables V if for every variable
the term voe is ground.
be two substitutions with disjoint domains, The union of ' 1 and
is the substitution oe defined as follows. For every variable v we
have
Note that we use the union notation only for substitutions with disjoint
domains.
The inference systems used in this paper are defined with respect to a reduction
ordering, denoted by - which is total on ground terms. Our results are valid for
any such ordering.
A formula is in the Skolem negation normal form if it is constructed from
literals using the connectives - and the quantifier 8. There is a satisfiability-
preserving structure-preserving translation of formulas without equivalences into
formulas in Skolem negation normal form consisting of the standard skolemization
and a translation into negation normal form used e.g. in (Andrews, 1981). In order
to prove an arbitrary formula ', we translate :' in Skolem negation normal form
obtaining a formula / and try to establish unsatisfiability of /. For this reason,
theorems in this paper are formulated in terms of unsatisfiability.
For an equation s ' t and a multiset of equations E we write E ` s ' t to
denote that the formula ( V
is provable in first-order logic with
equality. For such formulas provability can be tested by the congruence closure
algorithm (Shostak, 1978). For the inclusion of multisets we shall use notation
3 Rigid basic superposition
The term "rigid paramodulation" has already been used in (Becher and Peter-
mann, 1994; Plaisted, 1995) for systems of inference rules in which all variables
are treated as "rigid". For example, rigid clause paramodulation of (Plaisted, 1995)
is essentially paramodulation and resolution over a set of clauses, where all substitutions
are applied to the whole set of clauses. A similar system for resolution has
been proposed earlier in (Chang, 1972) as V-resolution and in (Lee and Chang,
for resolution with paramodulation as V-resolution and V-paramodulation.
6 Anatoli Degtyarev and Andrei Voronkov
We shall use the term "rigid basic superposition" to denote a "rigid" version of
basic superposition. We formalize rigid basic superposition using constraints that
is close to the presentation of (Nieuwenhuis and Rubio, 1995).
DEFINITION 3.1 (Constraints). By an (ordering) constraint we mean a set of
expressions which can be of two kinds: an equality constraint s ' t, or an inequality
constraint s - t, where s; t are terms. A substitution ' is a solution to a constraint
(respectively, a constraint s - t) if ' is grounding for
coincides with t' (respectively, s' - t').
A substitution ' is a solution to a constraint C if ' is a solution to every equality
or inequality constraint in C. A constraint C is satisfiable if it has a solution.
Constraints C 1 and C 2 are called equivalent if they have the same sets of solutions.
We assume that there is an effective procedure for checking constraint satisfiability.
For example, there are efficient methods for solving ordering constraints for lexicographic
path orderings given by (Nieuwenhuis, 1993; Nieuwenhuis and Rubio,
1995).
DEFINITION 3.2. A rigid equation is an expression of the form E ' 8 s ' t,
where E is a finite multiset of equations and s; t are terms. Its solution is any
substitution ' such that E' ' s' ' t' 2 .
Below we shall introduce a system BSE for solving rigid equations. The derivable
objects of BSE are constraint rigid equations:
DEFINITION 3.3 (Constraint rigid equation). A constraint rigid equation is a
pair consisting of a rigid equation R and a constraint C. Such a constraint rigid
equation will be denoted R \Delta C.
DEFINITION 3.4 (Calculus BSE). The calculus BSE of constraint rigid equations
consists of the following inference rules:
Left rigid basic superposition:
(lrbs)
Right rigid basic superposition:
2 The term "rigid equation" could be more adequately expressed as "instance of a (non-
simultaneous) rigid E-unification problem", but this would be too lengthy.
What You Always Wanted to Know About Rigid E-Unification 7
Equality resolution:
Application of the rules is restricted to the following conditions:
1. The constraint at the conclusion of the rule is satisfiable;
2. The right-hand side of the rigid equation at the premise of the rule does not
have the form q ' q.
3. In the basic superposition rules, the term p is not a variable.
4. In the left basic superposition rule, s[r] 6= t.
The basic restriction in BSE is formalized by representing most general unifiers
through equality constraints. Condition 1 has two purposes. The satisfiability of
equations in constraints is needed to preserve correctness of the method. The
satisfiability of inequality constraints is needed to ensure termination (Theorem 3.9
below). Conditions 3-4 are not essential, they are added as standard optimizations
used in paramodulation-based methods. Condition 2 prohibits to apply any rules
to rigid equations of the form E ' 8 q ' q.
We denote by R \Delta C the fact that R 0 \Delta C 0 is obtained from R \Delta C by
an application of one of the inference rules of BSE. The symbol ;   denotes the
reflexive and transitive closure of ;.
3.5. Consider the rigid equation ha ' a; hx ' a; hb ' fy ` 8 y '
gfy. The ordering - is the Knuth-Bendix ordering (see Martin, 1987) in which all
weights of symbols are equal to 1 and which uses the precedence relation f ? h ?
a. Under this ordering we have ht - a and f t - hb for every ground term t.
The following is a BSE-derivation for this rigid equation:
fy ` 8 y ' gfy
fy ` 8 y ' ghb \Delta ffy - hb; gfy - fy ' fyg
fy ` 8 y ' ga
\Deltaff y - hb; gfy - fy ' fy; hx - a; ghb -
fy ' fy; hx - a; ghb -
By using constraint simplification, i.e. replacement of constraints by equivalent
"more simple" constraints we can rewrite this derivation as
fy ` 8 y ' gfy
fy ` 8 y ' ghb
fy ` 8 y ' ga \Delta fghb -
8 Anatoli Degtyarev and Andrei Voronkov
THEOREM 3.6 (Soundness of BSE). Let R substitution
satisfying C is a solution to R. In particular, R is solvable.
Proof. For any constraint C, denote by C ' the constraint obtained from C be
removing all inequality constraints. First we note that for every application of
an inference rule of BSE of the
By induction on the number of inference steps and using
the fact C i ' C i+1 , we prove the same statement for multi-step derivations
Let R have the form E Applying the obtained statement to the
multi-step derivation R t.
Hence, any solution to C. We have
Any constraint in C ' ` has the form u ' u. Hence,
solution to
This theorem leads to the following definition:
DEFINITION 3.7 (Answer constraint). A constraint C is called an answer constraint
for a rigid equation R if for some rigid equation
We note that BSE is an incomplete calculus for solving rigid equations. It
means that there are solvable rigid equations R that have no answer constraint.
For instance, consider the rigid equation 3 x ' a ` 8 gx ' x. It has one solution
fga=xg. However, no rule of BSE is applicable to x ' a ` 8 gx ' x \Delta ;.
This means that BSE can yield less solutions to a rigid equation than any other
known procedure, for example that of (Gallier et al., 1992) because all these procedures
are existentially complete. At the same time, BSE can yield more solutions
than the procedure of (Gallier et al., 1992) as the following example shows. For
the rigid equation a ' fa ` 8 x ' fa the procedure of (Gallier et al., 1992) will
find one solution fa=xg, but there are two answer constraints whose solutions are
the substitutions fa=xg and ffa=xg respectively.
In order to show that there is only finite number of derivations in BSE from a
given constraint rigid equation, we prove an auxiliary statement.
be an infinite sequence of terms in a finite signature all
whose variables belong to a finite set. Then there are numbers
and the constraint t i - t j is unsatisfiable.
Proof. Following (Kruskal, 1960) we introduce a partial ordering - on terms as
the smallest reflexive and transitive relation satisfying
1.
2. if s - t then r[s] - r[t].
3 Suggested by G.Becher (private communication).
What You Always Wanted to Know About Rigid E-Unification 9
By Kruskal's Tree Theorem (Kruskal, 1960) there exist
It is easy to see that the constraint t i - t j is unsatisfiable.
Similar statements have been proven in (Dershowitz, 1982; Plaisted, 1986).
THEOREM 3.9 (Termination of BSE). For any constraint rigid equation R \Delta C,
there exists a finite number of derivations from R \Delta C.
Proof. Suppose that there exists an infinite number of derivations from R \Delta C.
Then, by K-onig's lemma there exists an infinite derivation R \Delta
consisting of superpositions. Consider any application of superposition
it have the form
(lrbs)
(the case of right rigid basic superposition is similar). We prove that for every
the constraint C n is equivalent to C n [fs[p] - s[r]g. Indeed, the constraint
(and hence the constraint C n ) contains pg. By the definition of
reduction orderings, if p - r, then s[p] - s[r]. This implies that C n is equivalent
to s[r]g.
Since every application of rigid basic superposition replaces a literal s[p] '
t (or s[p] 6' t) in R i by a literal s[r] ' t (respectively, s[r] 6' t), there is an
infinite sequence of terms t and an increasing sequence of natural numbers
with the following property. For every positive natural number k the
constraint C n k
is equivalent to C n k
. Since all terms t k are in the same
finite signature and have variables in the same finite set, by Lemma 3.8, there are
and the constraint t
for
all k - j, the constraint C n j
is equivalent to C n j
, for all k - j. Hence,
the constraint is equivalent to C n j . Thus, C is
satisfiable. But satisfiability of C implies satisfiability of t i - t j . Contradiction.
Note. In (Degtyarev and Voronkov, 1996f) the left rigid basic superposition has
been formulated incorrectly in the following way:
(lrbs)
With this formulation, termination is not guaranteed as the following example
shows. Consider the rigid equation fgx ' gx; gx ' a ' 8 a ' b and arbitrary
reduction ordering - total on ground terms. The following is an infinite sequence
of applications of (lrbs):
ag
(lrbs)
\Deltafgx ' gx; fgx - gx; gx - a; gx - fag
(lrbs)
ag
It is easy to see that the constraint
ag
is satisfied by the substitution ff a=xg.
Inequality constraints are not needed for soundness or completeness of our
method. The pragmatics behind inequality constraints is to ensure that the search
for solutions of a rigid equation is finite. In addition, the use of ordering constraints
prunes the search space.
To illustrate this theorem, we consider Example 3.5. The rigid equation of this
example has an infinite number of solutions including fb=x; gh n a=yg, for every natural
number n. However, all possible BSE-derivations starting with ha ' a; hx '
fy ` 8 y ' gfy \Delta ; give only two answer constraints, one is
ffy - hb; gfy - fy ' fy; hx - a; ghb -
shown in Example 3.5, another is ffy - hb; gfy - fy ' fy; y ' ghbg obtained
from the following derivation:
fy ` 8 y ' gfy
fy ` 8 y ' ghb \Delta ffy - hb; gfy - fy ' fyg
fy ' fy; y ' ghbg
This answer constraint can be simplified to fy ' ghbg.
Theorem 3.9 yields
THEOREM 3.10. Any rigid equation has a finite number of answer constraints.
There is an algorithm giving for any rigid equation R the set of all answer constraints
for R.
What You Always Wanted to Know About Rigid E-Unification 11
In the rules (fl) the variable y does not occur in the premise.
Fig. 1. Tableau Expansion Rules
4 Answer constraints and the tableau method
In this section we consider how to use the system BSE for theorem proving by the
tableau method. Since we only consider skolemized formulas, we have no ffi-rules
in tableau calculi.
DEFINITION 4.1 (Branch and tableau). A branch is a finite multiset of formulas.
A tableau is a finite multiset of branches. A tableau with branches
be denoted by \Gamma . The tableau with is called the empty tableau
and denoted by #.
Often, tableaux are represented in tree form. Representation of tableaux as
multisets of branches is more convenient for us for several reasons. For this representation
we introduce a logical system allowing to expand tableaux:
DEFINITION 4.2 (Tableau expansion rules). The rules (ff), (fi) and (fl) of Figure
are called tableau expansion rules.
DEFINITION 4.3. Let \Gamma be a branch of a tableau. The set of rigid equations on
\Gamma is defined in the following way. A rigid equation t is on \Gamma if E is the
multiset of all equations in \Gamma and (s 6' t) 2 \Gamma.
We extend the notion of answer constraints to tableau branches:
DEFINITION 4.4. A constraint C is an answer constraint for a tableau branch \Gamma
if C is an answer constraint for some rigid equation on \Gamma.
By Theorem 3.10, we obtain
THEOREM 4.5. Any tableau branch has a finite number of answer constraints.
There is an algorithm which for any tableau branch \Gamma computes the set of all
answer constraints for \Gamma.
The following theorem states soundness and completeness of the tableau method
with answer constraints:
THEOREM 4.6 (Soundness and completeness). Let - be a sentence in Skolem negation
normal form. Then - is unsatisfiable if and only if there is a
obtained from - by tableau expansion rules and answer constraints C
respectively, such that
Proof. Soundness follows from soundness of BSE .
The proof of completeness is quite lengthy and is given in Appendix A. It
is based on the completeness of the equality elimination method (Degtyarev and
Voronkov, 1994; Degtyarev and Voronkov, 1995a; Degtyarev and Voronkov, 1996b).
To illustrate this theorem, consider the formula of Example 1.1. Assume that
we want to prove the formula
d oe g(u; x; y) ' g(v; fa; fb))). The negation normal form of :- is 8xyzu((a '
The ordering - is the lexicographic path ordering (see e.g. Nieuwenhuis and
Rubio, 1995) based on the precedence g ? f ? a d. For purely
illustrative purpose, we shall display tableaux in the tree form. After one quantifier
duplication (application of a fl-rule) and some other tableau expansion rules we
obtain the following tableau:
a ' b c ' d
There is one rigid equation on each branch of the tableau:
Rigid basic superposition is applicable to none of this rigid equations. Rigid equation
(1) has one answer constraint fg(x; u; v) ' g(y; f c; fd)g obtained by an application
of the equality resolution rule:
Similarly, rigid equation (2) has one answer constraint fg(u; x; y) ' g(v; fa; fb)g.
The union of these constraints fg(x; u; v) ' g(y; f c; fd); g(u; x; y) ' g(v; fa; fb)g is
total.tex - Date: June 3, 1997
What You Always Wanted to Know About Rigid E-Unification 13
unsatisfiable. Thus, our method does not find solution after one quantifier dupli-
cation. After three quantifier duplications and some other tableau expansion steps
we obtain the following tableau:
a ' b c ' d
a ' b c ' d
a ' b
It has four branches:
Consider the following rigid equations R 1 -R 4 on the branches \Gamma 1 -\Gamma 4 , respectively

We can apply the following BSE-derivations to R 1
a ' b; a ' b ' 8
a
a
14 Anatoli Degtyarev and Andrei Voronkov
a
a
ag
The union of the answer constraints of these derivations is
a - b; a ' a;
This constraint is satisfiable. To check this, we can consider the following substitution

5 Tableau basic superposition
As a simple consequence of our results, we prove a completeness result for a
paramodulation rule working on tableaux. A paramodulation rule working directly
on tableaux was proposed in (Loveland, 1978) in the context of model elimination
and later in (Fitting, 1990). However, their formulations have all disadvantages of
the early paramodulation rule of (Robinson and Wos, 1969):
1. Functional reflexivity rule is used;
2. Paramodulation into variables is allowed;
3. Increasing applications of paramodulation are allowed (for example, x can be
rewritten to f(x).
As a consequence, for a given tableau expansion there may be an infinite sequence
of paramodulations, in particular due to the use of functional reflexivity or increasing
applications of paramodulation. Since the publication of the book (Loveland,
1978), no improvements of the paramodulation-based tableau calculi have been
described except for (Plaisted, 1995) who has shown how to transform derivations
with resolution and paramodulation to tableaux by introducing a tableau factoring
rule.
Here we show that paramodulation is complete under the following restrictions:
What You Always Wanted to Know About Rigid E-Unification 15
1. No functional reflexivity is needed;
2. Paramodulation into variables is not allowed;
3. Orderings are used so that there are no increasing applications of paramodulation

4. Basic restriction on paramodulation prohibits paramodulation into terms introduced
by unification.
All these refinements are a consequence of our main result (Theorem 4.6).
In order to formalize the basic strategy, we keep the substitution condition as
a set of constraints, as before. Thus, we work with constraint tableaux:
DEFINITION 5.1 (Constraint tableau). A constraint tableau is a pair consisting
of a tableau T and a constraint C, denoted T \Delta C.
Now we adapt the tableau rules of (Fitting, 1990) to the case of constraint
tableaux. For simplicity, we only consider signatures whose only predicate symbol
is '. When we prove a formula ', we construct the Skolem negation normal form
/ of :' and, starting with the constraint tableau / try to derive the empty
tableau # with some satisfiable constraint.
DEFINITION 5.2 (Calculus T BSE). The free-variable tableau calculus T BSE
is shown in Figure 2.
DEFINITION 5.3 (Constraint tableau expansion rules). The rules (ff), (fi) and
(fl) of T BSE are called constraint tableau expansion rules.
The calculus T BSE has the required completeness property:
THEOREM 5.4 (Soundness and completeness). Let ' be a formula in the Skolem
negation normal form. It is unsatisfiable if and only if there is a derivation from
the constraint tableau ' \Delta ; of a constraint tableau # \Delta C.
Proof. Straightforward from Theorem 4.6 by noting that the rules of BSE can
be simulated by the corresponding tableau rules.
This logical system has one more pleasant property:
THEOREM 5.5 (Termination). For any constraint tableau T \Delta C there is only a
finite number of derivations from T \Delta C not using constraint tableau expansion
rules.
(lrbs)
In the rules (fl) the variable y does not occur in the premise. The conditions on
the rules (lrbs) and (rrbs) are the same as for the corresponding rules of BSE.
Fig. 2. Calculus T BSE
Proof. Similar to that of Theorem 3.9.
This means, that for a given amplification, we cannot have infinite search. Infinite
search without any expansion steps is possible in Fitting's system.
To illustrate the connection between the tableau rigid basic superposition rule
and rules of BSE, we reconsider the example of Section 4. On the branch containing
the literal g(x fd) and the equation c ' d, we can apply rigid
basic superposition that adds g(x fd) to the branch. Similarly,
we can apply rigid basic superposition to the branch containing
This results in the
tableau given in Figure 3 (the picture does not include the constraint, it is discussed
below).
After four application of the (er) rules all branches of this tableau become
closed. The resulting constraint of this derivation is the same as the union of the
answer constraints shown at the end of Section 4.
6 Related work
The problem of extending tableaux with equality rules is crucial for enriching the
deductive capabilities of the tableau method. Despite the fact that this problem
has been attacked by a growing number of researchers during the last years, known
solutions are not yet convincing. At the same time tableau methods of automated
deduction play an important role in various areas of artificial intelligence and
computer science - see e.g. special issues of the Journal of Automated Reasoning,
v. 13, no. 2,3, 1994. These issues contain a survey (Schumann, 1994) of implemen-
What You Always Wanted to Know About Rigid E-Unification 17
a ' b c ' d
a ' b c ' d
a ' b
Fig. 3.
tations of tableau-based provers. Among 24 systems mentioned in the survey only
two are able to handle equality.
The systems PROTEIN (Baumgartner and Furbach, 1994) and KoMeT (Bibel
et al., 1995) implement the modification method of (Brand, 1975). This method
transforms a set of clauses with equality into a set of clauses without equality.
This transformation usually yields a considerably larger set of clauses. In partic-
ular, the symmetry and the transitivity axioms must be explicitly applied to all
positive occurrences of the equality predicate. Recently, (Degtyarev and Voronkov,
1996c) proposed a new translation method based on the so-called basic folding
demonstrated for Horn clauses.
According to (Schumann, 1994), the system 3 T A P uses the method of (Beckert
and H-ahnle, 1992). Paper (Beckert and H-ahnle, 1992) claims the completeness of
the method, but this claim is not true. The method expands the tableau using
the standard tableau rules, including fl-rules. For finding a closing substitution,
an analogue of linear paramodulation without function reflexivity has been pro-
posed. As it is well known, linear paramodulation is incomplete without function
reflexivity. The same is true for the method of (Beckert and H-ahnle, 1992), as the
following example shows. Suppose that we prove the formula 9x(a ' b-g(fa; fb) '
In order to prove it using paramodulation, we need
to paramodulate a ' b into g(fa; fb) ' h(fa; fb). The method of (Beckert and
H-ahnle, 1992) only allows for paramodulation into copies of g(x; x) ' h(x; x)
obtained by applications of the fl-rule. Thus, this (provable) formula cannot be
proved using the method of (Beckert and H-ahnle, 1992).
Consider now approaches based on simultaneous rigid E-unifiability by (Gallier
et al., 1987; Gallier et al., 1992) and related methods. We do not consider numerous
total.tex - Date: June 3, 1997
works dedicated to (non-simultaneous) rigid E-unifiability. This problem is NP-complete
and there exist a number of complete algorithms for its solution (Gallier
et al., 1988; Gallier et al., 1990; Goubault, 1993; Becher and Petermann, 1994;
De Kogel, 1995; Plaisted, 1995). Since simultaneous rigid E-unification is undecidable
(Degtyarev and Voronkov, 1996d; Degtyarev and Voronkov, 1996e), these
completeness results are useless from the viewpoint of general purpose theorem
proving as proposed in (Gallier et al., 1987; Gallier et al., 1992). Our system BSE
can easily be extended to a calculus complete for rigid E-unifiability, but such
completeness is not our aim. We tried to restrict the number of possible BSE-
derivations preserving completeness of the general-purpose method of Section 4.
It is not known whether the procedure described in (Gallier et al., 1992) is
complete for theorem proving 4 . Even if it is complete, our procedure based on
BSE has some advantages over Gallier et.al.'s procedure. For example, for every
tableau branch with p equations and q disequations, we consider q rigid equations,
while Gallier et.al.'s procedure checks q \Delta 2 p rigid equations.
(Gallier et al., 1988; Gallier et al., 1990) introduced the notion of a complete
set of solutions for rigid E-unification, proved finiteness of such sets and gave
an algorithm computing finite complete set of solutions. According to this result,
(Goubault, 1994) proposed to solve simultaneous rigid E-unifiability by using finite
complete sets of solutions to the components of the simultaneous problem. Paper
(Goubault, 1994) contained faulty results. The undecidability of simultaneous rigid
E-unification shows that finite complete sets of solutions do not give a solution to
the simultaneous problem. The reason for this is that substitutions belonging to
complete sets of solutions for different rigid equations are minimal modulo different
congruences.
(Petermann, 1994) introduces a "complete connection calculus with rigid E-
unification". Here the completeness is achieved by changing the notion of a complete
set of unifiers so that solutions to all subproblems are compared modulo
the same congruence (generated by the empty equality theory). In this case,
a non-simultaneous problem can have an infinite number of solutions and no
finite complete set of solutions. For example, for the rigid E-unification problem
f(a) ' a ` 8 x ' a the complete set of solutions in the sense of (Gallier et al.,
1992) consists of one substitution fa=xg (and there is only one answer constraint
ag obtained by our method), but the complete set of solutions in the sense
of (Petermann, 1994) is infinite and consists of substitutions ff n (a)=xg, for all
:g. This implies that proof-search by the method of (Petermann, 1994)
can be non-terminating even for a limited number of applications of the fl-rule
(i.e. for a particular tableau), unlike algorithms based on the finite complete sets
of unifiers in the sense of (Gallier et al., 1992) or based on minus-normalization
(Kanger, 1983). The implementation of the method of (Petermann, 1994) uses a
completion-based procedure by (Beckert, 1994) of generation of complete sets of
4 For example, the completeness of Gallier et.al.'s procedure does not follow from our method
because, as noted above, our calculus BSE can give more solutions to some rigid equations.
What You Always Wanted to Know About Rigid E-Unification 19
rigid E-unifiers. This procedure is developed with the aim of solving a more general
problem - so-called mixed E-unification and has been implemented as part of the
tableau-based theorem prover 3 T A P . Complete sets of unifiers both in the sense
of (Gallier et al., 1992) and in the sense of (Petermann, 1994) can be computed
by this procedure in the case when all variables are treated as rigid. However, the
termination is not guaranteed even for complete sets of rigid E-unifiers in the sense
of (Gallier et al., 1992).
(Plaisted, 1995) gives "techniques for incorporating equality into theorem prov-
these techniques have a rigid flavor". His method of path paramodulation guarantees
termination for a given amplification and, in the case of success "solves
the simultaneous rigid E-unification problem, in a sense". However, this does not
solve the problem attacked by a number of researchers: extend the method of
matings to languages with equality by rigid E-unification. First, unlike (Gallier
et al., 1992) the search for solutions for a given amplification is not incremental
(the method does not allow "branch-wise" computation of solutions to rigid E-
unification for separate branches). Second, within a given amplification Plaisted
uses factoring rules which involves two branches (paths). As a consequence, even
when the original formula contains no equality, his method results in the standard
tableau calculus plus the factoring rule.
In fact, path paramodulation of (Plaisted, 1995) simulates resolution-paramodu-
lation inference in a connection-like calculus. Although it is not noted in (Plaisted,
1995), this technique has been demonstrated for resolution in many papers, for
example in (Bibel, 1981; Eder, 1988; Eder, 1991; Mints, 1990; Baumgartner and
Furbach, 1993; Avron, 1993). The generalization of this simulation to paramodulation
is straightforward.
However, this simulation technique is insufficient for proving the results of our
paper since, in particular, it gives no insight on how to avoid factoring in tableaux
with equality. The use of factoring prevents not only from the independent search
for solutions for tableau branches, but even from the incremental solving of rigid
equations on tableau branches as proposed by Gallier et.al.
Our equality elimination method (Degtyarev and Voronkov, 1996b; Degtyarev
and Voronkov, 1995b; Degtyarev and Voronkov, 1995a) is based on extending a
tableau prover by a bottom-up equation solver using basic superposition. Solutions
to equations are generated by this solver and used to close branches of a tableau.
Thus, the method combines (non-local) tableau proof search with the (local) equation
solving. Only completely solved equations are used in the tableau part of the
proof, thus reducing non-determinism created by applications of the MGU replacement
rule of (Fitting, 1990). The equation solution is even more restricted by the
use of orderings, basic simplification and subsumption.
A similar idea: combination of proof-search in tableaux with a bottom-up equality
saturation of the original formula is used in (Moser et al., 1995) for constructing
a goal-directed version of model elimination and paramodulation.
One of advantages of the tableau method is its applicability to non-classical
logics. However, handling equality in non-classical logics seems to be a much more
difficult problem than that in classical logic. For example, it is shown in (Voronkov,
1996) that procedures for intuitionistic logic with equality must handle simultaneous
rigid E-unification. This implies that our method based on BSE does not give a
complete procedure for intuitionistic logic with equality. Other results on relations
between simultaneous rigid E-unification and intuitionistic logic are considered in
(Degtyarev and Voronkov, 1996a; Degtyarev et al., 1996a; Degtyarev et al., 1996b;
Veanes, 1997).
An extensive discussion of equality reasoning in sequent-based systems may be
found in (Degtyarev and Voronkov, 1997).

Acknowledgments

We thank Gerard Becher and Uwe Petermann for helpful discussions, anonymous
referees for their valuable comments and the guest editors Jose Julio Alves Alferes
and Luis Moniz Pereira for their patience.



--R

Theorem proving via general matings.

Basic paramodulation and superposition.

Basic paramodulation.
Consolution as a framework for comparing calculi.
PROTEIN: A PROver with a Theory Extension INterface.

An ordered theory resolution calculus.
Rigid unification by completion and rigid paramodulation.
An improved method for adding equality to free variable semantic tableaux.
A completion-based method for mixed universal and rigid E-unification

Issues in theorem proving based on the connection method.
On matrices with connections.
Proving theorems with the modification method.
Theorem proving with variable-constrained resolution
Rigid E-unification simplified
Equality elimination for semantic tableaux.
Equality elimination for the inverse method and extension proce- dures
General connections via equality elimination.
Decidability problems for the prenex fragment of intuitionistic logic.
Equality elimination for the tableau method.

Handling equality in logic programs via basic folding.
Simultaneous rigid E-unification is undecidable
The undecidability of simultaneous rigid E-unification
What you always wanted to know about rigid E-unification
Equality reasoning and sequent-based methods
Simultaneous rigid E-unification and related algorithmic problems
"Logic in Computer Science"
Orderings for term rewriting systems.
Consolution and its relation with resolution.
First Order Logic and Automated Theorem Proving.
Theorem proving using rigid E-unification: Equational matings
IEEE Computer Society Press
Rigid E-unification is NP-complete
Rigid E-unification and its applications to equational matings
Rigid E-unification: NP-completeness and applications to equational matings
Theorem proving using equational matings and rigid E-unification


The many-valued tableau-based theorem prover 3 T A P
Technical Report 30/94
A simplified proof method for elementary logic.
Well quasi ordering
Symbolic Logic and Mechanical Theorem Proving.
Automated Theorem Proving: a Logical Basis.
How to choose weights in the Knuth-Bendix ordering
Invertible sequential variant of constructive predicate calculus (in Russian).
On variants of classical predicate calculus with the unique deduction tree (in Russian).

Model elimination with basic ordered paramodula- tion
Basic superposition is complete.
Theorem proving with ordering and equality constrained clauses.
Journal of Symbolic Computations

On the size of derivations under minus-normalization in Russian
A complete connection calculus with rigid E-unification
A simple non-termination test for the Knuth-Bendix method
Special cases and substitutes for rigid E-unification
An improved proof procedure.
Paramodulation and theorem-proving in first order theories with equality

An algorithm for reasoning about equality.

On Simultaneous Rigid E-Unification
Proof search in intuitionistic logic with equality
--TR
equality reasoning;tableau method;rigid E-unification