Correspondence:
[*]
Address for correspondence: Department of Mathematics and Computer Science, University of Catania, Italy
Abstract: In this paper we consider the most common TBox and ABox reasoning services for the description logic ๐โโฉ4LQSR,xโช(D) (๐โD4,ร, for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQSR. ๐โD4,ร is a very expressive description logic. It combines the high scalability and efficiency of rule languages such as the SemanticWeb Rule Language (SWRL) with the expressivity of description logics. In fact, among other features, it supports Boolean operations on concepts and roles, role constructs such as the product of concepts and role chains on the left-hand side of inclusion axioms, role properties such as transitivity, symmetry, reflexivity, and irreflexivity, and data types. We further provide a KE-tableau-based procedure that allows one to reason on the main TBox and ABox reasoning tasks for the description logic ๐โD4,ร. Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the ฮณ-rule. The novel system, called KEฮณ-tableau, turns out to be an improvement of the system introduced in [1] and of standard first-order KE-tableaux [2]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that in several cases the performances of the KEฮณ-tableau-based reasoner are up to about 400% better than the ones of the other two systems.
