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)$--admitting 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).
Download