The Combined Approach to Query Answering Beyond the OWL 2 Profiles

1 Introduction

Answering conjunctive queries (CQs) over ontology-enriched datasets is a core reasoning task for many applications. CQ answering is computationally expensive: for expressive description logic ontology languages it is at least doubly exponential in combined complexity [Lutz, 2007], and it remains single exponential even when restricted to Horn ontology languages [Ortiz et al., 2011].

In recent years, there has been a growing interest in ontology languages with favourable computational properties, such as EL [Baader et al., 2005], DL-Lite [Calvanese et al., 2007] and the rule language datalog, which provide the foundation for the EL, QL and RL profiles of OWL 2, respectively [Motik et al., 2009]. Standard reasoning tasks (e.g., satisfiability checking) are tractable for all three profiles. CQ answering is NP-complete (in combined complexity) for the QL and RL profiles, and PSPACE-complete for OWL 2 EL [Stefanoni et al., 2014]; PSPACE-hardness of CQ answering in EL is due to role composition axioms and the complexity further drops to NP if these are restricted to express role transitivity and reflexivity [Stefanoni and Motik, 2015]. Furthermore, in all these cases CQ answering is tractable in data complexity. Such complexity bounds are rather benign, and this has spurred the development of practical algorithms.

∗Work supported by the Royal Society, the EPSRC grants Score!, DBOnto and MaSI3 , the NSF award 1017255 "III: Small: TROn: Tractable Reasoning with Ontologies" and "La Caixa" Foundation.

A technique that is receiving increasing attention is the combined approach [Lutz et al., 2009; Kontchakov et al., 2010; 2011; Lutz et al., 2013; Stefanoni et al., 2013], which can be summarised as follows. First, the data is augmented in a query-independent way to build (in polynomial time) a canonical interpretation. Although this interpretation cannot be homomorphically embedded into each model (and might not be a model itself), it can be exploited for CQ answering in two equivalent ways. In the approach by [Kontchakov et al., 2010] the query is first rewritten and then evaluated against the interpretation. Alternatively, in [Stefanoni et al., 2013; Lutz et al., 2013] the query is first evaluated over the interpretation and unsound answers are discarded by means of a filtration process. With the exception of [Gottlob et al., 2014] and [Thomazo and Rudolph, 2014] who focus on decidable classes of existential rules, algorithms based on the combined approach are restricted to (fragments of) the OWL 2 profiles.

Our goal is to push the boundaries of the logics underpinning the OWL 2 profiles while retaining their nice complexity for CQ answering. Furthermore, we aim to devise algorithms that seamlessly extend the combined approach and which can be applied to a wide range of ontologies.

Recently, a class of Horn ontologies has been proposed [Carral et al., 2014a; 2014b] that extends the profiles and cannot be captured by known decidable classes of existential rules, while ensuring tractability of standard reasoning tasks. The idea is to allow the use of all language constructs in the profiles, while establishing polynomially checkable conditions that preclude their harmful interaction. Ontologies satisfying these conditions are referred to as role safety acyclic (RSA). The roles in an RSA ontology are partitioned into safe and unsafe depending on the way they are used, where the latter ones are involved in potentially harmful interactions which could increase complexity; then, an acyclicity condition is imposed on unsafe roles to ensure tractability. A recent evaluation revealed that over 60% of out-of-profile Horn ontologies are RSA [Carral et al., 2014b].

In this paper, we investigate CQ answering over RSA ontologies and show its feasibility in NP. This result has significant implications in practice as it shows that CQ answering over a wide range of out-of-profile ontologies is no harder (in combined complexity) than over a database. Our procedure generalises the combined approach for ELHO [Stefanoni et al., 2013] and DL-LiteR [Lutz et al., 2013] in a seamless way by means of a declarative encoding of CQ answering into fact entailment w.r.t. a logic program (LP) with function symbols and stratified negation. The least Herbrand model of this program can be computed in time polynomial in the ontology size and exponential in query size. We have implemented our encoding using the LP engine DLV [Leone et al., 2006] and tested its feasibility with encouraging results.

