An Optimized KE-Tableau-Based System for Reasoning in the Description Logic ${\mathcal {DL}}_{{\mathbf {D}}}^{4,\!\times }$

Abstract

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal {DL}\langle \mathsf {4LQS^{R,\!\times }}\rangle (\mathbf {D})$, in short $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$. The logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$, representable in the decidable multi-sorted quantified set-theoretic fragment $\mathsf {4LQS^R}$, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics.

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 $\gamma$-rule. The novel system, called KE$^{\mathbf {\gamma }}$-tableau, turns out to improve both the system introduced in [3] and the standard first-order KE-tableaux [10]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the KE$^{\mathbf {\gamma }}$-tableau-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set theory.

1 Introduction

Recently, decidability results in Computable Set Theory have been used for knowledge representation and reasoning, in particular, in the context of description logics (DLs) and rule languages for the Semantic Web. These efforts are motivated by the fact that there exists a natural translation function between set-theoretic fragments and languages for the Semantic Web.

In particular, the decidable four-level stratified set-theoretic fragment $\mathsf {4LQS^R}$, involving variables of four sorts, pair terms, and a restricted form of quantification over variables of the first three sorts (cf. [1]), has been used in [2] to represent the description logic $\mathcal {DL}\langle \mathsf {4LQS^{R,\!\times }}\rangle (\mathbf {D})$, in short $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$.

The description logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ supports various constructs on concepts and roles, and it also admits data types, relevant in real word applications. In addition, it permits to express the Semantic Web Rule Language (SWRL), an extension of the Ontology Web Language (OWL). Decidability of the Conjunctive Query Answering (CQA) problem for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ has been proved in [2] via a reduction to the CQA problem for $\mathsf {4LQS^R}$, whose decidability easily follows from that of $\mathsf {4LQS^R}$ (see [1]). In [2], the authors provided a terminating KE-tableau based procedure that, given a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-query Q and a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-knowledge base $\mathcal {KB}$ represented in set-theoretic terms, determines the answer set of Q with respect to $\mathcal {KB}$. Such an algorithm serves also as a decision procedure for the consistency problem for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-knowledge bases (KBs). We recall that KE-tableaux systems [10] construct tableaux whose distinct branches define mutually exclusive situations, thus preventing the proliferation of redundant branches, typical of semantic tableaux.

The results presented in [2] have been extended in [3] to the main ABox reasoning tasks for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$, such as instance checking and concept retrieval, by defining the Higher-Order Conjunctive Query Answering (HOCQA) problem for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$. Such problem, instantiable to the principal reasoning tasks for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-ABoxes, has been defined by introducing Higher Order (HO) $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-conjunctive queries, admitting variables of three sorts: individual and data type variables, concept variables, and role variables. Decidability of the HOCQA problem for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ has been proved via a reduction to the HOCQA problem for the set-theoretic fragment $\mathsf {4LQS^R}$.

In [4], an implementation of the KE-tableau procedure defined in [3] has been presented. Such prototype, written in C++, supports $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KBs serialized in OWL/XML. It has been implemented only for TBox-reasoning services, namely, for verifying the consistency of given ontologies. Purely universal quantifiers are eliminated by the reasoner during a preprocessing phase, in which each quantified formula is instantiated in a systematic way with the individuals of the KB. The resulting instances are then suitably handled by applying to them the KE-elimination and bivalence rules. In the light of the benchmarking of the prototype, it turned out that the preprocessing phase of the universally quantified formulae is more and more expensive as the size of the KB grows.

In this paper, the KE-tableau-based procedure defined in [3] is modified, by eliminating the preprocessing phase for universally quantified formulae and replacing the standard KE-elimination rule with a novel elimination rule, called $\text {E}^{\gamma }\text {-rule}$, that incorporates the standard rule for treating universally quantified formulae ($\gamma$-rule). The resulting system¹ turns out to be more efficient than the KE-system in [4] and the First-Order (FO) KE-system in [10], as shown by suitable benchmarking tests executed on C++ implementations of the three systems. The main reason for such a speed-up relies on the fact that the $\text {E}^{\gamma }\text {-rule}$ does not need to store the instances of the quantified formulae on the KE-tableau.

2 Preliminaries

2.1 The Set-Theoretic Fragment

It is convenient to recall the main set-theoretic notions behind the description logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ and its reasoning problems. For space reasons, we do not report the syntax and semantics of the whole $\mathsf {4LQS^R}$: the interested reader can find it in [1], together with the decision procedure for its satisfiability problem. Thus, we just focus on the class of $\mathsf {4LQS^R}$-formulae actually involved in the set-theoretic representation of $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$, namely, the propositional combinations of $\mathsf {4LQS^R}$-quantifier-free literals (atomic formulae and their negations) and of $\mathsf {4LQS^R}$ purely universal formulae of the types displayed in Table 1. For the sake of conciseness, we refer to such class of $\mathsf {4LQS^R}$-formulae as .

