We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (strati ed) set theory expressing the description logic DLh4LQSR; i(D) (DL4D; , for short). Our application solves the main TBox and ABox reasoning problems for DL4D; . In particular, it solves the consistency problem for DL4D; -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 optimizes abapseresv(ioseues [p7r])o,toistyipmepfloermtehnetecdo ninsisCte+n+cy. Icthescukpinpgorotsf DDLL44DD;; --kknnoowwlleeddggee bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).
A wealth of decidability results has been collected over the years within the research eld of Computable Set Theory [2, 11, 17]. However, only recently some of these results have been applied in the context of knowledge representation and reasoning for the semantic web. Such e orts have been motivated by the characteristics of the set-theoretic fragments considered, as they provide very expressive unique formalisms that combine the modelling capabilities of a rule language with the constructs of description logics. The decidable multi-sorted quanti ed set-theoretic fragment 4LQSR [3] is appropriate in this sense, in consideration of the fact that its decision procedure is e ciently implementable. We recall that the language of 4LQSR involves variables of four sorts, pair terms, and a restricted form of quanti cation.
In [5], the theory 4LQSR has been used to represent the expressive description 4; by means of a suitable translation mapping. Moreover, decidability of logic DLD the most widespread reasoning problems for DL4D; , such as the consistency problem and the Conjunctive Query Answering (CQA) problem for DL4D; -knowledge bases (KBs) were proved via a reduction to the satis ability problem for 4LQSR. Since 4LQSR admits variables of four sorts, the CQA problem was generalized in such a way as to admit queries over three sorts of variables. Such a generalization, called Higher-Order Conjunctive Query Answering (HOCQA) problem can be instantiated to the most widespread reasoning tasks for DL4D; -ABox.
The description logic DLD
stract roles, concept domain and range, and existential and minimum cardinality
restriction on the left-hand side of inclusion axioms. It also supports role chains
on the left-hand side of inclusion axioms and properties on roles such as
transitivity, symmetry, and re exivity. In [4], its consistency problem has been shown
to be NP-complete under not very restrictive constraints. Such a low complexity
result depends on the fact that existential quanti cation cannot appear on the
right-hand side of inclusion axioms. Nonetheless, DL4D; turns out to be more
expressive than other low complexity logics such as OWL RL [16] and
therefore it is very suitable for representing real-world ontologies. For instance, the
restricted version of DL4D; mentioned above allows one to express several OWL
ontologies, such as ArcheOntology [16] and OntoCeramic [10], for the classi cation
of archaeological nds, and ArchivioMuseoFabbrica [
4; are not subject to any ordering relationship, ioms, as the roles involved in DLD and the notion of simple role is not needed. For example, the role hierarchy presented in [13, page 2] is not expressible in SROIQ(D), but can be represented in DL4D; . In addition, DLD
4; is a powerful rule language able to express rules with negated atoms such as
Person(?p) ^ :hasHome(?p; ?h) =) HomelessPerson(?p) that are not supported by the SWRL language.
In [7], we presented a rst e ort to implement in C++ a KE-tableau-based decision procedure for the consistency problem of DL4D; -KBs, by resorting to the algorithm introduced in [5]. The choice of KE-tableau systems [14], instead of traditional semantic tableaux [19], was motivated by the fact that KE-tableau systems introduce an analytic cut rule which permits to construct trees whose branches de ne mutually exclusive situations, thus avoiding the proliferation of redundant branches, typical of Smullyan's semantic tableaux [19]. Thus, given as input a consistent KB, the procedure yields a KE-tableau whose open branches induce distinct models of the KB. Otherwise, a closed KE-tableau is returned.
In this contribution we improve the reasoner presented in [7] by introducing a system called KE -tableau which admits a generalization of the KE-elimination rule incorporating the -rule, namely the expansion rule for handling universally quanti ed formulae. The reasoner also includes a procedure to compute the HOCQA problem for DL4D; . Finally, through suitable benchmark tests, we show that such a novel reasoner is more e cient than the one introduced in [7].
The set-theoretic fragment 4; We summarize the set-theoretic notions underpinning the description logic DLD and its reasoning tasks. For the sake of conciseness, we avoid to report here the syntax and semantics of the whole 4LQSR theory (the interested reader can nd it in [3] together with the decision procedure for its satis ability problem). Thus, we focus on the 4LQSR-formulae de facto involved in the set-theoretic representation of DL4D; , namely propositional combinations of 4LQSR-literals (atomic formulae or their negations) and 4LQSR purely universal formulae of the types displayed in Table 1. The class of such 4LQSR-formulae is called 4LQSRDL4D; .
We recall that the fragment 4LQSR admits four collections, Vari, of variables of sort i denoted by Xi; Y i; Zi; : : :, for i = 0; 1; 2; 3 (variables of sort 0 are also denoted by x; y; z; : : :). Besides variables, also pair terms of the form hx; yi, with x; y 2 Var0, are allowed. Since the types of formulae displayed in Table 1 do not contain variables of sort 2, here we limit ourselves only to notions and de nitions relative to 4LQSRDL4D; -formulae involving variables of sorts 0; 1; and 3.
Literals of level 0 x = y; x 2 X1; hx; yi 2 X3 :(x = y); :(x 2 X1); :(hx; yi 2 X3)
Purely universal quanti ed formulae of level 1 (8z1) : : : (8zn)'0, where z1; : : : ; zn 2 Var0 and '0 is any propositional combination of
literals of level 0. is the mapping ' 7! ' such that, for any given universal quanti ed 4LQSRDL4D; formula ', ' is the result of replacing in ' the free occurrences of the variables xi in x (for i = 1; : : : ; n) with the corresponding yi in y, of Xj1 in X1 (for j = 1; : : : ; m) with Yj1 in Y 1, and of Xh3 in X3 (for h = 1; : : : ; q) with Yh3 in Y 3, respectively. A substitution is free for ' if the formulae ' and ' have exactly the same occurrences of quanti ed variables. The empty substitution, denoted , satis es ' = ', for each 4LQSRDL4D; -formula '.
A 4LQSRDL4D; -interpretation is a pair M = (D; M ), where D is a nonempty collection of objects (called domain or universe of M) and M is an assignment over the variables in Vari, for i = 0; 1; 3, such that:
M X0 2 D; M X1 2 P(D); M X3 2 P(P(P(D))); where Xi 2 Vari, for i = 0; 1; 3, and P(s) denotes the powerset of s. Pair terms are interpreted a la Kuratowski, and therefore we put
- M = (D; M ) be a 4LQSRDL4D; -interpretation, - x1; : : : ; xn 2 Var0, and - u1; : : : ; un 2 D.
M hx; yi := ffM xg; fM x; M ygg.
By M[x=u], we denote the interpretation M0 = (D; M 0) such that M 0xi = ui (for i = 1; : : : ; n), and which otherwise coincides with M on all remaining variables. For a 4LQSRDL4D; -interpretation M = (D; M ) and a formula ', the satis ability relationship M j= ' is recursively de ned over the structure of ' as follows. Literals are evaluated in a standard way, based on the usual interpretation of the predicates `2' and `=', and of the propositional negation `:'. Compound formulae are interpreted according to the standard rules of propositional logic. Finally, purely universal formulae are evaluated as follows: - M j= (8z1) : : : (8zn)'0 i
M[z=u] j= '0, for all u 2 Dn.
If M j= ', then
M is said to be a 4LQSRDL4D; -model for '. A 4LQSRDL4D; is valid if it is satis ed by all 4LQSRDL4D; -interpretations. formula is said to be satis able if it has a 4LQSRDL4D; -model. A 4LQSRDL4D; -formula 2.2
The logic DLh4LQSR; i(D) It is convenient to recall the main notions and de nitions concerning the description logic DLh4LQSR; i(D) (also called DL4D; ) [4].
Let RA, RD, C, and Ind be denumerable pairwise disjoint sets of abstract role names, concrete role names, concept names, and individual names, respectively. We assume that the set of abstract role names RA contains a name U denoting the universal role.
Data types are introduced through the notion of data type maps, de ned according to [15] as follows. A data type map is a quadruple D = (ND; NC ; NF ; D), where ND is a nite set of data types, NC is a function assigning a set of constants NC (d) to each data type d 2 ND, NF is a function assigning a set of facets NF (d) to each d 2 ND, and D is (i) a function assigning a data type interpretation dD to each data type d 2 ND, (ii) a facet interpretation f D dD to each facet f 2 NF (d), and (iii) a data value edD 2 dD to every constant ed 2 NC (d). Facets determine subsets of data values considered of interest in a speci c application domain. We shall assume that the interpretations of the data types in ND are nonempty pairwise disjoint sets. (a) DL4D; -data types, (b) DL4D; -concepts, (c) DL4D; -abstract roles, and (d) DL4D; concrete role terms are de ned according to the DL standard notation (see [13]) as follows: ! dr j :t1 j t1 u t2 j t1 t t2 j fedg ;
! A j > j ? j :C1 j C1 tC2 j C1 uC2 j fag j 9R:Self j9R:fagj9P:fedg ; ! S j U j R1 j :R1 j R1tR2 j R1uR2 j RC1j j RjC1 j RC1 j C2 j id(C) j ! T j :P1 j P1 t P2 j P1 u P2 j PC1j j Pjt1 j PC1jt1 ; where dr is a data range for D, t1; t2 are data type terms, ed is a constant in NC (d), a is an individual name, A is a concept name, C1; C2 are DL4D; -concept terms, S is an abstract role name, R; R1; R2 are DL4D; -abstract role terms, T is a concrete role name, and P; P1; P2 are DL4D; -concrete role terms. Notice that data type terms are intended to represent derived data types.
A DL4D; -KB is a triple K = (R; T ; A) such that R is a DL4D; -RBox, T is a DL4D; -TBox, and A a DL4D; -ABox.
A DL4D; -RBox is a collection of statements of the following types: R1
R1 R2; Ref(R1);
C1
R1 v R2;
Irref(R1); C2; P1 P2;
R1 : : : Rn v Rn+1;
Dis(R1; R2);
P1 v P2;
Sym(R1);
Tra(R1); Dis(P1; P2);
Asym(R1); Fun(R1); Fun(P1); where R1; R2 are DL4D; -abstract role terms, C1; C2 are DL4D; -abstract concept terms, and P1; P2 are DL4D; -concrete role terms. Any expression of the type R1 : : : Rn v R, where R1; : : : ; Rn; R are DL4D; -abstract role terms, is called a role inclusion axiom (RIA).
A DL4D; -T Box is a set of statements of the types: - C1 - t1
C2, C1 v C2, C1 v 8R:C2, 9R:C1 v C2, t2, t1 v t2, C1 v 8P:t1, 9P:t1 v C1, nR:C1 v C2, C1 v nP:t1 v C1, C1 v nR:C2, nP:t1, where C1; C2 are DL4D; -concept terms, t1; t2 data type terms, R a DL4D; -abstract role term, and P a DL4D; -concrete role term. Statements of the form C v D, where C and D are DL4D; -concept terms, are general concept inclusion axioms.
A DL4D; -ABox is a set of individual assertions of the forms: a : C1; (a; b) : R1; a = b; a 6= b; ed : t1; (a; ed) : P1; with C1 a DL4D; -concept term, d a data type, t1 a data type term, R1 a DL4D; abstract role term, P1 a DL4D; -concrete role term, a; b individual names, and ed a constant in NC (d).
The semantics of DL4D; is given via interpretations of the form I = ( I; D; I), where I and D are nonempty disjoint domains such that dD D, for every d 2 ND, and I is an interpretation function. The interpretation of concepts and roles, axioms and assertions is de ned in [8, Table 2].
Let R, T , and A be as above. An interpretation I = ( I; D; I) is a D-model of R (resp., T ), and we write I j=D R (resp., I j=D T ), if I satis es each axiom in R (resp., T ) according to the semantic rules in [8, Table 2]. Analogously, I = ( I; D; I) is a D-model of A, and we write I j=D A, if I satis es each assertion in A, according to [8, Table 2]. A DL4D; -KB K = (A; T ; R) is consistent if there exists a D-model I = ( I; D; I) of A, T , and R.
The HOCQA problem for DL4D; . We recall that the problem of HigherOrder Conjuctive Query Answering (HOCQA) for DL4D; , introduced in [5], is a generalization of the Conjunctive Query Answering problem for DL4D; de ned in [4]. The HOCQA problem for DL4D; relies on the notion of Higher-Order (HO) DL4D; -conjunctive query, admitting variables of three sorts: individual and data type variables, concept variables, and role variables. The HOCQA problem for DL4D; consists in nding the HO answer set of an HO-DL4D; -conjunctive query (see below) with respect to a DL4D; -KB.
Speci cally, let Vi = fv1; v2; : : :g, Ve = fe1;e2; : : :g, Vd = ft1;t2; : : :g, Vc = fc1; c2; : : :g, Var = fr1; r2; : : :g, and Vcr = fp1; p2; : : :g be pairwise disjoint denumerably in nite sets of variables disjoint from Ind, SfNC (d) : d 2 NDg, C, RA, and RD. HO-DL4D; -atomic formulae are expressions of the following types:
R(w1; w2); P (w1; u); C(w1); t(u); r(w1; w2); p(w1; u); c(w1); t(u); w1 = w2; where w1; w2 2 Vi [Ind, u 2 Ve [SfNC (d) : d 2 NDg, R is a DL4D; -abstract role term, P is a DL4D; -concrete role term, C is a DL4D; -concept term, t is a DL4D; data type term, r 2 Var, p 2 Vcr, c 2 Vc, t 2 Vd. A HO-DL4D; -atomic formula containing no variables is said to be ground. A HO-DL4D; -literal is a HO-DL4D; atomic formula or its negation. A HO-DL4D; -conjunctive query is a conjunction of HO-DL4D; -literals. We denote with the empty HO-DL4D; -conjunctive query.
Let v1; : : : ; vn 2 Vi, e1; : : : ; eg 2 Ve, t1; : : : ; tl 2 Vd,c1; : : : ; cm 2 Vc, r1; : : : ; rk 2 Var, p1; : : : ; ph 2 Vcr, o1; : : : ; on 2 Ind, ed1 ; : : : ; edg 2 SfNC (d) : d 2 NDg, C1; : : : ; Cm 2 C, R1; : : : ; Rk 2 RA, and P1; : : : ; Ph 2 RD. A substitution := fv1=o1; : : : ; vn=on; e1=ed1 ; : : : ; eg=edg ; t1=t1; : : : ; tl=tl; c1=C1; : : : ; cm=Cm; r1=R1; : : : ; rk=Rk; p1=P1; : : : ; ph=Phg is a map such that, for every HO-DL4D; literal L, L is obtained from L by replacing: (a) the occurrences of vi in L with oi, for i = 1; : : : ; n; (b) the occurrences of eb in L with db, for b = 1; : : : ; g; (c) the occurrences of ts in L with ts, for s = 1; : : : ; l; (d) the occurrences of cj in L with Cj , for j = 1; : : : ; m; (e) the occurrences of r` in L with R`, for ` = 1; : : : ; k; (f) the occurrences of pt in L with Pt, for t = 1; : : : ; h. Substitutions can be extended to HO-DL4D; -conjunctive queries in the usual way.
Let Q := (L1 ^ : : : ^ Lm) be a HO-DL4D; -conjunctive query, and KB a DL4D; KB. A substitution involving exactly the variables occurring in Q is a solution for Q w.r.t. KB, if there exists a DL4D; -interpretation I such that I j=D KB and I j=D Q . The collection of the solutions for Q w.r.t. KB is the higher-order answer set of Q w.r.t. KB. Then the higher-order conjunctive query answering problem for Q w.r.t. KB consists in nding the HO answer set of Q w.r.t. KB.
4; can be instantiated to the most signi cant The HOCQA problem for DLD
4; (see [5]).
ABox reasoning problems for DLD Representing DL4D; in set-theoretic terms. DL4D; -KBs and HO-DL4D; conjunctive queries can be represented in set-theoretic terms by exploiting a mapping de ned in [5]. The function translates DL4D; statements in 4LQSRDL4D; formulae in CNF. Speci cally, maps injectively individuals a, constants ed 2 NC (d), variables w 2 Vi, and variables u 2 Ve into sort 0 variables xa, xed , xw, xu, the constant concepts > and ?, data type terms t, concept terms C, c 2 Vc, and t 2 Vd into sort 1 variables X1 , X1 , Xt1, XC1 , Xc1, Xt1 respectively, and the > ? universal relation U , abstract role terms R, concrete role terms P , r 2 Var, and p 2 Vcr into sort 3 variables XU3 , XR3, XP3 , X3, Xp3, respectively.1 r The mapping is de ned for HO-DL4D; -atomic formulae as follows: (R(w1; w2)) := hxw1 ; xw2 i 2 XR3, (P (w1; u)) := hxw1 ; xui 2 XP3 , (C(w1)) := xw1 2 XC1 , (t(u)) := xu 2 Xt1, (w1 = w2) := xw1 = xw2 , (t(u)) := xu 2 Xt1, (c(w1)) := xw1 2 Xc1, (r(w1; w2)) := hxw1 ; xw2 i 2 Xr3, (p(w1; u)) := hxw1 ; xui 2 Xp3.
Finally, is extended to HO-DL4D; -conjunctive queries and to substitutions in a standard way.
From now on we denote with KB the 4LQSRDL4D; translation of a DL4D; -KB KB and with Q the 4LQSRDL4D; -formula representing the HO-DL4D; -conjunctive query Q. The formula
KB is a conjunction of 4LQSRDL4D; -formulae of type (8z1) : : : (8zn)'0, with '0 a clause of 4LQSRDL4D; -literals, since (a) each DL4D; KB KB is a set of statements H such that (H) is a 4LQSRDL4D; -formula in Table 1; and (b) KB is constructed by conjoining the (H)s, moving universal quanti ers as inward as possible, and renaming quanti ed variables as to be pairwise distinct. The interested reader is referred to [6] for full details.
Finally, the HOCQA problem for 4LQSRDL4D; -formulae can be stated as follows. Let be a conjunction of 4LQSRDL4D; -literals and a 4LQSRDL4D; -formula. The HOCQA problem for w.r.t. consists in computing the HO answer set of w.r.t. , namely the collection 0 of all the substitutions 0 such that M j= ^ 0, for some 4LQSRDL4D; -interpretation M. 3
We present a general overview of the reasoner and the main notions and de nitions concerning the procedures upon which it is based.
The input of the reasoner is an OWL ontology serialized in the OWL/XML syntax and admitting SWRL rules (see Figure 1). 1 The use of level 3 variables to model abstract and concrete role terms is motivated by the fact that their elements, that is ordered pairs hx; yi, are encoded in Kuratowski's style as ffxg; fx; ygg, namely as collections of sets of objects.
Let
KB := f :
is a conjunct of rceopnrsetsreuncttisnag ctohmepsalettueraKtiEon-toafbtlheeauDTLK4DB; f-oKrBt.he set
If the ontology meets the DLD coding of all axioms and assertions of the ontology in set-theoretic terms, as a list of strings. Then the system builds the data-structures required to execute the algorithm. In the two subsequent steps, the reasoner constructs a complete KE -tableau TKB whose open branches represent all possible models for the input KB KB (see below for the de nition of KE -tableau). The tableau TKB is constructed (1) by systematically applying the following two rules: (1a) a generalization of the KE-elimination rule incorporating the -rule, and (1b) the principle of bivalence rule (PB-rule) (thus constructing all branches of the KE tableau|see Figure 2), and then (2) processing each open branch # of TKB by constructing the equivalence classes of the individuals involved in formulae of type x = y occurring in # and substituting each individual x on # with the representative of the equivalence class of x. Such step returns the complete KE tableau. Finally, the reasoner takes as input the internal coding of Q, i.e. the set-theoretic representation of a query Q, and computes the HO-answer set of Q with respect to KB. The task of computing the complete KE -tableau for 4; illustrated in [8, Figure 8],
KB is performed by procedure Consistency-DLD whereas the task of computing the HOCQA answer set of a given query w.r.t 4; shown in [8, Figure 9]. the KB is performed by procedure HOCQA -DLD : : : _ n), with 1 : : : n 4LQSRDL4D; -literals. T is a KE -tableau for if there exists a nite sequence T1; : : : ; Tt such that (i) T1 is a one-branch tree consisting of the sequence C1; : : : ; Cp, (ii) Tt = T , and (iii) for each i < t, Ti+1 is obtained from Ti either by an application of one of the rules (E -rule or PB-rule) in Figure 2 or by applying a substitution to a branch # of Ti (in particular, the substitution is applied to each formula X of # and the resulting branch will be denoted with # ). In the de nition of the E -rule reported in Figure 2, (a) := fx1=xo1 : : : xm=xom g is a substitution such that x1; : : : ; xm are the quanti ed variables in and xo1 ; : : : ; xom 2 Var0( KB); and (b) S i := f 1 ; : : : ; n g n f i g is a set containing the complements of all the disjuncts 1 : : : n to which the substitution is applied, with the exception of the disjunct i.
Initially, the procedure Consistency-DL4D; constructs a one-branch KE tableau TKB for the set KB of conjuncts of KB. Then, it expands TKB by systematically applying the E -rule and the PB-rule in Figure 2 to formulae of type = (8x1) : : : (8xm)( 1 _ : : : _ n) till they are all ful lled, giving priority to the E -rule. Once such rules are no longer applicable, for each open branch # of the resulting KE -tableau, atomic formulae of type x = y occurring in # are used to compute the equivalence class of x and y. For each open branch # of TKB, the equivalence class of each variable occurring in # is obtained by computing
At this point, it is convenient to give the de nition of KE -tableaux. Let := fC1; : : : ; Cpg, where each Ci is either a 4LQSRDL4D; -literal of the types in Table 1 or a 4LQSRDL4D; -purely universal quanti ed formula of the form (8x1) : : : (8xm)( 1 _ 4; KBg. The procedure Consistency-DLD
KB of the conjuncts of
KB the substitution # such that # # does not contain literals of type x = y, for distinct x; y. The resulting pair (#; #) is added to the set E .
S i
E -rule i where := (8x1) : : : (8xm)( 1 _ : : : _ n), := fx1=xo1 : : : xm=xom g, and S i := f 1 ; :::; n g n f i g, for i = 1; :::; n
PB-rule A j A where A is a literal
The procedure HOCQA -DL4D; takes as input a query Q and the set E yielded by the procedure Consistency-DL4D; and returns the answer set 0 of
Q w.r.t. KB4.; For each open and complete branch # of TKB, the procedure HOCQA -DLD builds a decision tree D# where each maximal branch induces a substitution 0 such that # 0 belongs to the answer set of Q w.r.t. to KB.
D# is obtained by constructing a stack of its nodes. Initially the stack contains just the root node ( ; Q #) of D#, with the empty substitution. At each step, the procedure pops out from the stack an element ( 0; Q # 0) and iteratively selects a literal q from the query Q # 0 and eliminates it from Q # 0. Then, the set of literals t in # matching q is computed by putting Litq# := ft 2 # : t = q , for some substitution g. The successors of the current node are computed by pushing the node ( 0 ; Q # 0 ) in the stack, for each element in Litq# . If the current node has the form of ( 0; ), with the empty query, the last literal of Q has been treated and the substitution # 0 is inserted in 0. Notice that, in case of a failing query match, the set Litq# is empty and then no successor node is pushed into the stack. Thus, the failing branch of D# is abandoned and another branch is selected by popping one of the nodes of D# from the stack.
Computational complexity results can be found in [9]. We rst show how the internal coding of DL4D; -KBs is represented in terms of 4LQSRDL4D; -formulae and the data-structures used by the reasoner for representing formulae, nodes, and how KE -tableaux are implemented. Then we describe the 4; and most relevant functions that implement the procedures Consistency-DLD 4; and also illustrate an example of reasoning in DL4D; .
HOCQA -DLD
To begin with, 4LQSRDL4D; -variables, quanti ers, Boolean operators, set-theoretic relators, and pairs are mapped into strings as follows. Variables of type Xniame are mapped into strings of the form Vi fnameg. For the sake of uniformity, variables of sort 0 are denoted with X0; Y 0; : : :, whereas individuals a, concepts C, and roles R of a DL4D; -KB are respectively mapped into the variables Xa0, XC1 , and XR3, according to the function described in [5]. The symbols 8, ^, _, :^, :_ are mapped into the strings $FA, $AD, $OR, $DA, $RO, respectively. The relators 2, 62, =, 6= are mapped into the strings $IN, $NI, $EQ, $QE, respectively. A pair hX10; X20i is mapped into the string $OA V01 $CO V02 $AO, where $OA represents the bracket \h", $AO the bracket \i", and $CO the comma symbol.
Then, data-structures for representing the KB are built. 4LQSRDL4D; -variables are implemented by means of the class Var that has four elds. The eld type of type integer indicates the sort of the variable, the eld name of type string represents the name of the variable, and the eld var of type integer represents a free variable if set to 0, and a quanti ed variable if set to 1. The eld index stores the position of the variable in the vector VVL, delegated to collect free variables. Quanti ed and free variables are collected in the vectors VQL and VVL respectively, which provide a subvector for each sort of variable.
The operators admitted in 4LQSRDL4D; , internally coded as strings, are mapped into three vectors that are elds of the class Operator. Speci cally, the vector boolOp contains the values $OR, $AD, $RO, $DA, the vector setOp the values $IN, $EQ, $NI, $QE, $OA, $AO, $CO, and the vector qutOp the value $FA.
4LQSRDL4D; -literals are stored using the class Lit that has two elds. The eld litOp of type integer represents the operator of the formula and corresponds to the index of one of the rst four elements of the vector setOp. The eld components is a vector whose elements point to the variables involved in the literal and stored in VQL and VVL.
4LQSRDL4D; -formulae are represented by the class Formula, having a binary tree structure, whose nodes contain objects of the class Lit. The left and right children contain the left and right subformula, respectively. The class Formula contains the following elds: the eld lit of type pointer to Lit represents the literal; the eld operand represents the propositional operator, and its value is the index of the corresponding element of the vector boolOp; the eld psubformula of type pointer to Formula is the pointer to the father node, whereas the elds lsubformula and rsubformula contain the pointers to the nodes representing the left and the right component of the formula, respectively.
The procedure Consistency-DL4D; is based on the data-structure implemented by the class Tableau. This class uses the instances of the class Node that represents the nodes of the KE -tableau. The class Node has a tree-shaped structure and four elds: the eld setFormula, of type vector of Formula, that collects the formulae of the current node, and three pointers to instances of the class Node. These are the leftchild, rightchild, and father elds, which point to the left child node, right child node, and father node, respectively.
The root node of the class Tableau contains the eld root of type pointer to Node. The elds openbranches and closedbranches collect the set of open branches and of closed branches, respectively. In addition, the class Tableau is provided with the eld EqSet that is a three-dimensional vector of integers storing the equivalence classes induced by atomic formulae of type X0 = Y 0. In particular, EqSet stores a vector containing the indices of VVL corresponding to the variables belonging to the equivalence classes.
As mentioned above, the reasoner takes as input an OWL ontology compat4; requirements, also admitting SWRL rules, and serialized in ible with the DLD the OWL/XML syntax. As rst step, the function readOWLXMLontology produces the internal coding of all axioms and assertions of the ontology, yielding a list of strings. Then the reasoner builds from the output of readOWLXMLontology R the objects of type Formula that implement the 4LQSDL4D; -formulae representing the KB, and stores them in the eld root of an object of type Tableau. In this phase, formulae are transformed in CNF and universal quanti ers are moved as inward as possible and renamed in such a way as to be pairwise distinct. The object of type Tableau representing the KE -tableau is the input to the procedure expandGammaTableau that expands the KE -tableau by iteratively selecting and ful lling purely universal quanti ed input formulae. Once a purely universal quanti ed formula has been selected, expandGammaTableau builds iteratively the set of substitutions to be applied to the selected formula. A substitution is a map from the indices of the quanti ed variables of the formula, selected in order of appearance, to the elements of the vector VVL. The implementation of applies standard techniques for computing the variations with repetition of the set of indices of the elements of VVL taken to k by k, where k is the number of quanti ed variables occurring in the selected formula.
The procedure expandGammaTableau ful lls the formula selected by systematically applying the functions EGrule with the current and PBrule, respectively implementing the E -rule and the PB-rule. More precisely, it works as follows. The disjuncts of the current formula to which is applied are stored in a temporary vector and selected iteratively. If a disjunct has its negation on the branch, it is removed from the temporary vector. Once all the elements of the temporary vector have been selected, if the last one does not have its negation on the branch, then EGrule is applied to the formula and the last element of the temporary vector is inserted in the branch according to Figure 2. If there is more than one element left in the temporary vector, then the procedure PBrule is applied. In case the stack is empty, a contradiction is found and the branch gets closed and inserted in the vector closedbranches.
If the procedure expandGammaTableau terminates with some elements in openbranches, then the reasoner builds the set of equivalence classes of the variables involved in formulae of type X0 = Y 0, for each element of openbranches by means of the procedure buildsEqSet. The latter procedure updates the eld EqSet of the object of type Tableau with the new information concerning the set of equivalence classes. After the execution of buildsEqSet, if openbranches contains some elements, a consistent KB is returned.
Procedure HOCQA -DLD that takes as input the object of type Tableau returned by buildsEqSet and a string representing the internal coding of the input query Q, and returns an object of type QueryManager storing, among other information, the answer set of
Q w.r.t. KB. The function performQuery uses an object of type QueryManager that stores the input query Q as a string, an object of type Formula representing
Q, and the answer set of Q w.r.t. KB, for each element of openbranches. The answer set is implemented by endowing the object of type QueryManager with the pair of vectors VarMatch. The rst vector of VarMatch contains an integer for each element in openbranches: this is set to 1 if the corresponding branch has solution, 0 otherwise. The second (three-dimensional) vector contains for each element in openbranches a vector of solutions, each one constituted by a vector of pairs of pointers to Var. The rst Var of such pair is a variable belonging to the query, whereas the second Var is the matched individual.
For each element in openbranches, the function performQuery implements a decision tree by means of a stack that keeps track of the partial solutions of the query, as nodes of the decision tree. Such a stack, called matchSet, is constituted by a vector of pairs of objects of type Var such that the rst one represents the query variable and the second one the matched element. Initially, matchSet is empty. At rst step, the procedure selects the rst conjunct of the query and, for each match found, it pushes in matchSet a vector of pairs representing the match. The procedure selects iteratively the conjuncts of the query and then applies to the selected conjunct the substitution that is currently at the top of matchSet. If the literal obtained by the application of such partial solution has one or more matches in the branch, the resulting substitutions are pushed in matchSet. Once all the literals of the query have been processed, if matchSet is not empty, it contains the leaves of the maximal branches of the decision tree, which are all added to VarMatch.
The KB in terms of 4LQSRDL4D; is the following formula:
KB := h:x(AhxnEn;vxa;AxnAnnin2i 2XR3XeMl3atoitvheer^)h^xEva; xEvai 2 XR3elative ^
(8z1)(8z2)(:(hz1; z2i 2 XM3other) _ hz1; z2i 2 XR3elative)
Let Q = hz; xEvai 2 XM3other be a query represented in set-theoretic terms. A complete KE -tableau for KB and the decision trees constructed for the evaluation of Q on each open branch of the KE -tableau are shown in Figure 4. Notice that, the decision tree constructed on the leftmost open branch of the KE -tableau provides no solution.
The internal representation of the OWL ontology is shown in Figure 5. The KE -tableau computed by the reasoner and the evaluation of the query Q are reported in Figure 6. Finally, Figure 7 shows a performance comparison between our implementation of the KE-tableau presented in [7] and the KE -tableau system for DL4D; presented in this paper. The metric used in the benchmarking is the number of models of the input KB computed by the reasoners and the time required to compute such models. As shown in Figure 7, the KE -tableau has a better performance than the KE-tableau up to about 400%, even if in some cases the performances of the two systems are comparable, as shown in the plot. We conclude that the KE -tableau system is always convenient, also because the expansions of quanti ed formulae are not stored in memory. We presented a C++ implementation of a KE -tableau system for the most widespread reasoning tasks of DL4D; , such as consistency checking of DL4D; -KBs and a generalization of the CQA problem for DL4D; , , called HOCQA problem, admitting conjunctive queries with variables of three sorts. These problems have been addressed by translating DL4D; -KBs and higher-order DL4D; -conjunctive queries in terms of formulae of the set-theoretic fragment 4LQSRDL4D; . The reasoner is an improvement of the KE-tableau system introduced in [7] to check consistency of DL4D; -KBs, as it admits a generalization of the KE-elimination rule incorporating the -rule. The reasoner takes as input OWL ontologies compatible with the speci cations of DL4D; serialized in the OWL/XML format and admitting SWRL rules.
Finally, we showed that the reasoner presented in this paper is more e cient than the one introduced in [7], by means of suitable benchmark test sets.
We plan to extend the set-theoretic fragment underpinning the reasoner to include also a restricted version of the operator of relational composition. This will allow ones to reason with description logics that admit full existential and universal quanti cation. In addition, we intend to improve our reasoner so as to deal with the reasoning problem of ontology classi cation. Then, we shall compare the resulting reasoner with existing well-known reasoners such as HermiT [12] and Pellet [18], providing some benchmarking. We also plan to allow data type reasoning by either integrating existing solvers for the Satis ability Modulo Theories (SMT) problem or by designing ad-hoc new solvers. Finally, as each branch of the KE -tableau can be computed by a single processing unit, we plan to implement a parallel version of the software by using the Nvidia CUDA library.