The proofs of all our results are delegated to an extended technical report (http://tinyurl.com/pqmxa5u).

2 Preliminaries

Logic Programs We use the standard notions of constants, terms and atoms in first-order logic (FO). A literal is an atom a or its negation not a. A rule r is an expression of the form ϕ(⃗x, ⃗z) → ψ(⃗x) with ϕ(⃗x, ⃗z) a conjunction of literals with variables ⃗x ∪ ⃗z, and ψ(⃗x) a non-empty conjunction of atoms over ⃗x. 1 We denote with vars(r) the set ⃗x∪⃗z. With head(r) we denote the set of atoms in ψ, body+(r) is the set of atoms in ϕ, and body-(r) is the set of atoms which occur negated in r. Rule r is safe iff vars(r) all occur in body+(r). We consider only safe rules. Rule r is definite if body-(r) is empty and it is datalog if it is definite and function-free. A fact is a rule with empty body and head consisting of a single function-free atom.

A program P is a finite set of rules. Let preds(X) denote the predicates in X, with X either a set of atoms or a program. A stratification of program P is a function str : preds(P) → {1, . . . , k}, where k ≤ |preds(P)|, s.t. for every r ∈ P and P ∈ preds(head(r)) it holds that:

• for every Q ∈ preds(body+(r)): str(Q) ≤ str(P)
• for every Q ∈ preds(body-(r)): str(Q) < str(P)

The stratification partition of P induced by str is the sequence (P1, . . . ,Pk), with each Pi consisting of all rules r ∈ P s.t. maxa∈head(r)(str(pred(a))) = i. The programs Pi are the strata of P. A program is stratified if it admits a stratification. All definite programs are stratified.

Stratified programs have a least Herbrand model (LHM), which is constructed using the immediate consequence operator TP . Let U and B be the Herbrand universe and base of P, and let S ⊆ B. Then, TP(S) consists of all facts in head(r)σ with r ∈ P and σ a substitution from vars(r) to U satisfying body+(r)σ ⊆ S and body-(r)σ ∩ S = ∅. The powers of TP are as follows: T 0P (S) = S, T n+1 P (S) = TP(T n P (S)), and T ω P (S) = ⋃∞i=0 T iP (S). Let str be a stratification of P, and let (P1, . . . ,Pk) be its stratification partition. Also, let U1 = T ω P1 (∅) and for each 1 ≤ i ≤ k let Ui+1 = T ω Pi+1 (Ui). Then, the LHM of P is Uk and is denoted M[P]. A program P entails a positive existential sentence α (P |= α) if M[P] seen as a FO structure satisfies α.

We use LPs to encode FO theories. For this, we introduce rules axiomatising the built-in semantics of the equality (≈) and truth (⊤) predicates. For a finite signature Σ, we denote with F ⊤ Σ the smallest set with a rule

1 We assume rule heads non-empty, and allow multiple atoms.

for each n-ary predicate p in Σ, and with F ≈ Σ the usual axiomatisation of ≈ as a congruence over Σ. For an LP P, we denote with P ≈,⊤ the extension of P to P ∪ F ⊤ Σ ∪F ≈ Σ with Σ the signature of P.

Ontologies and Queries We define Horn-ALCHOIQ and specify its semantics via translation to definite programs. W.l.o.g. we consider ontologies in a normal form close to that in [Ortiz et al., 2010]. Let NC, NR and NI be countable pairwise disjoint sets of concept names, role names and individuals. We assume {⊤,⊥} ⊆ NC. A role is an element of NR ∪ {R-|R ∈ NR}, where the roles in the latter set are called inverse roles. The function Inv(·) is defined as follows, where R ∈ NR: Inv(R) = R- and Inv(R-) = R. An RBox R is a finite set of axioms (R2) in Table 1, where R and S are roles and ⊑∗R is the minimal reflexive-transitive relation over roles s.t. Inv(R) ⊑∗R Inv(S) and R ⊑∗R S hold if R ⊑ S ∈ R. A TBox T is a finite set of axioms (T1)-(T5) where A,B ∈ NC and R is a role. 2 An ABox A is a finite set of axioms of the form (A1) and (A2), with A ∈ NC and R ∈ NR. An ontology is a finite set of axioms O = R∪T ∪A.

OWL 2 specifies the EL, QL, and RL profiles; these are fragments of Horn-ALCHOIQ with the exception of property chain axioms and transitivity, which we do not consider here. An ontology is: (i) EL if it does not contain inverse roles or axioms (T4); (i) RL if it does not contain axioms (T5); and (i) QL if it does not contain axioms (T2) or (T4), each axiom (T1) satisfies n = 1, and each axiom (T3) satisfies A = ⊤.

A conjunctive query (CQ) Q is a formula ∃⃗y.ψ(⃗x, ⃗y) with ψ(⃗x, ⃗y) a conjunction of function-free atoms over ⃗x∪⃗y, where ⃗x are the answer variables. We denote with terms(Q) the set of terms in Q. Queries with no answer variables are Boolean (BCQs) and for convenience are written as a set of atoms.

We define the semantics by a mapping π into definite rules as in Table 1: π(O) = {π(α) | α ∈ O} 3 . An ontology O is satisfiable if π(O)≈,⊤ ̸|= ∃y.⊥(y). A tuple of constants ⃗c is an answer to Q if O is unsatisfiable, or π(O)≈,⊤ |= ∃⃗y.ψ(⃗c, ⃗y). The set of answers is written cert(Q,O). This semantics is equivalent to the usual one.

2 Axioms A ⊑ ≥nR.B can be simulated by (T1) and (T5).

3 By abuse of notation we say that R- ∈ O whenever R- occurs in O.

3 Reasoning over RSAOntologies

CQ answering is EXPTIME-complete for Horn-ALCHOIQ ontologies [Ortiz et al., 2010], and the EXPTIME lower bound holds already for satisfiability checking. Intractability is due to and-branching: owing to the interaction between axioms in Table 1 of type (T5) with either axioms (T3) and (R1), or axioms (T4) an ontology may only be satisfied by large (possibly infinite) models which cannot be succinctly represented.

RSA is a class of ontologies where all axioms in Table 1 are allowed, but their interaction is restricted s.t. model size can be polynomially bounded [Carral et al., 2014b]. We next recapitulate RSA ontologies and their properties; in the remainder, we fix an arbitrary Horn-ALCHOIQ ontology O.

Roles in O are divided into safe and unsafe. The intuition is that unsafe roles may participate in harmful interactions.

Definition 1 A role R in O is unsafe if it occurs in axioms (T5), and there is a role S s.t. either of the following holds:

1. R ⊑∗R Inv(S) and S occurs in an axiom (T3) with lefthand-side concept ∃S.A where A ̸= ⊤.
2. S is in an axiom (T4) and R ⊑∗R S or R ⊑∗R Inv(S).

A role R in O is safe, if it is not unsafe.

It follows from Definition 1 that RL, QL, and EL ontologies contain only safe roles.

Example 1 Let OEx be the (out-of-profile) ontology with the following axioms, which we will use as a running example:

A(a) (1) A ⊑D (2) A ⊑ ∃S-.C (3) ∃S.A ⊑D (4) D ⊑ ∃R.B (5) B ⊑ ∃S.D (6) R ⊑ T - (7) S ⊑ T (8)

Roles R, S, T , and T - are safe; however, S- is unsafe as it occurs in an axiom (T5) while S occurs in an axiom (T3).

The distinction between safe and unsafe roles makes it possible to strengthen the translation π in Table 1 while preserving satisfiability and entailment of unary facts. The translation of axioms (T5) with R safe can be realised by replacing the functional term f A R,B (x) with a Skolem constant vA R,B unique to A, R and B. The modified transformation typically leads to a smaller LHM: if all roles are safe then O is mapped to a datalog program whose LHM is of size polynomial in the size of O.

Definition 2 Let vA R,B be a fresh constant for each pair of concepts A, B and each safe role R in O. The function πsafe maps each α ∈ O to

1. a rule A(x) → R(x, vA R,B ) ∧ B(vA R,B ) if α is of type (T5) with R safe; and
2. a rule π(α) otherwise.

Let P = {πsafe(α) | α ∈ O}; then, we define PO = P ≈,⊤.

Example 2 Mapping πsafe differs from π on ax. (5), and (6). For instance, (5) yields D(x) → R(x, vD R,B ) ∧ B(vD R,B ).

The properties of PO are given by the following theorem.

Theorem 1 [Carral et al., 2014b, Theorem 2] Ontology O is satisfiable iff PO ̸|= ∃y.⊥(y). If O is satisfiable, then O |= A(c) iff A(c) ∈ M[PO] for each unary predicate A and constant c in O.

If O has unsafe roles the model M[PO] might be infinite. We next define a datalog program PRSA by introducing Skolem constants for all axioms (T5) in O. PRSA introduces also a predicate PE which 'tracks' all binary facts generated by the application of Skolemised rules over unsafe roles. A unary predicate U is initialised with the constants associated to unsafe roles and a rule U(x) ∧ PE(x, y) ∧ U(y) → E(x, y) stores the PE-facts originating from unsafe roles using a predicate E. Then, M[PO] is of polynomial size when the graph induced by the extension of E is an oriented forest (i.e., a DAG whose underlying undirected graph is a forest). When this condition is fulfilled together with some additional conditions which preclude harmful interactions between equalitygenerating axioms and inverse roles, we say that O is RSA.

Definition 3 Let PE and E be fresh binary predicates, let U be a fresh unary predicate, and let uAR,B be a fresh constant for each concept A, B and each role R in O. Function πRSA maps each α ∈ O to

• A(x) → R(x, uAR,B ) ∧ B(uAR,B ) ∧ PE(x, uAR,B ) if α is of type (T5) and
• π(α), otherwise.

The program PRSA consists of πRSA(α) for each α ∈ O, a rule U(x) ∧ PE(x, y) ∧ U(y) → E(x, y), and a fact U(uAR,B ) for each uAR,B with R unsafe.

Let MRSA be the LHM of PRSA≈,⊤. Then, GO is the digraph with an edge (c, d) for each E(c, d) in MRSA. Ontology O is equality-safe if:

• for each pair of atoms w ≈ t (with w and t distinct) and R(t, uAR,B ) in MRSA and each role S s.t. R ⊑ Inv(S), it holds that S does not occur in an axiom (T4); and
• for each pair of atoms R(a, uAR,B ), S(uAR,B , a) inMRSA, with a ∈ NI, there does not exist a role T such that both R ⊑∗R T and S ⊑∗R Inv(T ) hold.

We say that O is RSA if it is equality-safe and GO is an oriented forest.

The fact that GO is a DAG ensures that the LHMM[PO] is finite, whereas the lack of 'diamond-shaped' subgraphs in GO guarantees polynomiality of M[PO]. The safety condition on ≈ ensures that RSA ontologies enjoy a special form of forest-model property that we exploit for CQ answering. Every ontology in QL (which is equality-free), RL (where PRSA has no Skolem constants) and EL (no inverse roles) is RSA.

Theorem 2 [Carral et al., 2014b, Theorem 3] If O is RSA, then |M[PO]| is polynomial in |O|.

Tractability of standard reasoning for RSA ontologies follows from Theorems 1, 2. It can be checked that OEx is RSA.

4 Answering Queries over RSAOntologies

We next present our combined approach with filtration to CQ answering over RSA ontologies, which generalises existing techniques for DL-LiteR and ELHO.

In Section 4.1 we take the LHM for RSA ontologies given in Section 3 as a starting point and extend it to a more convenient canonical model over an extended signature. In order to deal with the presence of inverse roles in RSA ontologies, the extended model captures the 'directionality' of binary atoms; this will allow us to subsequently extend the filtration approach from [Stefanoni et al., 2013] in a seamless way. The canonical model is captured declaratively as the LHM of an LP program over the extended signature.

As usual in combined approaches, this model is not universal (it cannot be homomorphically embedded into every other model of the ontology) and the evaluation of CQs may lead to spurious, i.e. unsound answers. In Section 4.2, we specify our filtration approach for RSA ontologies as the LHM of a stratified program. In the following, we fix an arbitrary RSA ontology O = R ∪ T ∪ A and an input CQ Q, which we use to parameterise all our technical results.

4.1 Constructing the Canonical Model

The LHMM[PO] in Section 3 is a model of O that preserves entailment of unary facts. It generalises the canonical model in [Stefanoni et al., 2013], which is specified as the LHM of a datalog program obtained by Skolemising all axioms (T5). However, RSA ontologies allow for unsafe roles and hence M[PO] may contain also functional terms.

A main source for spurious matches when evaluating Q over the canonical model of an EL ontology is the presence of 'forks'-confluent chains of binary atoms- in the query which map to 'forks' in the model over Skolem constants. This is also problematical in our setting since RSA ontologies have the forest-model property.

Example 3 Fig. 1 a) depicts the LHMM[POEx ] of OEx (the function fS,C is abbreviated with f). We see models as digraphs where the direction of edges reflects the satisfaction of axioms (T5). Consider Q1 = {A(y1), R(y1, y2), R(y3, y2)}. Substitution (y1 → a, y2 → vD R,B , y3 → vB S,D ) is a spurious match of Q1 as it relies on edges (a, vD R,B ) and (vB S,D , vD R,B )) in M[POEx ], which form a fork over vD R,B .

