A decidable quantified fragment of set theory with ordered pairs and some undecidable extensions

Domenico Cantone
(University of Catania)
Cristiano Longo
(NCE)

In this paper we address the decision problem for a fragment of set theory with restricted quantification which extends the language studied in [4] with pair related quantifiers and constructs, in view of possible applications in the field of knowledge representation. We will also show that the decision problem for our language has a non-deterministic exponential time complexity. However, for the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. We also observe that in spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are expressible. Finally, we present some undecidable extensions of our language, involving any of the operators domain, range, image, and map composition.

[4] Michael Breban, Alfredo Ferro, Eugenio G. Omodeo and Jacob T. Schwartz (1981): Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Communications on Pure and Applied Mathematics 34, pp. 177-195

In Marco Faella and Aniello Murano: Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2012), Napoli, Italy, September 6-8, 2012, Electronic Proceedings in Theoretical Computer Science 96, pp. 224–237.
Published: 7th October 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.96.17 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org