In this paper we use results from Computable Set Theory as a means to represent and reason about description logics and rule languages for the semantic web. Specifically, we introduce the description logic $mathcal{DL}langle 4LQS^Rrangle(D)$--admit
ting features such as min/max cardinality constructs on the left-hand/right-hand side of inclusion axioms, role chain axioms, and datatypes--which turns out to be quite expressive if compared with $mathcal{SROIQ}(D)$, the description logic underpinning the Web Ontology Language OWL. Then we show that the consistency problem for $mathcal{DL}langle 4LQS^Rrangle(D)$-knowledge bases is decidable by reducing it, through a suitable translation process, to the satisfiability problem of the stratified fragment $4LQS^R$ of set theory, involving variables of four sorts and a restricted form of quantification. We prove also that, under suitable not very restrictive constraints, the consistency problem for $mathcal{DL}langle 4LQS^Rrangle(D)$-knowledge bases is textbf{NP}-complete. Finally, we provide a $4LQS^R$-translation of rules belonging to the Semantic Web Rule Language (SWRL).
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 knowled
ge 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