In EL, only queries which themselves contain forks can be mapped to forks in the model. This is, however, no longer the case for RSA ontologies, where forks in the model can lead to spurious answers even for linearly-shaped queries due to the presence of inverse roles.

Example 4 Let Q2 = {A(y1),R(y1, y2), T(y2, y3)}. Substitution (y1 → a, y2 → vD R,B , y3 → f(a)) is a spurious match for Q2 as it relies on the fork (a, vD R,B ), (f(a), vD R,B ))

in M[POEx ]. This is due to axiom R ⊑ T - which causes a linear match over R and T to become a fork over R and T -.

To identify such situations, we compute a canonical model over an extended signature that contains fresh roles Rf and Rb for each role R. Annotations f (forward) and b (backwards) are intended to reflect the directionality of binary atoms in the model, where binary atoms created to satisfy an axiom (T5) are annotated with f. To realise this intuition declaratively, we modify the rules in PO for axioms (T5) as follows. If R is safe, then we introduce the rule A(x) → Rf (x, vA R,B ) ∧ B(vA R,B ); if it is unsafe, we introduce rule A(x) → Rf (x, f A R,B (x)) ∧ B(f A R,B (x)) instead.

Roles inherit the direction of their subroles, while roles and their inverses have opposite direction. This is captured with the following rules for ∗ ∈ {f, b}: (i) R∗ (x, y) → S∗ (x, y) for each R ⊑ S in O; (ii) Rf (x, y) → Inv(R)b (y, x) and Rb (x, y) → Inv(R)f (y, x) for each role R; and (iii) R∗ (x, y) → R(x, y) for each role R. Rules (ii) are included only if O has inverse roles, and rules (iii) 'copy' annotated atoms to atoms over the original predicate. Fig. 1 b) depicts the annotated model for POEx where solid (resp. dotted) lines represent 'forward' (resp. 'backwards') atoms.

