Automated Deduction - A Basis for Applications

Bernhard Beckert

Rigid E-unification


By replacing syntactical unification with rigid E-unification, equality
handling can be added to rigid variable calculi for first-order logic,
including free variable tableau, the mating method, the connection
method, and model elimination.

Ground E-unification (i.e., E-unification with variable-free equalities)
has long been known to be decidable. and classical universal
E-unification has long been known to be undecidable.  Rigid
E-unification is in between: It is decidable in the simple,
non-simultaneous case, but it is undecidable whether there is a
simultaneous solution for several rigid E-unification problems, which is
unfortunate as simultaneous rigid E-unification is of great importance
for handling equality in automated theorem proving.

In this chapter, we describe the basic idea of rigid E-unification and
its importance for adding equality to rigid variable calculi and
introduce syntax and semantics of first-order logic with equality.  We
formally define (non-simultaneous) rigid E-unification and the notion of
(minimal) complete sets of unifiers; and we briefly sketch proofs for
the decidability of ground E-unification and - based on this - for rigid
E-unification; methods for solving rigid E-unification problems are
compared.  The problem of finding a simultaneous solution for several
rigid E-unification problems is discussed; and mixed E-unification is
introduced, that is a combination of classical and rigid
E-unification. Using the example of free variable semantic tableaux, we
show how rigid E-unification can be used to handle equality in a free
variable calculus. Finally, we briefly summarize the properties of the
different types of E-unification.