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