Fig. 2 depicts the ways in which query matches may spuriously rely on a fork in an annotated model. Nodes represent the images in the model of the query terms; solid lines indicate the annotated atoms responsible for the match; and dashed lines depict the underpinning fork. The images of s and t must not be equal; additionally, y cannot be mapped to (a term identified to) a constant in O. For instance, the match in Ex. 4 is spurious as it corresponds to pattern (b) in Fig. 2.

Unfortunately, the annotated model can present ambiguity: it is possible for both atoms Rf (s, t) and Rb (s, t) to hold.

Example 5 Consider Q2 from Ex. 4. An alternative match is (y1 → a, y2 → vD R,B , y3 → vB S,D ), where T f (vD R,B , vB S,D ) and T b (vD R,B , vB S,D ) hold in the annotated model. The reason is that Sf (vD R,B , vB S,D ) and Rf (vB S,D , vD R,B ) form a cycle in the model and S ⊑∗R T and R ⊑∗R T - hold in OEx.

Such ambiguity is problematic for the subsequent filtration step. To disambiguate, we use a solution similar to the technique in [Lutz et al., 2013] for DL-LiteR, where the idea is to unfold certain cycles of length one (self-loops) and two in the canonical model by introducing additional auxiliary constants. We unfold self-loops to cycles of length three while cycles of length two are unfolded to cycles of length four.

