We address the problem of Conjunctive Query Answering (CQA) for the description logic DLh4LQSR,×i(D) (DL4D,×, for short) which extends the logic DLh4LQSRi(D) with Boolean operations on concrete roles and with the product of concepts. The result is obtained by formalizing DL4D,×-knowledge bases and DL4D,×conjunctive queries in terms of formulae of the four-level set-theoretic fragment 4LQSR, which admits a restricted form of quantification on variables of the first three levels and on pair terms. We solve the CQA 4,× through a decision procedure for the satisfiability problem for DLD problem of 4LQSR. We further define a KE-tableau based procedure for the same problem, more suitable for implementation purposes, and analyze its computational complexity.
In the last few years, results from Computable Set Theory have been used as a
means to represent and reason about description logics and rule languages for
the semantic web. For instance, in [
Copyright c by the paper’s authors. Copying permitted for private and academic
purposes.
in the decidable four-level stratified fragment of set theory 4LQSR involving a
restricted form of quantification over variables of the first three levels and pair
terms (cf. [
The consistency problem for DL4D-knowledge bases has been proved decidable
in [
In this paper we exploit decidability results presented in [
In particular, we introduce the description logic DLh4LQSR,×i(D) (DL4D,×, for
4
short), extending DLD with Boolean operations on concrete roles and with the
4,× and prove its
product of concepts. Then we define the CQA problem for DLD
decidability via a reduction to the CQA problem for 4LQSR, whose decidability
follows from that of the satisfiability problem for 4LQSR (proved in [
The set-theoretic fragment 4LQSR
It is convenient to first introduce the syntax and semantics of a more general
four-level quantified language, denoted 4LQS. Then we provide some restrictions
on quantified formulae of 4LQS that characterize 4LQSR. We recall that the
satisfiability problem for 4LQSR has been proved decidable in [
4LQS involves four collections, Vi, of variables of sort i, for i = 0, 1, 2, 3. Variables of sort i, for i = 0, 1, 2, 3, will be denoted by Xi, Y i, Zi, . . . (in particular, variables of sort 0 will also be denoted by x, y, z, . . .). In addition to variables, 4LQS involves also pair terms of the form hx, yi, with x, y ∈ V0. 4LQS-quantifier-free atomic formulae are classified as: - level 0: x = y, x ∈ X1, hx, yi = X2, hx, yi ∈ X3; - level 1: X1 = Y 1, X1 ∈ X2; - level 2: X2 = Y 2,
X2 ∈ X3. 4LQS purely universal formulae are classified as: - level 1: (∀z1) . . . (∀zn)ϕ0, where z1, . . . , zn ∈ V0 and ϕ0 is any propositional combination of quantifier-free atomic formulae of level 0; - level 2: (∀Z11) . . . (∀Zm1)ϕ1, where Z11, . . . , Zm1 ∈ V1 and ϕ1 is any propositional combination of quantifier-free atomic formulae of levels 0 and 1, and of purely universal formulae of level 1; - level 3: (∀Z12) . . . (∀Zp2)ϕ2, where Z12, . . . , Z2 p ∈ V2 and ϕ2 is any propositional combination of quantifier-free atomic formulae and of purely universal formulae of levels 1 and 2. 4LQS-formulae are all the propositional combinations of quantifier-free atomic formulae of levels 0, 1, 2 and of purely universal formulae of levels 1, 2, 3.
Let ϕ be a 4LQS-formula. Without loss of generality, we can assume that ϕ contains only ¬, ∧, ∨ as propositional connectives. Further, let Sϕ be the syntax tree for a 4LQS-formula ϕ,1 and let ν be a node of Sϕ. We say that a 4LQS-formula ψ occurs within ϕ at position ν if the subtree of Sϕ rooted at ν is identical to Sψ. In this case we refer to ν as an occurrence of ψ in ϕ and to the path from the root of Sϕ to ν as its occurrence path. An occurrence of ψ within ϕ is positive if its occurrence path deprived by its last node contains an even number of nodes labelled by a 4LQS-formula of type ¬χ. Otherwise, the occurrence is said to be negative.
The variables z1, . . . , zn are said to occur quantified in (∀z1) . . . (∀zn)ϕ0.
Likewise, Z11, . . . , Zm1 and Z12, . . . , Zp2 occur quantified in (∀Z11) . . . (∀Zm1)ϕ1 and in
(∀Z12) . . . (∀Z2)ϕ2, respectively. A variable occurs free in a 4LQS-formula ϕ if it
p
does not occur quantified in any subformula of ϕ. For i = 0, 1, 2, 3, we denote
with Vari(ϕ) the collections of variables of level i occurring free in ϕ.
1 The notion of syntax tree for 4LQS-formulae is similar to the notion of syntax tree
for formulae of first-order logic. A precise definition of the latter can be found in [
A (level 0) substitution σ := {x1/y1, . . . , xn/yn} is the mapping ϕ 7→ ϕσ such that, for any given 4LQS-formula ϕ, ϕσ is the 4LQS-formula obtained from ϕ by replacing the free occurrences of the variables x1, . . . , xn in ϕ with the variables y1, . . . , yn, respectively. We say that a substitution σ is free for ϕ if the formulae ϕ and ϕσ have exactly the same occurrences of quantified variables.
A 4LQS-interpretation is a pair M = (D, M ) where D is a non-empty collection of objects (called domain or universe of M) and M is an assignment over the variables in Vi, for i = 0, 1, 2, 3, such that: M X0 ∈ D, M X1 ∈ P(D), M X2 ∈ P(P(D)), M X3 ∈ P(P(P(D))), where Xi ∈ Vi, for i = 0, 1, 2, 3, and P(s) denotes the powerset of s.
Pair terms are interpreted à la Kuratowski, and therefore we put
M hx, yi := {{M x}, {M x, M y}}. - M = (D, M ) be a 4LQS-interpretation, - x1, . . . , xn ∈ V0, X11, . . . , Xm1 ∈ V1, X12, . . . , Xp2 ∈ V2, and - u1, . . . , un ∈ D, U11, . . . , U m1 ∈ P(D), U12, . . . , Up2 ∈ P(P(D)). By M[~x/~u, X~ 1/U~ 1, X~ 2/U~ 2], we denote the interpretation M0 = (D, M 0) such that M 0xi = ui (for i = 1, . . . , n), M 0Xj1 = Uj1 (for j = 1, . . . , m), M 0Xk2 = Uk2 (for k = 1, . . . , p), and which otherwise coincides with M on all remaining variables. For a 4LQS-interpretation M = (D, M ) and a 4LQS-formula ϕ, the satisfiability relationship M |= ϕ is defined inductively over the structure of ϕ as follows. Quantifier-free atomic formulae are evaluated in a standard way according to the usual meaning of the predicates ‘∈’ and ‘=’, and purely universal formulae are evaluated as follows: - M |= (∀z1) . . . (∀zn)ϕ0 iff M[~z/~u] |= ϕ0, for all ~u ∈ Dn; - M |= (∀Z11) . . . (∀Zm1)ϕ1 iff M[Z~ 1/U~ 1] |= ϕ1, for all U~ 1 ∈ P(D) m; - M |= (∀Z12) . . . (∀Zp2)ϕ2 iff M[Z~ 2/U~ 2] |= ϕ2, for all U~ 2 ∈ P(P(D)) p. Finally, compound formulae are interpreted according to the standard rules of propositional logic. If M |= ϕ, then M is said to be a 4LQS-model for ϕ. A 4LQS-formula is said to be satisfiable if it has a 4LQS-model. A 4LQS-formula is valid if it is satisfied by all 4LQS-interpretations.
We are now ready to present the fragment 4LQSR of 4LQS of our interest. This is the collection of the formulae ψ of 4LQS fulfilling the restrictions: 1. for every purely universal formula (∀Z11) . . . (∀Zm1)ϕ1 of level 2 occurring in ψ and every purely universal formula (∀z1) . . . (∀zn)ϕ0 of level 1 occurring negatively in ϕ1, ϕ0 is a propositional combination of quantifier-free atomic formulae of level 0 and the condition
¬ϕ0 → is a valid 4LQS-formula (in this case we say that (∀z1) . . . (∀zn)ϕ0 is linked to the variables Z11, . . . , Zm1);
Vin=1 Vjm=1 zi ∈ Zj1 2. for every purely universal formula (∀Z12) . . . (∀Zp2)ϕ2 of level 3 in ψ: - every purely universal formula of level 1 occurring negatively in ϕ2 and not occurring in a purely universal formula of level 2 is only allowed to be of the form with Yi2j ∈ V2, for i, j = 1, . . . , n; - purely universal formulae (∀Z11) . . . (∀Zm1)ϕ1 of level 2 may occur only positively in ϕ2.
Restriction 1 has been introduced for technical reasons concerning the
decidability of the satisfiability problem for the fragment, while restriction 2 allows
one to define binary relations and several operations on them (for space reasons
details are not included here but can be found in [
The semantics of 4LQSR plainly coincides with that of 4LQS.
The description logic DLh4LQSR,×i(D) (more simply referred to as DL4D,×) is
4 ) presented in [
As far as the construction of role inclusion axioms is concerned, DL4D,× is
more liberal than SROIQ(D) [
Datatypes are defined according to [
A facet expression for a datatype d ∈ ND is a formula ψd constructed from the elements of NF (d) ∪ {>d, ⊥d} by applying a finite number of times the connectives ¬, ∧, and ∨. The function ·D is extended to facet expressions for d ∈ ND by putting >dD = dD, ⊥dD = ∅, (¬f )D = dD \ f D, (f1 ∧ f2)D = f1D ∩ f2D, and (f1 ∨ f2)D = f1D ∪ f2D, for f, f1, f2 ∈ NF (d).
A data range dr for D is either a datatype d ∈ ND, or a finite enumeration of datatype constants {ed1 , . . . , edn }, with edi ∈ NC (di) and di ∈ ND, or a facet expression ψd, for d ∈ ND, or their complementation.
Let RA, RD, C, 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. (a) DL4D,×-datatype, (b) DL4D,×-concept, (c) DL4D,×-abstract role, and (d) DL4D,×concrete role terms are constructed according to the following syntax rules: (a) t1, t2 −→ dr | ¬t1 | t1 u t2 | t1 t t2 | {ed} , (b) C1, C2 −→ A | > | ⊥ | ¬C1 | C1 t C2 | C1 u C2 | {a} | ∃R.Self |∃R.{a}|∃P.{ed} , (c) R1, R2 −→ S | U | R1− | ¬R1 | R1 t R2 | R1 u R2 | RC1| | R|C1 | RC1 | C2 | id(C) |
C1 × C2 , (d) P1, P2 −→ T | ¬P1 | P1 t P2 | P1 u P2 | PC1| | P|t1 | PC1|t1 , 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.
A DL4D,×-knowledge base is a triple KB = (R, T , A) such that R is a DL4D,×RBox , T is a DL4D,×-TBox , and A a DL4D,×-ABox (see next).
A DL4D,×-RBox is a collection of statements of the following forms: R1 ≡ R2, R1 v R2, R1 . . . Rn v Rn+1, Sym(R1), Asym(R1), Ref(R1), Irref(R1), Dis(R1, R2), Tra(R1), Fun(R1), R1 ≡ C1 × C2, P1 ≡ P2, P1 v P2, Dis(P1, P2), 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 w v R, where w is a finite string of DL4D,×-abstract role terms and R is an DL4D,×-abstract role term is called a role inclusion axiom (RIA).
Next, a DL4D,×-TBox is a set of statements of the types: C1 ≡ C2, C1 v C2, C1 v ∀R1.C2, ∃R1.C1 v C2, ≥nR1.C1 v C2, C1 v ≤nR1.C2, t1 ≡ t2, t1 v t2, C1 v ∀P1.t1, ∃P1.t1 v C1, ≥nP1.t1 v C1, C1 v ≤nP1.t1, where C1, C2 are DL4D,×-concept terms, t1, t2 datatype terms, R1 a DL4D,×-abstract role term, and P1 a DL4D,×-concrete role term. Any statement C v D, with C and D DL4D,×-concept terms, is a general concept inclusion axiom (GCI).
Finally, a DL4D,×-ABox is a set of individual assertions of the forms: a : C1,
(a, b) : R1, a = b, ed : t1, (a, ed) : P1, with a, b individual names, C1 a
DL4D,×concept term, R1 a DL4D,×-abstract role term, d a datatype, ed a constant in NC (d),
t1 a datatype term, and P1 a DL4D,×-concrete role term. As mentioned above,
4,× is more liberal than SROIQ(D) in the construction of role inclusion
DLD
axioms. For example, the role hierarchy {RS v S, RT v R, V T v T, V S v V }
presented in [
The semantics of DLD and ΔD are non-empty disjoint domains such that dD ⊆ ΔD, for every d ∈ ND, and ·I is an interpretation function. The interpretation of concepts and roles, and of axioms and assertions is illustrated in [3, Table 1].
Let KB = (R, T , A) be a DL4D,×-knowledge base. An interpretation I = (ΔI, ΔD, ·I) is a D-model of R (and write I |=D R) if I satisfies each axiom in R according to the semantic rules in [3, Table 1]. Similar definitions hold for T and A too. Then I satisfies KB (and write I |=D KB) if it is a D-model of R, T , and A. A knowledge base is consistent if it is satisfied by some interpretation. 3 4,×
Conjunctive Query Answering for DLD Let V = {v1, v2, . . .} be a denumerable and infinite set of variables disjoint from Ind and from S{NC (d) : d ∈ ND}. A DL4D,×-atomic formula is an expression of of the following types
R(w1, w2),
P (w1, u1),
C(w1), w1 = w2, u1 = u2, where w1, w2 ∈ V ∪ Ind, u1, u2 ∈ V ∪ S{NC (d) : d ∈ ND}, R is a DL4D,×abstract role term, P is a DL4D,×-concrete role term, and C is a DL4D,×-concept term. A DL4D,×-atomic formula containing no variables is said to be closed. A 4,×-literal is a DL4D,×-atomic formula or its negation. A DL4D,×-conjunctive DLD
4,×-literals. Let v1, . . . , vn ∈ V and o1, . . . , on ∈ query is a conjunction of DLD Ind ∪ S{NC (d) : d ∈ ND}. A substitution σ := {v1/o1, . . . , vn/on} is a map 4,×-literal L, Lσ is obtained from L by replacing the such that, for every DLD occurrences of v1, . . . , vn in L with o1, . . . , on, respectively. Substitutions can be extended to DL4D,×-conjunctive queries in the usual way. Let Q := (L1 ∧ . . . ∧ Lm) be a DL4D,×-conjunctive query, and KB a DL4D,×-knowledge base. 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 |=D KB and I |=D Qσ. The collection Σ of the solutions for Q w.r.t. KB is the answer set of Q w.r.t. KB. Then the conjunctive query answering (CQA) problem for Q w.r.t. KB consists in finding the answer set Σ of Q w.r.t. KB.
We shall solve the CQA problem just stated by reducing it to the
analogous problem formulated in the context of the fragment 4LQSR (and in turn
to the decision procedure for 4LQSR presented in [
The following theorem states that also the CQA problem for DL4D,× is decidable.
Theorem 1. Given a DLD4,×-knowledge base KB and a DL4D,×-conjunctive query Q, the CQA problem for Q w.r.t. KB is decidable.
Proof (sketch). For space reasons we just outline the main ideas of the proof.
The interested reader, however, can find complete details in the extended version
of this paper (see [
As remarked above, the CQA problem for DL4D,× can be solved via an effective reduction to the CQA problem for 4LQSR-formulae, and then exploiting Lemma 1. The reduction is accomplished through a function θ that maps effectively variables in V and individuals in Ind into variables of sort 0 (of the 4LQSR-language), etc., DL4D,×-TBoxes, -RBoxes, and -ABoxes, and DL4D,×-conjunctive queries into 4LQSR-formulae in conjunctive normal form (CNF), which can be used to map effectively CQA problems from the DL4D,×-context into the 4LQSR-context. More specifically, given a DL4D,×-knowledge base KB and a DL4D,×-conjunctive query Q, using the function θ we can effectively construct the following 4LQSR-formulae in CNF:
φKB := VH∈KB θ(H) ∧ Vi1=2 1 ξi, ψQ := θ(Q) .2 Then, if we denote by Σ the answer set of Q w.r.t. KB and by Σ0 the answer set of ψQ w.r.t. φKB, we have that Σ consists of all substitutions σ (involving exactly the variables occurring in Q) such that θ(σ) ∈ Σ0. Since, by Lemma 1, Σ0 can be computed effectively, then Σ can be computed effectively too. above requirements, to compute the answer set of ψ w.r.t. φ, for each candidate substitution σ0 := {x1/y1, . . . , xn/yn} (with {x1, . . . , xn} = Var0(ψ) and {y1, . . . , yn} ⊆ Var0(φ)) one has just to test for satisfiability the 4LQSR-formula φ ∧ ψσ0. Since the number of possible candidate substitutions is |Var0(φ)||Var0(ψ)| and the satisfiability problem for 4LQSR-formulae is the decidable, it follows that the answer set of ψ w.r.t. φ can be computed effectively. Summarizing, Lemma 1. The CQA problem for 4LQSR-formulae is decidable. 4
In this section, we illustrate a KE-tableau based procedure that, given a
4LQSRformula φKB corresponding to a DL4D,×-knowledge base and a 4LQSR-formula
2 The definition of the function θ is inspired to that of the function τ introduced in the
proof of Theorem 1 in [
Let φKB be the formula obtained from φKB by: - moving universal quantifiers in φKB as inwards as possible according to the rule (∀z)(A(z) ∧ B(z)) ←→ ((∀z)A(z) ∧ (∀z)B(z)), - renaming universally quantified variables so as to make them pairwise distinct.
Exp(Si) := formLuetlaFe1a, n.d.. ,SF1,k. b..e,tShme ctohnejuconnctjusnocftφsKoBf φthKaBt tahreat4LarQeS4RL-qQuSaRn-tpifiuerer-lyfreuenaivtoermsaicl formulae. For every Si = (∀z1i) . . . (∀znii )χi, i = 1, . . . , m, we put V
Si{z1i/xa1 , . . . , znii /xani }. {xa1 ,...,xani }⊆Var0(φKB)
m Let ΦKB := {Fj : i = 1, . . . , k} ∪ S Exp(Si).
i=1
To prepare for the KE-tableau based procedure to be described next, we
introduce some useful notions and notations (see [
Let Φ = {C1, . . . , Cp} be a collection of disjunctions of 4LQSR-quantifier-free atomic formulae of level 0 of the types: x = y, x ∈ X1, hx, yi ∈ X3. T is a KE-tableau for Φ if there exists a finite 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 by an application of one of the rules in Fig 1. The set of formulae Siβ = {β1, . . . , βn} \ {βi} occurring as premise in the E-rule contains the complements of all the components of the formula β with the exception of the component βi.
β1 ∨ . . . ∨ βn βi
β Si
E-Rule wfohreire=S1iβ, .:.=., n{β1, ..., βn} \ {βi}, A | A with A a literal
PB-Rule
Let T be a KE-tableau. A branch ϑ of T is closed if it contains both A and ¬A, for some formula A. Otherwise, the branch is open. A formula β1 ∨ . . . ∨ βn is fulfilled in a branch ϑ, if βi is in ϑ, for some i = 1, . . . , n. A branch ϑ is complete if every formula β1 ∨ . . . ∨ βn occurring in ϑ is fulfilled. A KE-tableau is complete if all its branches are complete.
Next we introduce the procedure Saturate-KB that takes as input the set ΦKB constructed from a 4LQSR-formula φKB representing a DL4D,×-knowledge base KB as shown above, and yields a complete KE-tableau TKB for ΦKB.
1. TKB := ΦKB;
(a) Select a formula β1 ∨ . . . ∨ βn on ϑ that is not fulfilled. (b) If Sjβ is in ϑ, for some j ∈ {1, . . . , n}, apply the E-Rule to β1 ∨ . . . ∨ βn and
Sjβ on ϑ and go to step 2. (c) If Sjβ is not in ϑ, for every j = 1, . . . , n, let Bβ be the collection of formulae β1, . . . , βn present in ϑ and let βh be the lowest index formula such that βh ∈ {{β1, . . . , βn} \ Bβ}, then apply the PB-rule to βh on ϑ, and go to step 2.
Soundness of Procedure 1 can be easily proved in a standard way and its
completeness can be shown much along the lines of Proposition 36 in [
By the completeness of Procedure 1, each open branch ϑ of TKB induces a 4LQSR-interpretation Mϑ such that Mϑ |= ΦKB. We define Mϑ = (Dϑ, Mϑ) as follows. We put Dϑ := {x ∈ V0 : x occurs in ϑ}; Mϑx := x, for every x ∈ Dϑ; MϑXC1 = {x : x ∈ XC1 is in ϑ}, for every XC1 ∈ V1 occurring ϑ; MϑXR3 = {hx, yi : hx, yi ∈ XR3 is in ϑ}, for every XR3 ∈ V3 occurring in ϑ. It is easy to check that Mϑ |= φKB and thus, plainly, that Mϑ |= φKB.
Next, we provide some complexity results. Let r be the maximum number of universal quantifiers in Si, and k := |Var0(φKB)|. Then, each Si generates kr expansions. Since the knowledge base contains m such formulae, the number of disjunctions in the initial branch of the KE-tableau is m · kr. Next, let ` be the maximum number of literals in Si, for i = 1, . . . , m. Then, the maximum depth of the KE-tableau, namely the maximum size of the models of ΦKB constructed as illustrated above, is O(`mkr) and the number of leaves of the tableau, that is the number of such models of ΦKB, is O(2`mkr ).
We now describe a procedure that, given a KE-tableau constructed by Procedure 1 and a 4LQSR-formula ψQ representing a DL4D,×-conjunctive query Q, yields all the substitutions σ0 in the answer set Σ0 of ψQ w.r.t. φKB. By the soundness of Procedure 1, we can limit ourselves to consider only the models Mϑ of φKB induced by each open branch ϑ of TKB. For every open and complete branch ϑ of TKB, we construct a decision tree Dϑ such that every maximal branch of Dϑ defines a substitution σ0 such that Mϑ |= ψQσ0.
Let d be the number of literals in ψQ. Dϑ is a finite labelled tree of depth d + 1 whose labelling satisfies the following conditions, for i = 0, . . . , d: (i) every node of Dϑ at level i is labelled with (σi, ψQσi), and, in particular, the root is labelled with (σ00, ψQσ00), where σ00 is the empty substitution; (ii) if a node at level i is labelled with (σi0, ψQσi0), then its s-successors, with s > 0, are labelled with σi0%q1i+1, ψQ(σi0%q1i+1) , . . . , σi0%qsi+1, ψQ(σi0%qsi+1) , where qi+1 is the (i + %qi+1, . . . , %qi+1} is the collection of the 1)-st conjunct of ψQσi0 and Sqi+1 = { 1 s substitutions % = {x1/y1, . . . , xj /yj } with {x1, . . . , xj } = Var0(qi+1) such that p = qi+1%, for some literal p on ϑ. If s = 0, the node labelled with (σi0, ψQσi0) is a leaf node and, if i = d, σi0 is added to Σ0.
Let δ(TKB) and λ(TKB) be, respectively, the maximum depth of TKB and
the number of leaves of TKB computed above. Plainly, δ(TKB) = O(`mkr) and
λ(TKB) = O(2`mkr ). It is easy to verify that s = 2k is the maximum branching
of Dϑ. Since Dϑ is a s-ary tree of depth d + 1, where d is the number of literals
in ψQ, and the s-successors of a node are computed in O(δ(TKB)) time, the
number of leaves in Dϑ is O(s(d+1)) = O(2k(d+1)) and they are computed in
O(2k(d+1)δ(TKB)) time. Finally, since we have λ(TOK(B2)k(odf+1s)uδc(hTKdBe)cλis(iToKnBt)r)ee=s,
the answer· `smetkrof· 2ψ`Qmkr ) = O(`mkr2k(d+1)+`mkr ) time. Since the size of φKB
w.r.t. φKB is computed in
O(2k(d+1)
and of ψQ are polynomially related to those of KB and of Q, respectively (see [
We have introduced the description logic DLh4LQSR,×i(D) (DL4D,×, for short) that extends the logic DLh4LQSRi(D) with Boolean operations on concrete roles and with the product of concepts. We addressed the problem of Conjunctive Query 4,× by formalizing DL4D,×-knowledge bases Answering for the description logic DLD and DL4D,×-conjunctive queries in terms of formulae of 4LQSR. Such formalization seems to be promising for implementation purposes.
In our approach, we first constructed a KE-tableau TKB for φKB, a 4LQSRformalization of a given DL4D,×-knowledge base KB, whose branches induce the smeondtienlgs oaf DφKLB4D,.×T-choennjuwnectciovmepquuteerdy tQh,e wanitshwreersspeetcotftao 4φLKQBSbRy-fomrmeaunlsa oψfQa, froerpersetof decision trees based on the branches of TKB and gave some complexity results.
We plan to generalize our procedure with a data-type checker in order to extend reasoning with data-types, and also to extend 4LQSR with data-type groups. We also intend to improve the efficiency of the knowledge base saturation algorithm and query answering algorithm, and to extend the expressiveness of the queries. Finally, we intend to study a parallel model of the procedure described and to provide an implementation of it.