Absorption-Based Query Entailment Checking for Expressive Description Logics

Abstract

Conjunctive query answering is an important reasoning task for logicbased knowledge representation formalisms, such as Description Logics, to query for instance data that is related in certain ways. Although there exist many knowledge bases that use language features of more expressive Description Logics, there are hardly any systems that support full conjunctive query answering for these logics. In fact, existing systems usually impose restrictions on the queries or only compute incomplete results. In this paper, we present a new approach for conjunctive query entailment checking that can directly be integrated into existing reasoning systems for expressive Description Logics and serves as basis for conjunctive query answering. The approach reminds of absorption, a well-known preprocessing step that rewrites axioms such that they can be handled more e ciently. In this sense, we rewrite the query such that entailment can dynamically be checked in the dominantly used tableau calculi with minor extensions. Our implementation in the reasoning system Konclude shows encouraging results.

Introduction

Although conjunctive query answering has intensively been studied for many expressive Description Logics (DL), most of the state-of-the-art reasoning systems for these DLs do not support conjunctive queries or only with limitations. In fact, conjunctive query answering is typically reduced to many query entailment checking problems for which decidability is still open in SROIQ. Furthermore, the used techniques for showing decidability and worst-case complexity of sub-languages (e.g., [ 3,13,16 ]) are often not directly suitable for practical implementations. For the DLs SH IQ and SH OQ approaches have been developed that reduce conjunctive query answering to instance checking (e.g, [ 4,6,10 ]), which is not goal-directed, often requires many unnecessary entailment checks, and may require language features (e.g., role conjunctions) which are not available in OWL 2 and, hence, usually not supported by reasoning systems. Even for queries with only answer variables, existing approaches (e.g., [ 8,12,17 ]) are often suboptimal since they are based on the above mentioned reduction to many instance checks. Recently, query answering has been improved by lower and upper bound optimisations that utilise model abstractions built by a reasoner [ 5 ] or delegate work to specialised procedures [ 14,22 ]. However, their e ectiveness is ontology dependent and, hence, optimised and deeply integrated query entailment checking and answering techniques for expressive DLs are still needed for further improvements.

In this paper, we present an approach that encodes the query such that entailment can e ciently be detected in the model construction process with minor extensions to the dominantly used tableau algorithm. The encoding serves to identify individuals involved in satisfying the query and guides the search for a model where the query is not entailed. We refer to this technique as absorption-based query entailment checking since it reminds of the absorption technique for nominal schemas [ 19 ]. The approach is correct and terminates for several expressive DLs for which decidability of conjunctive query entailment is well-known (e.g., SH IQ, SH OQ). For the challenging combination of nominals, inverse roles, and number restrictions, termination is only guaranteed if a bounded number of new nominals is generated. The technique seems well-suited for practical implementations since (i) it only requires minor extensions to tableau algorithms, (ii) can easily be combined with other well-known (query answering) optimisation techniques, and (iii) real-world ontologies hardly require the generation of (many) new nominals. We implemented the proposed technique in the reasoning system Konclude [ 20 ] with encouraging results. The accompanying technical report [ 18 ] sketches extensions to query answering and contains more details as well as evaluation results. 2

Preliminaries

We assume readers to be familiar with DLs and conjunctive queries (see, e.g., [ 1 ]). Since we focus on query entailment checking, we only consider Boolean queries (i.e., all variables are existential variables). A query Q is a set of query terms fq1; : : : ; qkg with qi either a concept term of the form C(z) or a role term of the form r(z1; z2). We consider r(x; y) 2 Q as equivalent to r (y; x) 2 Q and use vars(Q) to refer to the variables in Q. W.l.o.g. we do not use individual names in query terms and we assume that all variables are connected via role terms.

Reasoning algorithms for SROIQ are dominantly based on (variants of) tableau algorithms, which, roughly speaking, check the consistency of a knowledge base K by trying to construct an abstraction of a model for K , a so-called “completion graph”. A completion graph G is a tuple (V; E; L; ,˙ ), where each node v 2 V (edge hv; wi 2 E) represents one or more (pairs of) individuals. Each node v (edge hv; wi) is labelled with a set of concepts (roles), L(v) (L(hv; wi)), which the individuals represented by v (hv; wi) are instances of. The relation ,˙ records inequalities between nodes. We call C 2 L(v) (r 2 L(hv; wi)) a concept (role) fact, which we write as C(v) (r(v; w)). A node v is a nominal node if fag 2 L(v) for some individual a and a blockable node otherwise.