Example 6 Fig. 3 a) shows the model expansion for ontology OEx. Note that ambiguities are resolved. Fig. 3 b) shows the unfolding of a generic self-loop over a safe role R for which T exists s.t. R ⊑ T and R ⊑ Inv(T ) hold.

We now specify a program that yields the required model.

Definition 4 Let confl(R) be the set of roles S s.t. R ⊑∗R T and S ⊑∗R Inv(T ) for some T . Let ≺ be a strict total order on triples (A, R, B), with R safe and A, B concept names in O. For each (A,R,B), let vA,0 R,B , vA,1 R,B , and vA,2 R,B be fresh constants; let self(A,R,B) be the smallest set containing vA,0 R,B and vA,1 R,B if R ∈ confl(R); and let cycle(A,R,B) be the smallest set of terms containing, for each S ∈ confl(R),

• vD,0 S,C if (A, R, B) ≺ (D, S, C);
• vD,1 S,C if (D, S, C) ≺ (A, R, B); and
• f D S,C (vA,0 R,B ) and each f F T ,E (vA,0 R,B ) s.t. uDS,C ≈ uFT,E is in MRSA, if S is unsafe.

Finally, unfold(A, R, B) = self(A, R, B) ∪ cycle(A, R, B). Let Rf and Rb be fresh binary predicates for each role R in O, let NI be a fresh unary predicate, and notIn be a built-in predicate which holds when the first argument is an element of the set given as second argument. Let P be the smallest program with a rule → NI(a) for each constant a and all rules in Table 2. We define EO = P ≈,⊤.

