Web Ontology Representation and Reasoning via Fragments of Set Theory

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 DL⟨4LQS^R⟩(D)–allowing features such as min/max cardinality constructs on the left-hand/right-hand side of inclusion axioms, role chain axioms, and datatypes–which turn out to be quite expressive if compared with SROIQ(D), the description logic underpinning the Web Ontology Language OWL. Then we show that the consistency problem for DL⟨4LQS^R⟩(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 DL⟨4LQSR⟩(D)-knowledge bases is NP-complete. Finally, we provide a 4LQS^R-translation of rules belonging to the Semantic Web Rule Language (SWRL).