Catalogo Articoli (Spogli Riviste)
OPAC HELP
Titolo: Special cases and substitutes for rigid Eunification
Autore: Plaisted, DA;
 Indirizzi:
 Univ N Carolina, Dept Comp Sci, Chapel Hill, NC 27599 USA Univ N CarolinaChapel Hill NC USA 27599 p Sci, Chapel Hill, NC 27599 USA
 Titolo Testata:
 APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING
fascicolo: 2,
volume: 10,
anno: 2000,
pagine: 97  152
 SICI:
 09381279(200001)10:2<97:SCASFR>2.0.ZU;2R
 Fonte:
 ISI
 Lingua:
 ENG
 Soggetto:
 EQUATIONAL MATINGS; COMPLETENESS;
 Keywords:
 theorem proving; equality; unification; rigid Eunification; decidability; tableaux; horn clauses; firstorder logic;
 Tipo documento:
 Article
 Natura:
 Periodico
 Settore Disciplinare:
 Engineering, Computing & Technology
 Citazioni:
 23
 Recensione:
 Indirizzi per estratti:
 Indirizzo: Plaisted, DA Univ N Carolina, Dept Comp Sci, Chapel Hill, NC 27599 USA Univ N Carolina Chapel Hill NC USA 27599 Hill, NC 27599 USA



 Citazione:
 D.A. Plaisted, "Special cases and substitutes for rigid Eunification", APPL ALG EN, 10(2), 2000, pp. 97152
Abstract
The simultaneous rigid Eunification problem arises naturally in theorem proving with equality. This problem has recently been shown to be undecidable. This raises the question whether simultaneous rigid Eunification can usefully be applied to equality theorem proving. We give some evidence in theaffirmative, 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 Eunification 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).
ASDD Area Sistemi Dipartimentali e Documentali, Università di Bologna, Catalogo delle riviste ed altri periodici
Documento generato il 02/12/20 alle ore 07:39:35