A completion graph is initialised with one node for each individual in the input knowledge base. Concepts and roles are added to the node and edge labels as specified by concept and role assertions. Complex concepts are then decomposed using expansion rules, where each rule application can add new concepts to node labels and/or new nodes and edges, thereby explicating the structure of a model. The rules are applied until either the graph is fully expanded (no more rules are applicable), in which case the graph can be used to construct a model that is a witness to the consistency of K , or an obvious contradiction (called a clash) is discovered (e.g., a node v with C; :C 2 L(v)), proving that the completion graph does not correspond to a model. K is consistent if the rules (some of which are non-deterministic) can be applied such that they build a fully w t s x z r s expanded, clash-free completion graph. Cycle detection techniques such as pairwise blocking [ 9 ] prevent the infinite generation of new nodes.

For handling axioms of the form A v C, where A is atomic, one typically uses special lazy unfolding rules in the tableau algorithm, which add C to a node label if it contains the concept A. Axioms of the form C v D, where C is not atomic, cannot directly be handled with lazy unfolding rules. Instead, they are internalised to > v :C t D. Given that > is satisfied at each node, the disjunction is then present in all node labels. To avoid the non-determinism introduced by internalisation, one typically uses a preprocessing step called absorption to rewrite axioms into (possibly several) simpler concept inclusion axioms that can be handled by lazy unfolding. Binary absorption [ 11 ] utilises axioms of the form A1 u A2 v C for absorbing more complex axioms. This requires a binary unfolding rule that adds C to node labels if A1 and A2 are present. 3

Absorption-Based Query Entailment Checking

With the exception of role relationships between nominals/individuals, DLs allow only for expressing tree-shaped structures [ 7,21 ]. Even with nominals/individuals, forestshaped models exists [ 16 ]. Hence, we can check query entailment by “folding” the relational structure of (parts of) the query into a tree-shaped form by identifying variables. The resulting queries (query parts), called foldings, can then be expressed as DL concepts (possibly using role conjunctions). Such query concepts can be used to check query entailment: we have that a query (part) is not entailed if a completion graph exists that satisfies none of its foldings.

Example 1. Consider the (cyclic) query Q1 = ft(w; x); r(x; y); s(y; z); s(z; w)g (cf. Figure 1, left-hand side). There are di erent (tree-shaped) foldings of the query, e.g., by identifying x and z or w and y (cf. Figure 1, middle and right-hand side). The foldings can be expressed as 9(t u s ):9(r u s ):> and 9(t u r):9(s u s):>, respectively.

If we add, for each concept, say C, that represents a folding of the query, the axiom C v ? to the knowledge base, then consistency checking reveals query entailment. Note that the tableau algorithm decides for each node whether (sub-)concepts of the foldings are satisfied (due to the internalisation to > v :C t ?) and adds corresponding (sub-)concepts or their negations to the node labels and, hence, the expansion of nodes is not blocked too early w.r.t. deciding query entailment. Unfortunately, state-of-the-art reasoners do not support role conjunctions and there can be many foldings of a query (especially if the query has several nested cycles or uses role terms with complex roles).

Here we propose, as an alternative, to dynamically match and fold the query onto the completion graph. This is achieved by ‘absorbing’ a query into several simple axioms that can e ciently be processed, where intermediate states encode the parts of the query that are already satisfied. The intermediate states are tracked in the form of so-called query state concepts (written S, possibly with sub-/super-scripts), which can be seen as fresh atomic concepts with a set of associated bindings of query variables to nodes in the completion graph. To realise this, we extend the tableau algorithm to create variable bindings (to match a variable to a node in the completion graph), to propagate variable bindings in the process of folding the query onto the completion graph, and to join variable bindings. Creating and propagating variable bindings according to the role terms of a query ultimately allows us to detect when cycles are closed.