We recall that the fragment $\mathsf {4LQS^R}$ admits four collections, $\mathtt {Var}_i$, of variables of sort $i=0,1,2,3$, which are denoted by $X^i,Y^i,Z^i, \ldots$ (in particular, variables of sort 0 are also denoted by $x,y,z, \ldots$). In addition to variables, also pair terms of the form $\langle x,y \rangle$, with $x,y \in \mathtt {Var}_0$, are allowed. Since the types of formulae illustrated in Table 1 do not involve variables of sort 2, notions and definitions concerning -formulae will refer to variables of sorts 0, 1, and 3 only.

Table 1. Types of literals and quantified formulae admitted in .

The variables $z_1,\ldots ,z_n$ are said to occur quantified in $(\forall z_1) \ldots (\forall z_n) \varphi _0$. A variable occurs free in a -formula $\varphi$ if it does not occur quantified in any subformula of $\varphi$. For $i = 0,1,3$, we denote with $\mathtt {Var}_i(\varphi )$ the collections of variables of sort i occurring free in $\varphi$.

For space reasons, the notions of -substitution and of -interpretation are not included here, but they can be found in [5].

2.2 The Logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$

In what follows, we present the syntax and semantics of the description logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$.

Let $\mathbf {R_A}$, $\mathbf {R_D}$, $\mathbf {C}$, $\mathbf {I}$ be denumerable pairwise disjoint sets of abstract role names, concrete role names, concept names, and individual names, respectively.

The definition of data types relies on the notion of data type map, given according to [11] as follows. A data type map is a quadruple $\mathbf {D}= (N_{D}, N_{C},N_{F},\cdot ^{\mathbf {D}})$, where $N_{D}$ is a finite set of data types, $N_{C}$ is a function assigning a set of constants $N_{C}(d)$ to each data type $d \in N_{D}$, $N_{F}$ is a function assigning a set of facets $N_{F}(d)$ to each $d \in N_{D}$, and $\cdot ^{\mathbf {D}}$ is a function assigning a data type interpretation $d^{\mathbf {D}}$ to each $d \in N_{D}$, a facet interpretation $f^{\mathbf {D}} \subseteq d^{\mathbf {D}}$ to each facet $f \in N_{F}(d)$, and a data value $e_{d}^{\mathbf {D}} \in d^{\mathbf {D}}$ to every constant $e_{d} \in N_{C}(d)$. We shall assume that the interpretations of the data types in $N_{D}$ are nonempty pairwise disjoint sets.

(a) $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-data type, (b) $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-concept, (c) $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-abstract role, and (d) $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-concrete role terms are constructed according to the following syntax rules:

• (a) $t_1, t_2 \longrightarrow dr ~|~\lnot t_1 ~|~t_1 \sqcap t_2 ~|~t_1 \sqcup t_2 ~|~\{e_{d}\}\, ,$

• (b) $C_1, C_ 2 \longrightarrow A ~|~\top ~|~\bot ~|~\lnot C_1 ~|~C_1 \sqcup C_2 ~|~C_1 \sqcap C_2 ~|~\{a\} ~|~\exists R{.} Self | \exists R{.}\{a\}| \exists P{.}\{e_{d}\}\, ,$

• (c) $R_1, R_2 \longrightarrow S ~|~U ~|~R_1^{-1} ~|~ \lnot R_1 ~|~R_1 \sqcup R_2 ~|~R_1 \sqcap R_2 ~|~R_{C_1 |} ~|~R_{|C_1} ~|~R_{C_1 ~|~C_2} ~|$ $~id(C) ~|~ C_1 \times C_2 \, ,$

• (d) $P_1,P_2 \longrightarrow T ~|~\lnot P_1 ~|~ P_1 \sqcup P_2 ~|~ P_1 \sqcap P_2 ~|~P_{C_1 |} ~|~P_{|t_1} ~|~P_{C_1 | t_1},$

where dr is a data range for $\mathbf {D}$, $t_1,t_2$ are data type terms, $e_{d}$ is a constant in $N_{C}(d)$, a is an individual name, A is a concept name, $C_1, C_2$ are $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-concept terms, S is an abstract role name, U is an abstract role name denoting the universal role, $R, R_1,R_2$ are $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-abstract role terms, T is a concrete role name, and $P,P_1,P_2$ are $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-concrete role terms. We remark that data type terms are introduced in order to represent derived data types.

