Catalogo Articoli (Spogli Riviste)

OPAC HELP

Titolo:
Decidability and complexity of simultaneous rigid E-unification with one variable and related results
Autore:
Degtyarev, A; Gurevich, Y; Narendran, P; Veanes, M; Voronkov, A;
Indirizzi:
Max Planck Inst Informat, D-66123 Saarbrucken, Germany Max Planck Inst Informat Saarbrucken Germany D-66123 aarbrucken, Germany Univ Uppsala, Dept Comp Sci, S-75105 Uppsala, Sweden Univ Uppsala Uppsala Sweden S-75105 pt Comp Sci, S-75105 Uppsala, Sweden Univ Michigan, Dept EECS, Ann Arbor, MI 48109 USA Univ Michigan Ann ArborMI USA 48109 , Dept EECS, Ann Arbor, MI 48109 USA SUNY Albany, Dept Comp Sci, Albany, NY 12222 USA SUNY Albany Albany NY USA 12222 bany, Dept Comp Sci, Albany, NY 12222 USA
Titolo Testata:
THEORETICAL COMPUTER SCIENCE
fascicolo: 1-2, volume: 243, anno: 2000,
pagine: 167 - 184
SICI:
0304-3975(20000728)243:1-2<167:DACOSR>2.0.ZU;2-Z
Fonte:
ISI
Lingua:
ENG
Soggetto:
INTUITIONISTIC LOGIC; MATINGS; SYSTEMS;
Keywords:
rigid E-unification; finite tree automata; logic with equality;
Tipo documento:
Article
Natura:
Periodico
Settore Disciplinare:
Engineering, Computing & Technology
Citazioni:
56
Recensione:
Indirizzi per estratti:
Indirizzo: Veanes, M Max Planck Inst Informat, Stadtwald, D-66123 Saarbrucken, Germany Max Planck Inst Informat Stadtwald Saarbrucken Germany D-66123
Citazione:
A. Degtyarev et al., "Decidability and complexity of simultaneous rigid E-unification with one variable and related results", THEOR COMP, 243(1-2), 2000, pp. 167-184

Abstract

We show that simultaneous rigid E-unification, or SREU for short, is decidable and in fact EXPTIME-complete in the case of one variable. This result implies that the For All*There Exists For All* fragment of intuitionistic logic with equality is decidable: Together with a previous result regarding the undecidability of the There Exists There Exists-fragment, we obtain a complete classification of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantifier prefix. It is also proved that SREU with one variable and a constant bound on the number of rigidequations is P-complete. Moreover, we consider a case of SREU where one allows several variables, but each rigid equation either contains one variable, or has a ground left-hand side and an equality between two variables as a right-hand side. We show that SREU is decidable also in this restricted case. (C) 2000 Elsevier Science B.V. All rights reserved.

ASDD Area Sistemi Dipartimentali e Documentali, Università di Bologna, Catalogo delle riviste ed altri periodici
Documento generato il 28/11/20 alle ore 04:35:27