In this paper we address the decision problem for a two-sorted fragment of set theory with restricted quantification which extends the language studied in [4] with pair-related quantifiers and constructs. We also show that the decision problem for our language has a nondeterministic exponential-time complexity. However, in the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. In spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are still expressible. We also argue that our restricted language has applications to knowledge representation, with particular reference to metamodeling issues. Finally, we compare our proposed language with two similar languages in terms of their expressivity and present some undecidable extensions of it, involving any of the domain, range, image, and map composition operators.

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

CANTONE, Domenico;
2014-01-01

Abstract

In this paper we address the decision problem for a two-sorted fragment of set theory with restricted quantification which extends the language studied in [4] with pair-related quantifiers and constructs. We also show that the decision problem for our language has a nondeterministic exponential-time complexity. However, in the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. In spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are still expressible. We also argue that our restricted language has applications to knowledge representation, with particular reference to metamodeling issues. Finally, we compare our proposed language with two similar languages in terms of their expressivity and present some undecidable extensions of it, involving any of the domain, range, image, and map composition operators.
2014
Decision procedures; Set theory; Undecidability; Ordered pairs
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11769/16601
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact