The decidability of simultaneous rigid E-unification with one variableShow others and affiliations
1998 (English)In: REWRITING TECHNIQUES AND APPLICATIONS, ISSN 0302-9743, Vol. 1379, p. 181-195Article in journal (Other scientific) Published
Abstract [en]
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
Place, publisher, year, edition, pages
SPRINGER-VERLAG BERLIN , 1998. Vol. 1379, p. 181-195
Keywords [en]
INTUITIONISTIC LOGIC
Identifiers
URN: urn:nbn:se:uu:diva-27353OAI: oai:DiVA.org:uu-27353DiVA, id: diva2:55248
Note
Addresses: Degtyarev A, Univ Uppsala, Dept Comp Sci, POB 311, S-75105 Uppsala, Sweden. Univ Uppsala, Dept Comp Sci, S-75105 Uppsala, Sweden. Univ Michigan, Dept EECS, Ann Arbor, MI 48109 USA. SUNY Albany, Dept Comp Sci, Albany, NY 12222 USA. Max Planck In
2008-10-172008-10-172011-01-14