English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Special cases and substitutes for rigid $E$-unification

MPS-Authors
/persons/resource/persons45200

Plaisted,  David
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

95-2-010.pdf
(Any fulltext), 37MB

Supplementary Material (public)
There is no public supplementary material available
Citation

Plaisted, D.(1995). Special cases and substitutes for rigid $E$-unification (MPI-I-1995-2-010). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-A1B5-9
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).