In this paper we address the decision problem for a fragment of set theory with restricted quantification which extends the language studied in  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.
|Titolo:||A decidable quantified fragment of set theory with ordered pairs and some undecidable extensions|
|Data di pubblicazione:||2012|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|