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

Domenico Cantone, Cristiano Longo & Marianna Nicolosi Asmundo
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...