Catalogo Articoli (Spogli Riviste)

OPAC HELP

Titolo:
THE UNDECIDABILITY OF SIMULTANEOUS RIGID E-UNIFICATION
Autore:
DEGTYAREV A; VORONKOV A;
Indirizzi:
UPPSALA UNIV,DEPT COMP SCI,BOX 311 S-75105 UPPSALA SWEDEN UPPSALA UNIV,DEPT COMP SCI S-75105 UPPSALA SWEDEN
Titolo Testata:
Theoretical computer science
fascicolo: 1-2, volume: 166, anno: 1996,
pagine: 291 - 300
SICI:
0304-3975(1996)166:1-2<291:TUOSRE>2.0.ZU;2-J
Fonte:
ISI
Lingua:
ENG
Soggetto:
EQUATIONAL MATINGS; LOGIC;
Tipo documento:
Article
Natura:
Periodico
Settore Disciplinare:
CompuMath Citation Index
Science Citation Index Expanded
Citazioni:
31
Recensione:
Indirizzi per estratti:
Citazione:
A. Degtyarev e A. Voronkov, "THE UNDECIDABILITY OF SIMULTANEOUS RIGID E-UNIFICATION", Theoretical computer science, 166(1-2), 1996, pp. 291-300

Abstract

Simultaneous rigid E-unification was introduced in 1987 by Gallier, Raatz and Snyder. It is used in the area of automated reasoning with equality in extension procedures, like the tableau method or the connection method. Many articles in this area assumed the existence of an algorithm for the simultaneous rigid E-unification problem. There were several faulty proofs of the decidability of this problem. In this paperwe prove that simultaneous rigid E-unification is undecidable. As a consequence, we obtain the undecidability of the There Exists-fragmentof intuitionistic logic with equality.

ASDD Area Sistemi Dipartimentali e Documentali, Università di Bologna, Catalogo delle riviste ed altri periodici
Documento generato il 02/12/20 alle ore 07:42:30