Combining CPDL (Propositional Dynamic Logic with Converse) and regular grammar logic results in an expressive modal logic denoted by CPDLreg. This logic covers TeamLog, a logical formalism used to express properties of agents' cooperation in terms of beliefs, goals and intentions. It can also be used as a description logic for expressing terminological knowledge, in which both regular role inclusion axioms and CPDL-like role constructors are allowed. In this paper, we develop an expressive rule language called Horn-CPDLreg that has PTime data complexity. As a special property, this rule language allows the concept constructor \universal restriction" to appear at the left hand side of general concept inclusion axioms. We use a special semantics for Horn-CPDLreg that is based on pseudo-interpretations. It is called the constructive semantics and coincides with the traditional semantics when the concept constructor \universal restriction" is disallowed at the left hand side of concept inclusion axioms or when the language is used as an epistemic formalism and the accessibility relations are serial. We provide an algorithm with PTime data complexity for checking whether a knowledge base in Horn-CPDLreg has a pseudo-model. This shows that the instance checking problem in Horn-CPDLreg with respect to the constructive semantics has PTime data complexity.
ular grammar logic [
to express properties of agents' cooperation in terms of beliefs, goals and intentions. It can also be used as a description logic, in which both regular role inclusion axioms and CPDL-like role constructors are allowed.
Description logics (DLs) are variants of modal logics suitable for expressing terminological knowledge. They represent the domain of interest in terms of individuals (objects), concepts and roles. A concept stands for a set of individuals, a role stands for a binary relation between individuals. In comparison with modal logic, concepts correspond to formulas, role names correspond to modal indices, roles correspond to programs in dynamic logic, and the constructors 8R:C and
1.1
Related Work and Motivation
hard [25]. The hardness is caused by that basic roles are not required to be serial (i.e., to satisfy the condition 8x9y R(x; y)). A naive approach for overcoming the
side) of v in TBox axioms [
E L [
More sophisticated approaches for dealing with the mentioned NP-hardness are as follows: { allowing 8R:C to appear at the LHS of v in TBox axioms when R is serial and using the traditional semantics for it, { allowing a special kind of 8R:C like 89R:C (de ned as 8R:C u 9R:C) to appear at the LHS of v in TBox axioms and using the traditional semantics for it, { allowing 8R:C to appear at the LHS of v in TBox axioms and using a special semantics for it.
works [21{24, 8, 32, 30, 11, 29, 28] on rule languages in propositional modal and description logics follow the rst two of the above approaches.
The objective of this paper is to formulate an as rich as possible Horn fragment in CPDLreg together with an appropriate semantics for it. As discussed in [25, 28], for R 2 R, the concept constructor 89R:C is more constructive than
a constructor similar to [ ]3 ' of [23] seems to be too strong and complicated for practical applications. A natural question is: Can the concept constructor 8R:C be directly used at the LHS of v in TBox axioms? Our answer is: Yes, why not? To obtain the PTime data complexity, just formulate and use an appropriate semantics for that constructor. 1.2
Our Contributions and the Structure of This Paper
concept constructors 89R:C and 8R:C to appear at the LHS of v in TBox axioms. We use a special semantics for Horn-CPDLreg that is based on pseudointerpretations. It is called the constructive semantics and coincides with the traditional semantics when the concept constructor 8R:C is disallowed at the
and the accessibility relations are serial. We provide an algorithm with PTime data complexity for checking whether a knowledge base in Horn-CPDLreg has a pseudo-model. This shows that the instance checking problem in Horn-CPDLreg with respect to the constructive semantics has PTime data complexity.
and semantics of CPDLreg. Section 3 de nes the rule language Horn-CPDLreg.
ties. Section 5 provides our algorithm for checking whether a given knowledge base in Horn-CPDLreg has a pseudo-model. Section 6 contains concluding remarks. Due to the lack of space, proofs of our results are presented in [27]. 2
role names, and a nite set I of individual names. We use letters like a, b to denote individual names, letters like A, B to denote concept names, and letters like r, s to denote role names. We use r to denote the inverse of r. For R = r, let R stand for r. Let R = fr j r 2 R+g and R = R+ [ R . We call the roles from R basic roles.
duction rules R ! S1 : : : Sk over alphabet R (i.e., R, S1, . . . , Sk 2 R). It is symmetric if, for every rule R ! S1 : : : Sk of S, the rule R ! Sk : : : S1 is also in S.1 It is regular if, for every R 2 R, the set of words derivable from R using the system is a regular language over R.
no designated start symbol and there is no distinction between terminal and non-terminal symbols. We assume that, for R 2 R, the word R is derivable from
S1 Sk v R, where k 0 and S1; : : : ; Sk; R 2 R. In the case k = 0, the
fR ! S1 : : : Sk j (S1
Sk v R) 2 Rg is a symmetric regular semi-Thue system S over R. We assume that R is given together with a mapping A that associates every R 2 R with a nite automaton AR recognizing the words derivable from R using S. We call A the RIAautomaton-speci cation of R. 1 In the case k = 0, the right hand sides of the rules stand for ". >I = I ?I = ; (:C)I = I n CI (C u D)I = CI \ DI (C t D)I = CI [ DI (8R:C)I = fx 2 I j 8y (hx; yi 2 RI ) y 2 CI )g (9R:C)I = fx 2 I j 9y (hx; yi 2 RI ^ y 2 CI )g "I = fhx; xi j x 2 RI = (RI ) 1 (R
S)I = RI SI (R t S)I = RI [ SI (R )I = (RI )
Recall that a nite automaton A over alphabet R is a tuple hR; Q; q0; ; F i, where Q is a nite set of states, q0 2 Q is the initial state, Q R Q is the transition relation, and F Q is the set of accepting states. A run of A on a word R1 : : : Rk over alphabet R is a nite sequence of states q0; q1; : : : ; qk such that (qi 1; Ri; qi) holds for every 1 i k. It is an accepting run if qk 2 F . We say that A accepts a word w if there exists an accepting run of A on w. The set of all words accepted by A is denoted by L(A).
rules, where A 2 C and r 2 R+:
C ::= > j ? j A j :C j C u C j C t C j 8R:C j 9R:C R ::= " j r j R j R R j R t R j R j C?
form C v D. A TBox is a nite set of TBox axioms. An ABox is a nite set of assertions of the form C(a) or r(a; b). A knowledge base in CPDLreg is a tuple hR; T ; Ai consisting of a regular RBox R, a TBox T and an ABox A.
An interpretation is a pair I = h I ; I i, where I is a non-empty set called the domain of I and I is a mapping called the interpretation function of I that associates each individual name a 2 I with an element aI 2 I , each concept name A 2 C with a set AI I , and each role name r 2 R+ with a binary relation rI I I . The interpretation function I is extended to complex concepts and complex roles as shown in Figure 1.
I j= ' is de ned as follows, where at the right hand side of \if" stands for the composition of binary relations:
I j= S1 I j= " v R I j= C v D I j= C(a) I j= r(a; b)
Sk v R if if if if if
SI
1 CI "I v RI
DI
SI k
RI aI 2 CI haI ; bI i 2 rI : If I j= ' then we say that I validates '.
validates all the axioms/assertions of that \box". It is a model of a knowledge base KB = hR; T ; Ai, denoted by I j= KB , if it is a model of R, T and A.
we write KB j= ' to mean that every model of KB validates '. If KB j= C(a) then we say that a is an instance of C w.r.t. KB .
occurring in '. The size of an ABox is the sum of the lengths of its assertions.
3
A Horn-CPDLreg TBox axiom is an expression of the form Cl v Cr, where l stands for \left", r stands for \right", Cl and Cr are concepts de ned by the following BNF grammar: (4) (5) (6) (7) Rl8 ::= r j R j Rl8 Rl9 ::= r j R j Rl9 { each Ci is of the form A, 9Rl9:A, 8Rl8:A, 89r:A or 89r:A, { D is of the form ?, A, 9r:A, 9r:A or 8Rl9:A, { Rl9 and Rl8 are now restricted by the following BNF grammar: Rl9 ::= r j r j Rl9 Rl8 ::= r j r j Rl8
Rl9 j Rl9 t Rl9 j Rl9 j A?
Rl8 j Rl8 t Rl8 j Rl8 j (:A)?
r(a; b), where Cr is a concept of the form speci ed by (4).
2 The clauses > v 9r:> and > v 9r:> can be replaced by > v 9r:A> or > v 9r:A>, respectively, where A> is a fresh concept name. We include them just for convenience. ?I = ; >I = I (:C)I = I n CI (C u D)I = CI \ DI (C t D)I = CI [ DI "I9 = fhx; xi j x 2 RI9 = (RI9 ) 1 (R
S)I9 = RI9 SI9 (R t S)I9 = RI9 [ SI9 (R )I9 = (RI9 ) (R
S)I8 = RI8 SI8 (R t S)I8 = RI8 [ SI8 (R )I8 = (RI8 ) (C?)I8 = (C?)I9 clausal Horn-CPDLreg TBox and A is a reduced ABox, we call such a knowledge base a clausal Horn-CPDLreg knowledge base.
the form C(a), where a 2 I and C is a concept of the family Cl speci ed by (1).
The Constructive Semantics of Horn-CPDLreg
notion for CPDLreg to deal with inverse roles, using a slightly di erent notation that is closer to the traditional notation of DLs.
De nition 4.1. A pseudo-interpretation is a pair I = h I ; I i, where I is a non-empty set called the domain of I and I is a mapping called the interpretation function of I that associates each individual name a 2 I with an element aI 2 I , each concept name A 2 C with a set AI I , and each role name r 2 R+ with a pair hrI9 ; rI8 i of binary relations such that: { rI9 rI8 { for every x 2
I
I ,
I , if Y = fy j hx; yi 2 rI9 g =6 ; then fy j hx; yi 2 rI8 g = Y .
SI9 k
RI9 and SI8 1 SI8 k
RI8 I jw S1 I jw " v R I jw C v D I jw C(a) I jw r(a; b) Sk v R if SI9 1 if "I9 v RI9 if CI DI if aI 2 CI if haI ; bI i 2 rI9 :
pseudo-model of an RBox R, a TBox T or an ABox A if it validates all the axioms/assertions of that \box". It is a pseudo-model of a knowledge base KB = hR; T ; Ai, denoted by I jw KB , if it is a pseudo-model of R, T and A. A knowledge base is satis able w.r.t. the constructive semantics if it has a pseudo-model. We de ne that hR; T ; Ai jw C(a) if, for every pseudo-model I of hR; T ; Ai, it holds that I jw C(a). C
rI9 = rI8 = rI for all r 2 R+. Thus, given an interpretation I, I j= KB i I jw KB , and I j= C(a) i I jw C(a). Conversely, a pseudo-interpretation I satisfying rI9 = rI8 = rI for all r 2 R+ can be treated as an interpretation. In particular, if I j= (> v 9R:>) for all R 2 R, then I can be treated as an interpretation.
Proposition 4.4. Let KB = hR; T ; Ai be a Horn-CPDLreg knowledge base. 1. If C(a) is a Horn-CPDLreg query then, for the Horn-CPDLreg knowledge base KB 0 = hR, T [ fC v Ag, A [ f:A(a)gi, where A is a fresh concept name, we have that: (a) KB jw C(a) i KB 0 does not have any pseudo-model, (b) KB j= C(a) i KB 0 does not have any model. 2. KB can be converted in polynomial time in the sizes of T and A to a Horn-CPDLreg knowledge base KB 0 = hR; T 0; A0i with A0 being a reduced ABox such that KB has a pseudo-model (resp. model) i KB 0 has a pseudomodel (resp. model). 3. KB can be converted in polynomial time in the size of T to a Horn-CPDLreg knowledge base KB 0 = hR; T 0; Ai with T 0 being a clausal Horn-CPDLreg TBox such that: { KB has a pseudo-model (resp. model) i KB 0 has a pseudo-model (resp.
model), { if T does not use the constructor 8R:C at the LHS of v then T 0 does neither.
Corollary 4.5. Every Horn-CPDLreg knowledge base KB can be converted in polynomial time in the sizes of T and A to a clausal Horn-CPDLreg knowledge base KB 0 = hR; T 0; A0i such that KB has a pseudo-model (resp. model) i KB 0 has a pseudo-model (resp. model).
Theorem 4.6. Let KB be a clausal Horn-CPDLreg knowledge base and C(a) be a Horn-CPDLreg query. Then: 1. If KB jw C(a) then KB j= C(a). 2. If f> v 9R:> j R 2 Rg T then: (a) if KB has a pseudo-model then it also has a model, (b) KB jw C(a) i KB j= C(a). 3. If KB is speci ed without using the constructor 8Rl8:Cl in the grammar rule (1) and has a pseudo-model then it also has a model. 4. If KB and C are speci ed without using the constructor 8Rl8:Cl in the grammar rule (1), then KB jw C(a) i KB j= C(a). 5
Checking Constructive Satis ability in Horn-CPDLreg
knowledge base KB = hR; T ; Ai together with the RIA-automaton-speci cation
5.1
Automaton-Modal Operators
struction the inverse operation is applied only to role names and the test operator
as a regular expression over the alphabet = R [ fA?; (:A)? j A 2 Cg (where corresponds to ; and t corresponds to [). The regular language characterized by such a role R is denoted by L(R). A word R1R2 : : : Rk over is also treated as the role R1 R2 Rk.
language L(R). For each role R in ITNFsuch that R 2= R, let AR be a nite automaton recognizing the language L(R0), where R0 is obtained from R by simultaneously substituting each S 2 R by a regular expression representing L(AS).
of the automata (AS)S2R. Roughly speaking, AR can be obtained from AR by simultaneously substituting each transition hq1; S; q2i by the automaton AS.
ton A over alphabet , we de ne AI (resp. AI8 , AI9 ) to be fhx; yi 2 I I j there exist a word R1 : : : Rk accepted by A and elements x0 = x, x1, . . . , xk = y of I such that hxi 1; xii 2 RiI (resp. hxi 1; xii 2 RiI8 , hxi 1; xii 2 RiI9 ) for all 1 i kg.
A is a nite automaton over alphabet and C is a concept. Such
constructors (called formulas with automaton-modal operators) were used earlier, among
others, in [
I j 8y hx; yi 2 AI implies y 2 CI ;
I j 9y hx; yi 2 AI and y 2 CI ; { given a pseudo-interpretation I,
([A]C)I = ([A]9 C)I = (hAiC)I = x 2 x 2 x 2
I j 9y hx; yi 2 AI9 and y 2 CI : ; ;
A = h ; QA; qA; A; FAi:
tomaton obtained from A by replacing the initial state by q.
Lemma 5.1. Let I be a pseudo-model of a regular RBox R, A the RIAautomaton-speci cation of R, and C a concept. Then: { (8R:C)I = ([AR]C)I and (9R:C)I = (hARiC)I , { CI ([AR]9 hARiC)I and CI ([AR]9 9R:C)I .
5.2
Our Algorithm
assumption. That is, C v D is logically equivalent to :C t D, and it is a global assumption for an interpretation I if (:C t D)I = I .
Let X be a set of concepts. The saturation of X (w.r.t. A and T ), denoted by Satr(X), is de ned to be the least extension of X such that: 1. for every R 2 R, [AR]9 9R:> 2 Satr(X), 2. if 8R:C 2 Satr(X) then [AR]C 2 Satr(X), 3. if [A]C 2 Satr(X), hqA; B?; qi 2 A and B 2 Satr(X) then [Aq]C 2 Satr(X), 4. if [A]9 C 2 Satr(X), hqA; B?; qi 2 A and B 2 Satr(X) then [Aq]9 C 2 Satr(X), 5. if ([A]C 2 Satr(X) or [A]9 C 2 Satr(X)) and qA 2 FA then C 2 Satr(X),
Trans(X; R) = f[Aq]C j [A]C 2 X and hqA; R; qi 2 Ag Trans9 (X; R) = Trans(X; R) [ f[Aq]9 C j [A]9 C 2 X and hqA; R; qi 2 Ag: Our algorithm for checking whether KB = hR; T ; Ai has a pseudo-model uses the data structure G = h 0; ; Label ; Next ; LeastSucc; Statusi, which is called a Horn-CPDLreg graph, where: { { 0 : the set of all individual names occurring in A, : a set of objects including 0, { Label : a function mapping each x 2 to a set of concepts, { Next : f9R:>; 9R:A j R 2 R; A 2 Cg ! is a partial mapping, { LeastSucc : R ! is a partial mapping, { Status 2 funknown; unsat ; sat g.
De ne Edges = fhx; R; yi j R(x; y) 2 A or Next (x; 9R:C) = y for some C or LeastSucc(x; R) = yg. A tuple hx; R; yi 2 Edges represents an edge hx; yi with label R of the graph. If R(x; y) 2 A or Next (x; 9R:C) = y then we call hx; R; yi a rm edge, else if LeastSucc(x; R) = y then we call hx; R; yi a pseudo edge. The notions of predecessor and successor are de ned as usual. We say that x 2 is reachable from 0 if there exist x0; : : : ; xk 2 and elements R1; : : : ; Rk of R such that k 0, x0 2 0, xk = x and hxi 1; Ri; xii 2 Edges for all 1 i k.
For x 2 , Label (x) is called the label of x. A fact Next (x; 9R:C) = y means that 9R:C 2 Label (x), C 2 Label (y), and 9R:C is \realized" at x by going to y.
of x", and LeastSucc(x; R) denotes the \logically smallest R-successor of x". A fact Status = unsat means the knowledge base does not have any pseudo-model. A fact Status = unsat means the knowledge base has a pseudo-model. De nition 5.2. Let G; x 6j=c [A]B stand for \it is not certain that G satis es [A]B at x", where x 2 , A is a nite automaton over and B 2 C. We de ne 6j=c to be the smallest relation such that G; x 6j=c [A]B holds if one of the following holds (for some B0 or R when it is related): { qA 2 FA and B 2= Label (x); { hqA; (:B0)?; qi 2 A, B0 2= Label (x) and G; x 6j=c [Aq]B; { hqA; R; qi 2 A, 9R:> 2= Label (x) and LeastSucc(x; R) is not de ned; { hqA; R; qi 2 A, 9R:> 2= Label (x), LeastSucc(x; R) = y and G; y 6j=c [Aq]B; { hqA; R; qi 2 A, 9R:> 2 Label (x) and Next (x; 9R:>) is not de ned; { hqA; R; qi 2 A, Next (x; 9R:>) = y and G; y 6j=c [Aq]B.
We de ne that G; x 6j=c 8R:A if G; x 6j=c [AR]A.
pseudo-model extends A with disjoint trees rooted at the named individuals occurring in A. The trees may be in nite. However, we represent such a semiforest as a graph with global caching: if two nodes that are not named individuals occur in a tree or in di erent trees and have the same label, then they should be merged.
Theorem 5.3. Algorithm 1 runs in polynomial time in the size of the ABox A and correctly checks whether the clausal Horn-CPDLreg knowledge base KB has a pseudo-model.
Corollary 5.4. The Horn-CPDLreg rule language has PTime data complexity (when used with the constructive semantics).
C Function Find(X) z := Find(Label (z) [ Satr(X)); foreach y, R, C such that Next (y; 9R:C) = z do Next (y; 9R:C) := z ; foreach y and R such that LeastSucc(y; R) = z do LeastSucc(y; R) := z ; Function CheckPremise(x; C) 1 if C = > then return true 2 else let C = C1 u : : : u Ck; 3 foreach 1 i k do 4 if Ci = A and A 2= Label (x) then return false 5 else if Ci = 89R:A and (9R:> 2= Label (x) or Next (x; 9R:>) is not de ned or A 2= Label (Next (x; 9R:>))) then 6 return false 7 else if Ci = 9R:A and hARiA 2= Label (x) then return false 8 else if Ci = 8R:A and G; x 6j=c 8R:A then return false 9 return true
Input: a clausal Horn-CPDLreg knowledge base KB = hR; T ; Ai and the RIA-automaton-speci cation A of R.
Output: true if KB has a pseudo-model, or false otherwise.
Global data: a Horn-CPDLreg graph G and a TBox T 0. 1 let 0 be the set of all individuals occurring in A; 2 if 0 = ; then 0 := f g; 3 := 0, T 0 := Satr(T ), set Next and LeastSucc to the empty mappings; 4 foreach a 2 0 do 5 Label (a) := Satr(fA j A(a) 2 Ag) [ T 0 6 while some rule in Table 1 can make changes do 7 choose such a rule and execute it; // any strategy can be used 8 if Status = unsat then return false 9 return true (81) if r(a; b) 2 A then
ExtendLabel(b; Trans9 (Label (a); r)), ExtendLabel(a; Trans9 (Label (b); r)); (82) if x is reachable from 0 and Next (x; 9R:C) = y then
Next (x; 9R:C) := Find(Label (y) [ Satr(Trans9 (Label (x); R))); (83) if x is reachable from 0 and Next (x; 9R:C) = y then
ExtendLabel(x; Trans9 (Label (y); R)); (84) if x is reachable from 0 and LeastSucc(x; R) = y then
LeastSucc(x; R) := Find(Label (y) [ Satr(Trans(Label (x); R))); (85) if x is reachable from 0 and LeastSucc(x; R) = y then
ExtendLabel(x; Trans(Label (y); R)); if x is reachable from 0, 9R:C 2 Label (x), R 2 R and Next (x; 9R:C) is not de ned then
Next (x; 9R:C) := Find(Satr(fCg [ Trans9 (Label (x); R)) [ T 0); (LS) if x is reachable from 0, R 2 R and LeastSucc(x; R) is not de ned then
LeastSucc(x; R) := Find(Satr(Trans(Label (x); R)) [ T 0); if x is reachable from 0, (C v D) 2 Label (x) and CheckPremise(x; C) then
ExtendLabel(x; fDg); if ? 2 Label (x) or there exists fA; :Ag
Label (x) then Status := unsat ;
knowledge base in Horn-CPDLreg has a pseudo-model.
ied in our (joint) works [
the concept constructors 89R:C (for R 2 R) and 8R:C (for any role R) to appear at the LHS of TBox axioms.
In comparison with Horn-DL [29, 28], apart from the concept constructor 89R:C (for R 2 R), Horn-CPDLreg also allows the concept constructor 8R:C (for any role R) to appear at the LHS of TBox axioms. However, Horn-CPDLreg is not more general than Horn-DL because the latter additionally allows nominals, quanti ed number restrictions, the 9r:Self constructor, the universal role as well as assertions of the form disjoint(s; s0), irre exive(s), :s(a; b), a 6=: b. As future work, we will extend Horn-CPDLreg with these features to obtain a rule language Horn-DL2 that is more general than Horn-DL, and hence also more general than Horn-SHIQ and Horn-SROIQ.
oping richer and richer tractable rule languages in modal and description logics.
16. D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, 2000. 17. U. Hustadt, B. Motik, and U. Sattler. Reasoning in description logics by a reduction to disjunctive Datalog. J. Autom. Reasoning, 39(3):351{384, 2007. 18. A. Krisnadhi and C. Lutz. Data complexity in the EL family of description logics.
In Proceedings of LPAR'2007, volume 4790 of LNCS, pages 333{347. Springer, 2007. 19. M. Krotzsch, S. Rudolph, and P. Hitzler. Complexity boundaries for Horn description logics. In Proceedings of AAAI'2007, pages 452{457. AAAI Press, 2007. 20. M. Krotzsch, S. Rudolph, and P. Hitzler. Conjunctive queries for a tractable fragment of OWL 1.1. In Proceedings of ISWC'2007 + ASWC'2007, LNCS 4825, pages 310{323. Springer, 2007. 21. L.A. Nguyen. Constructing the least models for positive modal logic programs.
Fundamenta Informaticae, 42(1):29{60, 2000. 22. L.A. Nguyen. A bottom-up method for the deterministic Horn fragment of the description logic ALC. In Proceedings of JELIA'2006, volume 4160 of LNAI, pages 346{358. Springer-Verlag, 2006. 23. L.A. Nguyen. On the deterministic Horn fragment of test-free PDL. In I. Hodkinson and Y. Venema, editors, Advances in Modal Logic - Volume 6, pages 373{392.
King's College Publications, 2006. 24. L.A. Nguyen. Constructing nite least Kripke models for positive logic programs in serial regular grammar logics. Logic Journal of the IGPL, 16(2):175{193, 2008. 25. L.A. Nguyen. Horn knowledge bases in regular description logics with PTime data complexity. Fundamenta Informaticae, 104(4):349{384, 2010. 26. L.A. Nguyen. Cut-free ExpTime tableaux for Converse-PDL extended with regular inclusion axioms. In Proceedings of KES-AMSTA'2013, volume 252 of Frontiers in Arti cial Intelligence and Applications, pages 235{244. IOS Press, 2013. 27. L.A. Nguyen. A long version of the current paper. Available at http://www.mimuw.
edu.pl/~nguyen/HornCPDLreg-long.pdf, June 2014. 28. L.A. Nguyen, T.-B.-L. Nguyen, and A. Szalas. A long version of the paper [29].
Available at http://www.mimuw.edu.pl/~nguyen/horn_dl_long.pdf. 29. L.A. Nguyen, T.-B.-L. Nguyen, and A. Szalas. Horn-DL: An expressive Horn description logic with PTime data complexity. In Proceedings of RR'2013, volume 7994 of LNCS, pages 259{264. Springer, 2013. 30. L.A. Nguyen, T.-B.-L. Nguyen, and A. Szalas. On Horn knowledge bases in regular description logic with inverse. In Proceedings of KSE'2013, volume 244 of Advances in Intelligent Systems and Computing, pages 37{49. Springer, 2013. 31. L.A. Nguyen and A. Szalas. ExpTime tableau decision procedures for regular grammar logics with converse. Studia Logica, 98(3):387{428, 2011. 32. L.A. Nguyen and A. Szalas. On the Horn fragments of serial regular grammar logics with converse. In Proceedings of KES-AMSTA'2013, volume 252 of Frontiers in Arti cial Intelligence and Applications, pages 225{234. IOS Press, 2013. 33. M. Ortiz, S. Rudolph, and M. Simkus. Query answering in the Horn fragments of the description logics SHOIQ and SROIQ. In Proceedings of IJCAI 2011, pages 1039{1044, 2011. 34. R. Rosati. On conjunctive query answering in EL. In Proceedings of DL'2007, pages 451{458.