For the creation of variable bindings, we borrow the # binders from Hybrid Logics [ 2 ]. Informally, a concept of the form #x:C in the label of a node v instructs the tableau algorithm to create a binding fx 7! vg, which binds x to the node v, and to store the binding for the sub-concept C. For the propagation of bindings, we extend the 8-rule of the tableau algorithm. For example, if 8r:C is in the label of a node v and the variable binding fx 7! vg is associated with it, then the tableau algorithm associates fx 7! vg with C for all r-successors of v. Additionally, propagation can happen within node labels, e.g., if S 2 L(v) with the associated binding fx 7! vg and the knowledge base contains S v C, we add C to L(v) and associate fx 7! vg with it. Finally, for joining bindings, we extend the binary unfolding rule. For example, if S1 and S2 are in the label of a node v and the bindings fx 7! v; y 7! wg and fx 7! v; z 7! wg are associated with them, respectively, then, for an axiom S1 u S2 v C in the knowledge base, we add C to L(v) and associate the joined bindings fx 7! v; y 7! w; z 7! wg with it. With these basic adaptations, we can capture the query in several simple types of axioms: S v #x:S 0 for creating bindings, S v S 0 and S v 8r:S 0 for propagating bindings, and S1 u S2 v S 0 for joining bindings, where S , S 0, S1, S2 are query state concepts and r is an atomic role or its inverse. The resulting axioms can usually be processed quite e ciently. 3.1

Query Absorption

Before presenting a formal algorithm, we demonstrate how the concepts and axioms for a query are obtained by means of an example. We call this process absorbing a query. Example 2 (Example 1 cont.). Consider again Q1 = ft(w; x); r(x; y), s(y; z); s(z; w)g. We first pick a starting variable, say w, and introduce the axiom > v #w:Sw, which triggers, for all nodes, that a binding for w is created. We use the (fresh) query state concept Sw to indicate that w is bound. Since it is convenient to continue with a role term containing w, we choose t(w; x) and propagate the bindings for w to t-successors using the axiom Sw v 8t:Stw (again Stw is fresh and indicates the state that bindings for w have been propagated via t). Nodes to which Stw (with the bindings for w) is propagated are suitable bindings for x. This is captured by the axiom Sw t v #x:S x. Since Stw may be propagated from di erent nodes, we join the propagated bindings for w and the newly created bindings for x using the axiom Stw u S x v Swx, for which the extended tableau algorithm attaches the joined bindings to the fresh concept Swx. We proceed analogously for r(x; y); s(y; z), and s(z; w) (see Figure 2 for all created axioms). Nodes to which the concept Swsxyz is propagated, potentially close the cycle in the query. The axiom Swsxyz u Sw v Swxyzw checks whether a join is possible. In case it is, the query is satisfied > v #w:Sw Stw u Sx v Swx Srwx u Sy v Swxy Swsxy u Sz v Swxyz

Sw v 8t:Stw

Swx v 8r:Srwx

Swxy v 8s:Swsxy

Swxyz v 8s:Swsxyz Stw v #x:Sx

Swx r v #y:Sy

Swsxy v #z:Sz Swsxyz u Sw v Swxyzw

Swxyzw v ?

and a clash is triggered by the axiom Swxyzw v ?. In this case, backtracking is potentially triggered to try other non-deterministic choices which might yield a complete and clashfree completion graph that is a counter example for the query entailment.

