An Improved Set-based Reasoner for the Description Logic 𝒟ℒD4,×^†

Issue title: 33rd Italian Conference on Computational Logic: CILC 2018

Guest editors: Paolo Felli, Marco Montali and Maurizio Proietti

Article type: Research Article

Authors: Cantone, Domenico | Nicolosi-Asmundo, Marianna^{; *} | Santamaria, Daniele Francesco

Affiliations: Department of Mathematics and Computer Science, University of Catania, Italy. domenico.cantone@unict.it, nicolosi@dmi.unict.it, santamaria@dmi.unict.it

Correspondence: [*] Address for correspondence: Dept. of Mathematics and Computer Science, Viale Andrea Doria 6, I -95125 Catania, Italy.

Note: [†] This is an extended and improved version of a paper published in the proceedings of the 3rd International Workshop about Sets and Tools (SETS 2018); see [1].

Abstract: We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic 𝒟ℒ〈4LQSR,×〉(D) (𝒟ℒD4,×, for short). Our application solves the main TBox and ABox reasoning problems for 𝒟ℒD4,×. In particular, it solves the consistency and the classification problems for 𝒟ℒD4,×-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 𝒟ℒD4,×-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

DOI: 10.3233/FI-2021-2009

Journal: Fundamenta Informaticae, vol. 178, no. 4, pp. 315-346, 2021