The set confl(R) contains the roles that may cause ambiguity in conjunction with R. The ordering ≺ determines how cycles are unfolded using auxiliary constants. Each axiom A ⊑ ∃R.B with R safe is Skolemised by default using vA,0 R,B , except when the axiom applies to an auxiliary constant in unfold(R, B) where we use vA,1 R,B or vA,2 R,B instead.

Theorem 3 The following holds: (i) M[EO] is polynomial in |O| (ii) O is satisfiable iff EO ̸|= ∃y.⊥(y) (iii) if O is satisfiable, O |= A(c) iff A(c) ∈ M[EO] and (iv) there are no terms s, t and role R s.t. EO |= Rf (s, t) ∧ Rb (s, t).

4.2 Filtering Unsound Answers

We now define a program PQ that can be used to eliminate all spurious matches of Q over the annotated model of O. The rules of the program are summarised in Table 3. In what follows, we refer to all functional terms and Skolem constants in the model that are not equal to a constant in O as anonymous.

Matches where an answer variable is not mapped to a constant in O are spurious. We introduce a predicate named and populate it with such constants (rules (2)); then, we flag answers as spurious using a rule with negation (rules (8a)).

To detect forks we introduce a predicate fk, whose definition in datalog will encode the patterns in Fig. 2 (rules (4)). If terms s and t in Fig. 2 are existential variables mapping to the same anonymous term, further forks might be recursively induced due to the identity of s and t.

the only match over the model in Fig. 3a). The identity of y2, y5 induces a fork on the match of R(y1, y2) and R(y4, y5).

We track identities in the model relative to a match using a fresh predicate id. It is initialised as the minimal congruence relation over the positions of the existential variables in the query which are mapped to anonymous terms (rules (3)). Identity is recursively propagated using rules (5). Matches involving forks are marked as spurious by rule (8b).

Spurious matches can also be caused by cycles in the model and query satisfying certain requirements. First, the positions of existential variables of the query must be cyclic when considering also the id relation. Second, the match must involve only anonymous terms. Finally, all binary atoms must have the same directionality.

Example 8 Consider the following BCQs over OEx:

Then, (y1 → vD,0 R,B , y2 → vB,0 S,D , y3 → vD,1 R,B , y4 → vB,1 S,D ) is a match of Q4 inducing a cycle: all binary atoms are mapped 'forward' and the cycle involves only anonymous terms. In contrast, match (y1 → vD,0 R,B , y2 → f(a), y3 → a) over Q5 does not satisfy the requirements as it involves constant a and the atoms do not have the same directionality. Note that Q4 and Q5 are cyclic. In contrast, Q6 is not cyclic; thus, although the match (y1 → vD,0 R,B , y2 → vB,0 S,D , y3 → vD,1 R,B , y4 → vB,1 S,D , y5 → vD,0 R,B ) involves a cycle in the model with the required properties, it is not spurious.

Such cycles are recognised by rules (6) and (7). Rule (6) defines potential arcs in the cycle with their directionality, and the position of each relevant existential variable. These are recorded using predicates AQ∗ with ∗ ∈ {f, b}. Rules (7) detect the cycles recursively using predicates TQ∗ . Matches involving cycles are marked as spurious by rules (8c). All correct answers are collected by rule (9) using predicate Ans.

We now define program PQ and its extension PO,Q with EO in Def. 4, which can be exploited to answer Q w.r.t. O.