The next example demonstrates how concept terms in the query are handled. Example 3 (Example 2 continued). Consider Q2 = Q1 [ fB(x)g. As in Example 2, we pick w as starting node and then process t(w; x). This yields (again) the first four axioms shown in Figure 2. Assume that we now process B(x). At the state Swx, the tableau algorithm can either satisfy :B (which indicates that the query is not satisfied with these bindings for w and x) or we have to assume a query state where also B(x) is satisfied. This is achieved by adding the axiom Swx v :B t F Bx, where F Bx is a fresh concept. Note that we want to keep the number of modified tableau rules minimal. Hence, when applied to :BtF Bx, the t-rule does not propagate variable bindings. In case, the disjunct F Bx is chosen, we join its empty set of variable bindings with those for Swx using the axiom Swx u F Bx v SwBx, which is handled by the extended binary unfolding rule. For the next role term r(x; y), we then add SwBx v 8r:Srwx and continue as in Example 2.

Algorithm 1 formalizes the query absorption process and extends the given knowledge base K via side e ects. The functions absorbCT (Algorithm 2) and absorbRT (Algorithm 3) handle concept and role terms, respectively. The functions use a mapping VLS from variables to the last query state concepts, i.e., each variable in the query is mapped to the last introduced query state concept for that variable such that we can later continue or incorporate the propagation for that variable. In the example, we always chose an adjacent next query term that contains the current variable z. In case a non-adjacent term is chosen, Lines 6–11 ensure the connection to the current variable (which exists as we consider connected queries, see Section 2). In our example, if we were to choose s(y; z) as first query term in Line 5 (with w as starting variable), Lines 6– 11 ensure that we process, for example, t(w; x) and r(x; y) before we process s(y; z) in Line 17. Clearly, the presented algorithm can further be optimised, e.g., by not creating binder concepts for variables that are not required in joins, but the presented algorithm is already quite convenient to show the principle of the approach. 3.2 As outlined in the previous sections, minor extensions and adaptations of the tableau algorithm are required for creating, propagating, and joining bindings as well as for Algorithm 1 absorbQ(Q; K ) Input: A query Q and a knowledge base K

that is extended via side e ects 1: z choose one variable from vars(Q) 2: Sz fresh query state concept 3: K K [ f> v #z:Szg 4: VLS (z) Sz 5: for each q 2 Q do 6: if q = C(x) or q = r(x; y), z , x then 7: choose q1; q2; : : : ; qn 2 Q with q1 = r1(z; y1); q2 = r2(y1; y2); : : : ; qn = rn(yn 1; x) 8: for 1 i n do 9: absorbRT(qi; VLS ; K ) 10: end for 11: end if 12: if q = C(x) then 13: absorbCT(C(x); VLS ; K ) 14: z x 15: end if 16: if q = r(x; y) then 17: absorbRT(r(x; y); VLS ; K ) 18: z y 19: end if 20: end for 21: Sz1:::zmz

VLS (z)

K [ fSz1:::zmz v ?g 22: K Algorithm 2 absorbCT(C(x); VLS ; K ) 1: Sx1:::x:::xn VLS (x) 2: FCx fresh atomic concept 3: SCx1:::x:::xn fresh query state concept 5: K KK [[SffSSx1xx::11:x::::::::xx:x::::n::xxnn uv F:CCxvtSFCxC1x:g::x:::xn g 4: K 6: VLS (x) C Algorithm 3 absorbRT(r(x; y); VLS ; K ) 1: Sx1:::x:::xn VLS (x) 2: Srx1:::x:::xn fresh query state concept 3: K K [ fSx1:::x:::xn v 8r:Srx1:::x:::xn g 4: if VLS (y) is undefined then 5: Sy fresh query state concept 6: K K [ fSrx1:::x:::xn v #y:Syg 7: VLS (y) Sy 8: end if 9: Sy1:::y:::ym VLS (y) 10: Sz1:::zk fresh query state concept with

z1 : : : zk = x1 : : : x : : : xny1 : : : y : : : ym 11: K

K [ fSrx1:::x:::xn u Sy1:::y:::ym v Sz1:::zk g 12: VLS (y) Sz1:::zk ensuring a correct blocking. First, we discuss the required rule extensions and define the notion of variable mappings:

Definition 1 (Variable Mapping). A variable mapping is a (partial) function from

variable names to nodes and we refer to the set of elements on which is defined as the domain, written dom( ), of . We say that two variable mappings 1 and 2 are compatible if 1(x) = 2(x) for all x 2 dom( 1) \ dom( 2).

For an extended completion graph G = (V; E; L; ,˙; M) and v 2 V, we denote with M(C; v) the sets of variable mappings that are associated with a concept C in L(v).

The #-rule creates and associates variable mappings with concept facts in the completion graph, which we then propagate to other concept facts w.r.t. the axioms from the query absorption by using the extensions of expansion rules depicted in Table 1. In particular, the application of the 8-rule to a concept fact 8r:C(v) now also propagates mappings that are associated with 8r:C(v) to the concept C in the labels of the r-neighbours. If complex roles have to be handled, one can, for example, use an unfolding of the universal restriction according to the automata for role inclusion axioms [ 9 ].

The remaining rules of Table 1 handle the (lazy) unfolding of the new query state concepts in node labels. Please note that the standard unfolding rules for simple atomic concepts are still necessary, i.e., C has to be added to a node label for axioms of the form A v C and A1 u A2 v C if A or A1 and A2 are present. In contrast, the new unfolding rules are only applied if at least one concept on the left-hand side is a query state concept and they additionally also propagate associated variable mappings to C. More precisely, if the query state concept Sx1:::xn is in the label of a node v and we have the variable mappings M associated with this fact, then we add C for an axiom of the form Sx1:::xn v C 2 K and we associate M also with C(v) (cf. v1-rule). For an axiom of the form Sx1:::xn u A v C, we only add C and propagate the mappings to C if also the atomic concept A is in the label (cf. v2-rule). Finally, the v3-rule handles binary inclusion axioms, where both concepts on the left-hand side are query state concepts, by propagating the join of the associated variable mappings to the implied concept. Definition 2 (Variable Mapping Join). A variable mapping 1 [ 2 is defined by setting ( 1 [ 2)(x) = 1(x) if x 2 dom( 1), and ( 1 [ 2)(x) = 2(x) otherwise. The join M1 1 M2 between the sets of variable mappings M1 and M2 is defined as follows:

M1 1 M2 = f 1 [ 2 j 1 2 M1; 2 2 M2 and 1 is compatible with 2g: By applying the rules of Table 1 (in addition to the standard tableau rules) for a knowledge base that is extended by the axioms from the query absorption, we get associations of variable mappings with query state concepts such that they indicate which parts of a query (and how these parts) are satisfied in the completion graph. Example 4 (Example 2 cont.). Assume we extend K1 = fA(a); A v 9t:B; B v 9r:A; t v s ; r v s g with the axioms from absorbing Q1 in Figure 2 and test the consistency with a tableau algorithm extended by the rules of Table 1. We observe that the constructed completion graph contains a clash and, consequently, Q1 is entailed (cf. Figure 3). More precisely, we create a node for the individual a and add A to its node label (due to A(a)). Now, we alternately create t- and r-successors (due to A v 9t:B and B v 9r:A), where the t-successors are labelled with B and the r-successors with A. Due to t v s and r v s , we add s to each edge label. It is obvious to see that the folding 9(t u s ):9(r u s ):> of Q1 (cf. Example 1 and Figure 1) is satisfied for each node that instantiates A. t; s r; s va v1 v2 : : : v3

8 L(va) = <> > :

>; A; 9t:B; #w:Sw; S wffw7!vagg; 8t:S twffw7!vagg;

S wsxyzffw7!va;x7!v1;y7!v2;z7!v1gg; S wxyzwffw7!va;x7!v1;y7!v2;z7!v1gg; ? 8> >; B; 9r:A; #w:Sw; S wffw7!v1gg; 8t:S twffw7!v1gg; S twffw7!vagg; #x:Sx; S xffx7!v1gg; 9 > >>> L(v1) = <>> S wxffw7!va;x7!v1gg; 8r:S rwxffw7!va;x7!v1gg; S wsxyffw7!va;x7!v1;y7!v2gg; #z:Sz; S zffz7!v1gg;=> >>>>: S wxyzffw7!va;x7!v1;y7!v2;z7!v1gg; 8s:S wsxyzffw7!va;x7!v1;y7!v2;z7!v1gg >>>>; 8 L(v2) = <> > : L(v3) = n >; A; 9t:B; #w:Sw; S wffw7!v2gg; 8t:S twffw7!v2gg; S rwxffw7!va;x7!v1gg; #y:Sy;

S yffy7!v2gg; S wxyffw7!va;x7!v1;y7!v2gg; 8s:S wsxyffw7!va;x7!v1;y7!v2gg; : : : >; B; 9r:A; #w:Sw; S wffw7!v3gg; : : : 9 > = > ; 9 > = > ; o Due to > v #w:Sw from the absorption, we add Sw to each node label and associate Sw with a mapping from w to the node. In particular, for va representing the individual a, we associate fw 7! vag with Sw. Note that fw 7! vag 2 M(Sw; va) is shown as S wffw7!vagg in Figure 3, i.e., we list the set of associated mappings as a second super-script highlighted in grey. To satisfy the axiom Sw v 8t:Stw, we unfold Sw to 8t:Stw and we also keep the variable mappings, i.e., we have fw 7! vag 2 M(8t:Stw; va). Now, the application of the 8-rule propagates fw 7! vag to Sw

t 2 L(v1). There, we unfold Stw to the binder concept for x, for which then the #-rule creates a new variable mapping fx 7! v1g that is joined by the v3-rule with fw 7! vag such that we have fw 7! va; x 7! v1g 2 M(Swx; v1). These steps are repeated until we have fw 7! va; x 7! v1; y 7! v2; z 7! v1g 2 M(Swsxyz; va). Since fw 7! vag is compatible with fw 7! va; x 7! v1; y 7! v2; z 7! v1g, the v3-rule adds the latter variable mapping to M(Swxyzw; va). Finally, the v1-rule adds ? to L(va). Since all facts and variable mappings are derived deterministically, no non-deterministic alternatives have to be evaluated and entailment of Q1 is correctly determined.

As one can see from the example, the variable mappings associated with query state concepts directly correspond to foldings of the query. In particular, variables that are mapped to the same node correspond to the folding where the corresponding variables are identified. In addition, if a variable is mapped to a nominal node, then the mapping basically represents the “folding” that is obtained by replacing the variable with the associated nominal/individual (and folding up the remaining terms).

Without further optimisations, we create new bindings for every node and, due to complex roles and/or nominals, variable mappings might be propagated arbitrarily far through a completion graph. At first sight, this seems problematic for blocking. The correspondence with foldings, however, helps us to find a suitable extension of the typically used pairwise blocking technique [ 9 ] defined as follows: Definition 3 (Pairwise Blocking). Let G = (V; E; L; ,˙; M) be a completion graph. We say that a node v with predecessor v0 is directly blocked if there exists an ancestor node w of v with predecessor w0 such that (1) v; v0; w; w0 are all blockable, (2) w; w0 are not blocked, (3) L(v) = L(w) and L(v0) = L(w0), and (4) L(hv0; vi) = L(hw0; wi). A node va v1 t t v2 g n ck t i o l b v3 is indirectly blocked if it has an ancestor node that is directly blocked, and a node is blocked if it is directly or indirectly blocked.

The query state concepts, which track how much of the query is satisfied, are already part of the concept labels. Hence, it remains to check whether the query is analogously satisfied (i.e., same foldings must exist) by, roughly speaking, checking whether the variable mappings have been propagated in the same way between the blocking node, its predecessor and (related) nominal nodes and between the blocked node, its predecessor and (related) nominal nodes. Note that a mapping and the query state concepts with which is associated capture which query parts are already satisfied. Query state concepts that are associated with mappings that are compatible with correspond to states where fewer or additional query parts are satisfied. The following notion captures such related query state concepts for a mapping and a node v of a completion graph: Definition 4. Let G = (V; E; L; ,˙ ; M) be a completion graph. For v 2 V and a mapping , we set states(v; ) = fC 2 L(v) j v 2 M(C; v) is compatible with g. Note that we do not limit states to query state concepts only to enable more absorption optimisations (see [ 18 ] for details). We formally capture (query state) concepts associated with a mapping and their relation to blocking with the notion of analogous propagation blocking and witness mappings: Definition 5 (Analogous Propagation Blocking). Let G = (V; E; L; ,˙; M) be a completion graph and o1; :::; on 2 V all the nominal nodes in G. We say that a node v with predecessor v0 is directly blocked by w with predecessor w0 if v is pairwise blocked by w and, for each mapping 2 M(C; v) [ M(C; v0) [ M(C; o1) [ ::: [ M(C; on); C 2 L(v) [ L(v0) [ L(o1) [ ::: [ L(on), there exists a witness mapping 0 2 M(D; w) [ M(D; w0) [ M(D; o1) [ ::: [ M(D; on); D 2 L(w) [ L(w0) [ L(o1) [ ::: [ L(on) and vice versa such that states(v; ) = states(w; 0), states(v0; ) = states(w0; 0), and states(oi; ) = states(oi; 0) for 1 i n. Example 5 (Example 2 cont.). For testing entailment of Q1 over K2 = fA(a); A v 9t:A; t t v tg, we can capture the transitivity of t by extending the axioms of Figure 2 with Stw v 8t:Stw (cf. [ 9 ]). For the resulting axioms, the tableau algorithm creates a completion graph as depicted in Figure 4, where the query is not entailed. Due to the axiom Av9t:A, the tableau algorithm successively builds t-successors until blocking is established. Note that new variable mappings are created for all nodes and all mappings are propagated to all descendants due to the transitive role t. Hence, we not only have mappings with new bindings for each new successor, but also an increasing number of mappings. Nevertheless, v3 is already directly blocked by v2 using analogous propagation blocking since all pairwise blocking conditions are satisfied (e.g., L(v3) = L(v2), L(v2) = L(v1)) and we have for each variable mapping a witness mapping as shown in Table 2. For example, for the mapping fw 7! v3g, we have states(v3; fw 7! v3g) = fSw; 8t:Stw; Sxg and states(v2; fw 7! v3g) = fSxg due to the compatible mappings fx 7! v3g and fx 7! v2g, respectively (cf. first row of Table 2). A witness for fw 7! v3g is fw 7! v2g since states(v2; fw 7! v2g) = fSw; 8t:Stw; Sxg and states(v1; fw 7! v2g) = fSxg.

To avoid considering all nominal nodes in blocking tests, one could obtain restricted sets of relevant nominal nodes by “remembering” nominal nodes over which variable mappings have been propagated, by tracking the usage of nominals for descendants or by indexing variable mappings propagated over nominal nodes.

4 Implementation and Experiments

The presented query entailment checking approach is implemented in the tableau-based reasoning system Konclude [ 20 ], which supports the DL SROIQ with nominal schemas, i.e., an extension of the nominal constructor by variables for natively representing rulebased knowledge in ontologies. Axioms with nominal schemas are also absorbed in Konclude such that variable bindings are appropriately propagated through the completion graph [ 19 ], which we reuse to some extent for the query entailment checking extension. The implementation and data for the experiments are available online [ 18 ].

At the moment, Konclude may not terminate for SROIQ ontologies if the absorption of the query leads to propagations over new nominal nodes. However, this does not seem problematic in practice. For example, the ORE2015 dataset [ 15 ] contains 1920 ontologies (with trivial ontologies already filtered out), but only 399 use all problematic language features (36 are OIQ, 281 are OIN , and 82 are OIF ). Konclude never applied the new nominal rule in the consistency checks for these 399 ontologies, but we terminated the reasoner (and, hence, the analysis of the new nominal generation) for 4 ontologies after reaching the time limit of 5 minutes. Even if new nominals are generated, it would further be required that the query propagates di erently over new nominal and blockable nodes such that blocking cannot be established.

For evaluating (the limits of) our query entailment checking approach, we identified several interesting ontologies (i.e., ontologies that use most features of SROIQ with at least 100 individuals and for which standard reasoning tasks are di cult but processable by Konclude), such as DMKB, FMA, OBI, UOBM (cf. Table 3), and generated 50 non-trivial queries with several cycles for each ontology. In summary, the entailment for most queries can be decided in under one second (90% require less than 1s, 49% less than 0:1s) by using one core of a Dell PowerEdge R420 server with two Intel Xeon E5-2440 CPUs at 2.4 GHz and 144 GB RAM under a 64bit Ubuntu 16.04.5 LTS. However, there are queries that lead to many propagations (e.g., UOBM) and/or require many blocking checks (e.g., Family) and, consequently, such queries require significantly more time (e.g., 30 queries for the Family ontology reached the time limit of 5 minutes since complex roles lead to many propagations with non-trivial blocking tests). To further improve the performance, one could also use a representative propagation of variable mappings [ 19 ] for entailment checks and/or index more precisely which nodes constitute blocker candidates. Nevertheless, the extension of the presented query entailment checking approach to query answering (with appropriate reduction optimisations) is already able to outperform PAGOdA [ 22 ] on some of the non-trivial real-world queries from the PAGOdA evaluation (see [ 18 ] for details). 5

Conclusions

We presented a novel query entailment checking approach based on the well-known absorption optimisation that improves the reasoning performance for several more expressive Description Logics. The approach can nicely be integrated into state-of-the-art tableau-based systems and our implementation in Konclude shows encouraging results.

References

1. Baader , F. , Calvanese , D. , McGuinness , D. , Nardi , D. , Patel-Schneider , P . (eds.): The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press, second edn. ( 2007 )

2. Blackburn , P. , Seligman , J.: Hybrid languages . Journal of Logic, Language and Information 4 ( 3 ) ( 1995 )

3. Calvanese , D. , Eiter , T. , Ortiz , M. : Answering regular path queries in expressive description logics: An automata-theoretic approach . In: Proc. 22nd AAAI Conf. on Artificial Intelligence (AAAI'07) . pp. 391 - 396 . AAAI Press ( 2007 )

4. Glimm , B. , Horrocks , I. , Sattler , U. : Unions of conjunctive queries in SH OQ . In: Proc. 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR'08) . pp. 252 - 262 . AAAI Press ( 2008 )

5. Glimm , B. , Kazakov , Y. , Kollia , I. , Stamou , G.: Lower and upper bounds for SPARQL queries over OWL ontologies . In: Proc. 29th Conf. on Artificial Intelligence (AAAI'15) . AAAI Press ( 2015 )

6. Glimm , B. , Lutz , C. , Horrocks , I. , Sattler , U. : Conjunctive query answering for the description logic SHIQ . J. of Artificial Intelligence Research 31 , 157 - 204 ( 2008 )

7. Grädel , E.: Why are modal logics so robustly decidable ? In: Paun, G. , Rozenberg , G. , Salomaa , A . (eds.) Current Trends in Theoretical Computer Science, Entering the 21th Century , vol. 2 , pp. 393 - 408 . World Scientific ( 2001 )

8. Haarslev , V. , Möller , R. , Wessel , M. : Querying the semantic web with Racer + nRQL . In: Proc. KI-2004 Int. Workshop on Applications of Description Logics ( 2004 )

9. Horrocks , I. , Kutz , O. , Sattler , U. : The even more irresistible SROIQ . In: Proc. 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR'06) . pp. 57 - 67 . AAAI Press ( 2006 )

10. Horrocks , I. , Tessaris , S. : Querying the semantic web: a formal approach . In: Proc. 1st Int. Semantic Web Conf. (ISWC'02) . pp. 177 - 191 . Springer ( 2002 )

11. Hudek , A.K. , Weddell , G.E. : Binary absorption in tableaux-based reasoning for description logics . In: Proc. 19th Int. Workshop on Description Logics (DL'06) . vol. 189 . CEUR ( 2006 )

12. Kollia , I. , Glimm , B. : Optimizing SPARQL query answering over OWL ontologies . J. of Artificial Intelligence Research 48 , 253 - 303 ( 2013 )

13. Ortiz , M. , Calvanese , D. , Eiter , T. : Data complexity of query answering in expressive description logics via tableaux . J. of Automated Reasoning 41 ( 1 ), 61 - 98 ( 2008 )

14. Pan , J.Z. , Thomas , E. , Zhao , Y. : Completeness guaranteed approximation for OWL-DL query answering . In: Proceedings of the 22nd International Workshop on Description Logics (DL'09) . vol. 477 . CEUR ( 2009 )

15. Parsia , B. , Matentzoglu , N. , Gonçalves , R.S. , Glimm , B. , Steigmiller , A. : The OWL reasoner evaluation (ORE) 2015 competition report . J. of Automated Reasoning 59 ( 4 ), 455 - 482 ( 2017 )

16. Rudolph , S. , Glimm , B. : Nominals, inverses, counting, and conjunctive queries or: Why infinity is your friend! J. of Artificial Intelligence Research 39 , 429 - 481 ( 2010 )

17. Sirin , E. , Parsia , B. , Cuenca Grau , B. , Kalyanpur , A. , Katz , Y. : Pellet: A practical OWL-DL reasoner . J. of Web Semantics 5 ( 2 ), 51 - 53 ( 2007 )

18. Steigmiller , A. , Glimm , B. : Absorption-based query answering for expressive description logics - technical report . Tech. rep. , Ulm University, Ulm, Germany ( 2019 ), available online at https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2019/ StGl2019-ABQA-TR-DL.pdf

19. Steigmiller , A. , Glimm , B. , Liebig , T. : Reasoning with nominal schemas through absorption . J. of Automated Reasoning 53 ( 4 ), 351 - 405 ( 2014 )

20. Steigmiller , A. , Liebig , T. , Glimm , B. : Konclude: system description . J. of Web Semantics 27 ( 1 ) ( 2014 )

21. Vardi , M.Y.: Why is modal logic so robustly decidable? In: Descriptive Complexity and Finite Models: Proceedings of a DIMACS Workshop. DIMACS: Series in Discrete Mathematics and Theoretical Computer Science , vol. 31 , pp. 149 - 184 . Memoirs of the American Mathematical Society ( 1997 )

22. Zhou , Y. , Cuenca Grau , B. , Nenov , Y. , Kaminski , M. , Horrocks , I.: PAGOdA: Pay-as-you-go ontology query answering using a datalog reasoner . J. of Artificial Intelligence Research 54 , 309 - 367 ( 2015 )