DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2011.129

A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics

Authors: Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract

We present a decision procedure for a quantified fragment of set theory involving ordered pairs and some operators to manipulate them. When our decision procedure is applied to formulae in this fragment whose quantifier prefixes have length bounded by a fixed constant, it runs in nondeterministic polynomial-time. Related to this fragment, we also introduce a description logic which provides an unusually large set of constructs, such as, for instance, Boolean constructs among roles. The set-theoretic nature of the description logics semantics yields a straightforward reduction of the knowledge base consistency problem to the satisfiability problem for formulae of our fragment with quantifier prefixes of length at most 2, from which the NP-completeness of reasoning in this novel description logic follows. Finally, we extend this reduction to cope also with SWRL rules.

Cite as

Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo. A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 129-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{cantone_et_al:LIPIcs.CSL.2011.129,
  author =	{Cantone, Domenico and Longo, Cristiano and Nicolosi Asmundo, Marianna},
  title =	{{A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{129--143},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.129},
  URN =		{urn:nbn:de:0030-drops-32278},
  doi =		{10.4230/LIPIcs.CSL.2011.129},
  annote =	{Keywords: NP-complete decision procedures, set theory, description logic}
}

Search Results

Documents authored by Longo, Cristiano

A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics

Abstract

Cite as

Thanks for your feedback!

Could not send message