A $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB is a triple ${\mathcal K} = (\mathcal {R}, \mathcal {T}, \mathcal {A})$ such that $\mathcal {R}$ is a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-RBox, $\mathcal {T}$ is a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-TBox, and $\mathcal {A}$ is a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-ABox. For space constraints, the definitions of $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-RBox, $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-TBox, $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-ABox and the semantics of $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ are omitted here, but the interested reader can find them in [5].

Expressiveness of the Description Logic $\varvec{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$. Despite the fact that the description logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ is limited as far as the introduction of new individuals is concerned, it is more liberal than $\mathcal {SROIQ}(\mathbf {D})$ [7] in the construction of role inclusion axioms, since the roles involved are not restricted by any ordering relationship, the notion of simple role is not needed, and Boolean operations on roles and role constructs such as the product of concepts are admitted. Moreover, $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ supports more OWL constructs than the DLs underpinning the profiles OWL QL, OWL RL, and OWL EL [8], such as disjoint union of concepts and union of data ranges. Furthermore, basic and derived data types can be used inside inclusion axioms involving concrete roles. In addition, concerning the expressiveness of rules, the set-theoretic fragment underpinning $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ allows one to express the disjunctive Datalog fragment admitting negation, equality and constraints, subject to no safety condition, and supporting for data types.

Reasoning with the Description Logic $\varvec{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$. Next, we introduce the reasoning services available for the description logic $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$, i.e., the type of inferences that can be drawn from what is explicitly asserted in a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB. Specifically, we focus on two families of reasoning tasks, concerning respectively TBoxes and ABoxes. Among the main TBox reasoning problems, such as satisfiability of a concept, subsumption of concepts, equivalence of concepts, and disjunction of concepts, the problem of deciding the consistency of a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB is the most representative one, as it includes the majority of them.² In [2], we proved the decidability of the consistency problem of a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB and of a relevant ABox reasoning task, namely the Conjunctive Query Answering (CQA) problem for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$ consisting in computing the answer set of a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-conjunctive query with respect to a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB. In [3], we generalized the problem introducing the Higher Order Conjuctive Query Answering (HOCQA) problem for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$. Such problem is characterized by Higher Order (HO) $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-conjunctive queries admitting variables of three sorts: individual and data type variables, concept variables, and role variables (the interested reader can find in [3] the definitions of HO-conjunctive queries, HO-substitutions, and HOCQA problem).

As illustrated in [3], the HOCQA problem can be instantiated to significant ABox reasoning problems such as (A) role filler retrieval, the problem of retrieving all the fillers x such that the pair (a, x) is an instance of a role R; (B) concept retrieval, the problem of retrieving all concepts which an individual is an instance of; (C) role instance retrieval, the problem of retrieving all roles which a pair of individuals (a, b) is an instance of; and (D) conjunctive query answering, the problem of finding the answer set of a conjunctive query.

In [3], we solved the HOCQA problem just stated by reducing it to the analogous problem formulated in the context of the fragment (and in turn of the decision procedure for $\mathsf {4LQS^R}$ presented in [1]).

The HOCQA problem in the context can be stated as follows. Let $\phi$ be a -formula and $\psi$ a conjunction of -literals. The HOCQA problem for $\psi$ w.r.t. $\phi$ consists in computing the HO answer set of $\psi$ w.r.t. $\phi$, namely, the collection $\varSigma '$ of all the substitutions $\sigma '$ such that , for some -interpretation .

In view of the decidability of the satisfiability problem for $\mathsf {4LQS^R}$-formulae, the HOCQA problem for -formulae is decidable as well. The reduction is carried out by means of a function $\theta$ that maps the $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB $\mathcal {KB}$ in a -formula $\phi _{\mathcal {KB}}$ in Conjunctive Normal Form (CNF) and the HO $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-conjunctive query Q in the -formula $\psi _{Q}$ (see [2] for details). Specifically,

Let $\varSigma$ be the HO-answer set of Q w.r.t. $\mathcal {KB}$ (see [3] for the definition of HO-answer set) and $\varSigma '$ the HO-answer set of $\psi _Q$ w.r.t. $\phi _{\mathcal {KB}}$. Then $\varSigma$ consists of all substitutions $\sigma$ (involving exactly the variables occurring in Q) such that $\theta (\sigma ) \in \varSigma '$. By Lemma 1 in [3], $\varSigma '$ can be effectively computed and thus $\varSigma$ can be effectively computed as well.

3 A KE-Tableau Based Algorithm for Reasoning in $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$

In what follows, we briefly discuss the procedures $\textit{Consistency-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ and $\textit{HOCQA}^\gamma \textit{-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$. The procedure $\textit{Consistency-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ checks the consistency of its input -formula $\phi _{\mathcal {KB}}$, representing a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KB. When $\phi _{\mathcal {KB}}$ is consistent, it builds a KE-tableau $\mathcal {T}_{\mathcal {KB}}$ whose distinct open and complete branches induce the models of $\phi _{\mathcal {KB}}$. Then the procedure $\textit{HOCQA}^\gamma \textit{-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ computes the HO-answer set of a given -formula $\psi _Q$ (representing a $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-HO conjunctive query Q) w.r.t. $\phi _{\mathcal {KB}}$, by means of a forest of decision trees based on the branches of the KE-tableau $\mathcal {T}_\mathcal {KB}$ computed by the procedure $\textit{Consistency-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ with input $\phi _\mathcal {KB}$.

We now shortly introduce a variant of KE-tableau called KE$^{\mathbf {\gamma }}$-tableau.³ Let , where each $C_i$ is either a -literal of the types illustrated in Table 1 or a -purely universal quantified formula of the form $(\forall {x_1})\ldots (\forall {x_m})(\beta _1 \vee \ldots \vee \beta _n)$, with $\beta _1,\ldots , \beta _n$ -literals. $\mathcal {T}$ is a for $\varPhi$ if there exists a finite sequence $\mathcal {T}_1, \ldots , \mathcal {T}_t$ such that (i) $\mathcal {T}_1$ is the one-branch tree consisting of the sequence $C_1,\ldots , C_p$, (ii) $\mathcal {T}_{i+1}$ is obtained from $\mathcal {T}_i$, for each $i<t$, either by an application of one of the rules ($\text {E}^{\gamma }\text {-rule}$ or PB-rule) in Fig. 1 or by applying a substitution $\sigma$ to a branch $\vartheta$ of $\mathcal {T}_i$ (in particular, the substitution $\sigma$ is applied to each formula X of $\vartheta$; the resulting branch will be denoted with $\vartheta \sigma$), and (iii) $\mathcal {T}_t = \mathcal {T}$. In the definition of the $\text {E}^{\gamma }\text {-rule}$ reported in Fig. 1 we have: (a) $\tau :=\{x_1/x_{o_1} \ldots x_m/x_{o_m}\}$ is a substitution such that $x_1,\ldots ,x_m$ are the quantified variables in $\psi$ and $x_{o_1}, \ldots , x_{o_m} \in \mathtt {Var}_0(\varPhi )$; (b) is a set containing the complements of all the disjuncts $\beta _1, \ldots , \beta _n$ to which the substitution $\tau$ is applied, with the exception of the disjunct $\beta _i$.

Fig. 1.

Expansion rules for the KE$^{\mathbf {\gamma }}$-tableau.

Let $\mathcal {T}$ be a KE$^{\mathbf {\gamma }}$-tableau. A formula $\psi =(\forall {x_1})\ldots (\forall {x_m})(\beta _1 \vee \ldots \vee \beta _n)$ is fulfilled in a branch $\vartheta$, if $\vartheta$ contains $\beta _i\tau$ for some $i=1,\ldots ,n$ and for all $\tau$ having as domain the set $Q\mathtt {Var}_0(\psi )=\{x_1, \ldots , x_m\}$ of the quantified variables occurring in $\psi$ and as range the set $\mathtt {Var}_0(\vartheta )$ of the variables of sort 0 occurring free in $\vartheta$. Notice that since the procedure $\textit{Consistency-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ does not introduce any new variable, $\mathtt {Var}_0(\vartheta )$ coincides with $\mathtt {Var}_0(\phi _{\mathcal {KB}})$, for every branch $\vartheta$. A branch $\vartheta$ is fulfilled if every formula $\psi =(\forall {x_1})\ldots (\forall {x_m})(\beta _1 \vee \ldots \vee \beta _n)$ occurring in $\vartheta$ is fulfilled. A KE$^{\mathbf {\gamma }}$-tableau is fulfilled when all its branches are fulfilled. A branch $\vartheta$ of $\mathcal {T}$ is closed if either it contains both A and $\lnot A$, for some formula A, or a literal of type $\lnot (x = x)$; otherwise, it is open. A KE$^{\mathbf {\gamma }}$-tableau is closed when all its branches are closed. A branch $\vartheta$ is complete if either it is closed or it is open, fulfilled, and it does not contain any literal of type $x=y$, with x and y distinct variables. A KE$^{\mathbf {\gamma }}$-tableau is complete (resp., fulfilled) if all its branches are complete (resp., fulfilled or closed). The notions of branch and KE$^{\mathbf {\gamma }}$-tableau satisfiability are the standard ones.

The procedure $\textit{Consistency-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ takes care of the literals of type $x=y$ occurring in the branches of $\mathcal {T}_\mathcal {KB}$ by constructing, for each open and fulfilled branch $\vartheta$ of $\mathcal {T}_\mathcal {KB}$, a substitution $\sigma _{\vartheta }$ such that $\vartheta \sigma _{\vartheta }$ does not contain literals of type $x=y$ with distinct x, y. Then, for every open and complete branch $\vartheta ':=\vartheta \sigma _{\vartheta }$ of $\mathcal {T}_{\mathcal {KB}}$, the procedure $\textit{HOCQA}^\gamma \textit{-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}$ constructs a decision tree $\mathcal {D}_{\vartheta '}$ whose maximal branches induce substitutions $\sigma '$ such that $\sigma _{\vartheta }\sigma '$ belongs to the HO-answer set of $\psi _{Q}$ with respect to $\phi _{\mathcal {KB}}$ (the definition of $\mathcal {D}_{\vartheta '}$ can be found in [5]).⁴

We recall that the HOCQA problem can be solved in exponential-time when the $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KBs do not contain qualified cardinality restrictions and role chain axioms, otherwise it can be solved in double-exponential time (see [5] for details).

Remarks on Different Versions of the Algorithm. The C++ implementation of the algorithm presented in this paper, called KE$^{\mathbf {\gamma }}$-system, is more efficient than the prototype KE-system proposed in [4]. The main motivation behind this performance improvement relies on the introduction of the $\text {E}^{\gamma }\text {-rule}$ (see Fig. 1) that acts on the -purely universal quantified formulae in the KB by systematically instantiating them and applying the standard E-rule (elimination rule) on-the-fly. The $\text {E}^{\gamma }\text {-rule}$ replaces the preliminary phase of systematic expansion of the -purely universal quantified formulae in the KB and the subsequent application of the E-rule implemented by the KE-system presented in [3]. In addition, the KE$^{\mathbf {\gamma }}$-system turns out be also more efficient than the implementation FO KE-system of the FO KE-tableau in [10], that applies the standard $\gamma$- and E-rules. Incidentally, it turns out that the KE-system and the FO KE-system have similar performances. As shown in [5, Fig. 3], the KE$^{\mathbf {\gamma }}$-system has a better performance, up to about $400\%$, than the other two, even if in some cases (lowest part of the plot) the performances of the three systems are comparable. Thus the KE$^{\mathbf {\gamma }}$-system is always convenient, also because the collection of the expansions of $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-purely universal quantified formulae of level 1 (exponential in the size of the KB) is not stored in memory.

The benchmarking process is based on a huge amount of KBs of different sizes and kinds, constructed ad hoc just for the purpose of comparing the three mentioned systems, and on some real-world ontologies developed by the authors.

4 Conclusions and Future Work

We presented an improvement, called KE$^{\mathbf {\gamma }}$-tableau, of the KE-tableau in [3] for the most widespread reasoning tasks for $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-TBoxes and $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$–ABoxes. These reasoning problems are addressed by translating $\mathcal {DL}_{\mathbf {D}}^{4,\!\times }$-KBs and queries in terms of formulae of the set-theoretic language . The procedure introduced in this paper generalizes the KE-elimination rule in such way as to incorporate the $\gamma$-rule, namely, the expansion rule for handling universally quantified formulae. The KE$^{\mathbf {\gamma }}$-tableau procedure has remarkable aftermath, since its implementation is markedly more efficient in terms of space and execution time than the KE-system [4] and the implementation FO KE-system of the FO KE-tableau [10], as observed in our experimental tests.

In order to be able to reason with description logics admitting full existential and universal quantification, we plan to extend the set-theoretic fragment underpinning our reasoner with a restricted version of the operator of relational composition. Results and notions presented in [9] will be of inspiration for such a task. We also intend to improve our reasoner so as to deal with the reasoning problem of ontology classification. We shall compare the resulting reasoner with existing well-known reasoners such as Hermit [6] and Pellet [12], providing also some benchmarking. In addition, we plan to allow data type reasoning by either integrating existing solvers for the Satisfiability Modulo Theories (SMT) problem or by designing ad hoc new solvers. Finally, as each branch of a KE$^{\mathbf {\gamma }}$-tableau can be independently computed by a single processing unit, we intend to implement a parallel version of the software by using the Nvidia CUDA framework.