MPI-I-95-2-010
Special cases and substitutes for rigid $E$-unification
Plaisted, David A.
November 1995, 46 pages.
.
Status: available - back from printing
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).
-
95-2-010.pdf
- Attachement: MPI-I-95-2-010.dvi.gz (85 KBytes); MPI-I-95-2-010.ps.gz (140 KBytes); 95-2-010.pdf (37318 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1995-2-010
BibTeX
@TECHREPORT{Plaisted95,
AUTHOR = {Plaisted, David A.},
TITLE = {Special cases and substitutes for rigid $E$-unification},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-95-2-010},
MONTH = {November},
YEAR = {1995},
ISSN = {0946-011X},
}