Catalogo Articoli (Spogli Riviste)

OPAC HELP

Titolo:
Special cases and substitutes for rigid E-unification
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:
0938-1279(200001)10:2<97:SCASFR>2.0.ZU;2-R
Fonte:
ISI
Lingua:
ENG
Soggetto:
EQUATIONAL MATINGS; COMPLETENESS;
Keywords:
theorem proving; equality; unification; rigid E-unification; decidability; tableaux; horn clauses; first-order 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 E-unification", APPL ALG EN, 10(2), 2000, pp. 97-152

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 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 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).

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