hide
Free keywords:
-
Abstract:
The simultaneous rigid $E$-unification problem arises
naturally in theorem proving with equality. This problem has recently
been shown to be undecidable. This raises the question whether
simultaneous rigid $E$-unification can usefully be applied to equality
theorem proving. We give some evidence in the affirmative, by presenting a
number of common special cases in which a decidable version of this
problem suffices for theorem proving with equality. We also present
some general decidable methods of a rigid nature that can be used for
equality theorem proving and discuss their complexity. Finally, we
give a new proof of undecidability of simultaneous rigid
$E$-unification which is based on Post's Correspondence Problem, and
has the interesting feature that all the positive equations used are
ground equations (that is, contain no variables).
