An Improved Set-based Reasoner for the Description Logic 𝒟 ℒ D 4,× †

Abstract

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic 𝒟ℒ〈4LQS^R,×〉(D) ( $𝒟 ℒ_{D}^{4, \times}$ , for short). Our application solves the main TBox and ABox reasoning problems for $𝒟 ℒ_{D}^{4, \times}$ . In particular, it solves the consistency and the classification problems for $𝒟 ℒ_{D}^{4, \times}$ -knowledge bases represented in set-theoretic terms, and a generalization of the Conjunctive Query Answering problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and improves a previous version, is implemented in C++. It supports $𝒟 ℒ_{D}^{4, \times}$ -knowledge bases serialized in the OWL/XML format and it admits also rules expressed in SWRL (Semantic Web Rule Language).

Keywords

Reasoners for description logics Consistency and classification problems Conjunctive query answering problem KE-tableau systems Semantic Web Automated reasoning Computable set theory