Definition 5 Let Q = ∃⃗y.ψ(⃗x, ⃗y) be a CQ, let QM, sp, and fk be fresh predicates of arity |⃗x|+|⃗y|, let id, AQ∗ , and TQ∗ , with ∗ ∈ {f, b}, be fresh predicates of arity |⃗x| + |⃗y| + 2, let Ans be a fresh predicate of arity |⃗x|, let named be a fresh unary predicate, and let U be a set of fresh variables s.t. |U| ≥ |⃗y|. Then, PQ is the smallest program with all rules in Table 3, and PO,Q is defined as EO ∪ PQ.

Note that ≈ is not axiomatised for the symbols in PQ that do not occur in EO. In this way, we can distinguish between the constants in O (recorded by predicate named in PQ) and their closure under equality (recorded by NI in EO).

Theorem 4 (i) PO,Q is stratified; (ii) M[PO,Q] is polynomial in |O| and exponential in |Q|; and (iii) if O is satisfiable, ⃗x ∈ cert(Q, O) iff PO,Q |= Ans(⃗x).

Theorem 4 suggests a worst-case exponential algorithm that, given O and Q, materialises PO,Q and returns the extension of predicate Ans. This procedure can be modified to obtain a 'guess and check' algorithm applicable to BCQs. This algorithm first materialises EO in polynomial time; then, it guesses a match σ to Q over the materialisation; finally, it materialises (PO,Q)σ, where variables ⃗x and ⃗y are grounded by σ. The latter step can also be shown to be tractable.

Theorem 5 Checking whether O |= Q with O an RSA ontology and Q a BCQ is NP-complete in combined complexity.

5 Proof of Concept

We have implemented our approach using the DLVsystem, 4 which supports function symbols and stratified negation. For testing, we have used the LUBM ontology [Guo et al., 2005] (which contains only safe roles) and the Horn fragments of the Reactome and Uniprot (which are RSA, but contain also unsafe roles). 5 LUBM comes with a data generator; Reactome and Uniprot come with large datasets, which we have sampled. All test queries are given in the appendix. In each experiment, we measured (M1) size (number of facts) of the given data; (M2) materialisation times for the canonical model; (M3) model size; (M4) query processing times (i.e., time needed to materialise PQ); (M5) number of candidate query answers, i.e. (unfiltered) answers of the query over the canonical model; and (M6) percentage of spurious answers. All experiments were performed on a MacBook Pro laptop with 8GB RAM and an Intel Core 2.4 GHz processor.

Fig. 4 and 5 summarise our results. The relevant measures M1-M5 are indicated in the headings of the tables. We can see that computation times for the models scale linearly in data size. Model size is at most 6 times larger than the original data, which we see as a reasonable growth factor in practice. As usual in combined approaches (e.g., see [Stefanoni et al., 2013]), query processing times depend on the number of candidate answers; thus, the applicability of the combined approach largely depends on the ratio between spurious and correct answers. Queries q1-q2 in Reactome and Uniprot are realistic queries given as examples in the EBI website. Neither of these queries lead to spurious answers, and processing times scale linearly with data size. No query in the LUBM benchmark leads to spurious answers (e.g., LUBM queries q3 and q4 in Fig. 5). Thus, we manually crafted one additional query for Reactome and Uniprot (q3 in both cases) and two for LUBM (queries q1 and q2), which lead to a high percentage of spurious answers. Although these queries are challenging, we can observe that the proportion of spurious answers (and thus growth in processing times) remains constant with increasing data size. Finally, note that query q1 in LUBM retrieves the highest number of candidate answers and is thus the most challenging query. Our prototype and all test data, ontologies and queries are available at http://tinyurl.com/qcolx3w.

4 http://www.dlvsystem.com/dlv/

5 http://www.ebi.ac.uk/rdf/platform

6 Conclusions and FutureWork

We have presented an extension to the combined approaches to query answering that can be applied to a wide range of out-of-profile Horn ontologies. Our theoretical results unify and extend existing techniques for ELHO and DL-LiteR in a seamless and elegant way. Our preliminary experiments indicate the feasibility of our approach in practice.

We anticipate several directions for future work. First, we have not considered logics with transitive roles. Recently, it was shown that CQ answering over EL ontologies with transitive roles is feasible in NP [Stefanoni and Motik, 2015]. We believe that our techniques can be extended in a similar way. Finally, we would like to optimise our encoding into LP and conduct a more extensive evaluation.