Computing Datalog Rewritings Beyond Horn Ontologies

1 Introduction

Answering conjunctive queries (CQs) over OWL 2 DL ontologies is a computationally hard [Glimm et al., 2008; Lutz, 2008], but key problem in many applications. Thus, considerable effort has been devoted to the development of OWL 2 DL fragments for which query answering is tractable in data complexity, which is measured in the size of the data only. Most languages obtained in this way are Horn: ontologies in such languages can always be translated into first-order Horn clauses. This includes the families of 'lightweight' languages such as DL-Lite [Calvanese et al., 2007], EL [Baader et al., 2005], and DLP [Grosof et al., 2003] that underpin the QL, EL, and RL profiles of OWL 2, respectively, as well as more expressive languages, such as Horn-SHIQ [Hustadt et al., 2005] and Horn-SROIQ [Ortiz et al., 2011].

Query answering can sometimes be implemented via query rewriting: a rewriting of a query Q w.r.t. an ontology T is another query Q′ that captures all information from T necessary to answer Q over an arbitrary data set. Unions of conjunctive queries (UCQs) and datalog are common target languages for query rewriting. They ensure tractability w.r.t. data complexity, while enabling the reuse of optimised data management systems: UCQs can be answered using relational databases [Calvanese et al., 2007], and datalog queries can be answered using rule-based systems such as OWLim [Bishop et al., 2011] and Oracle's Semantic Data Store [Wu et al., 2008]. Query rewriting algorithms have so far been developed mainly for Horn fragments of OWL 2 DL, and they have been implemented in systems such as QuOnto [Acciarri et al., 2005], Rapid [Chortaras et al., 2011], Presto [Rosati and Almatelli, 2010], Quest [Rodriguez-Muro and Calvanese, 2012], Clipper [Eiter et al., 2012], Owlgres [Stocker and Smith, 2008], and Requiem [P´erez-Urbina et al., 2010].

∗Work supported by the Royal Society, the EPSRC projects Score!, Exoda, and MaSI3 , and an FP7 Marie Curie Fellowship.

Horn fragments of OWL 2 DL cannot capture disjunctive knowledge, such as 'every student is either an undergraduate or a graduate'. Such knowledge occurs in practice in ontologies such as the NCI Thesaurus and the Foundational Model of Anatomy, so these ontologies cannot be processed using known rewriting techniques; furthermore, no query answering technique we are aware of is tractable w.r.t. data complexity when applied to such ontologies. These limitations cannot be easily overcome: query answering in even the basic non-Horn language ELU is co-NP-hard w.r.t. data complexity [Krisnadhi and Lutz, 2007], and since answering datalog queries is PTIME-complete, it may not be possible to rewrite an arbitrary ELU ontology into datalog unless PTIME = NP. Furthermore, Lutz andWolter [2012] showed that tractability w.r.t. data complexity cannot be achieved for an arbitrary nonHorn ontology T with 'real' disjunctions: for each such T , a query Q exists such that answering Q w.r.t. T is co-NP-hard.

The result by Lutz and Wolter [2012], however, depends on an interaction between existentially quantified variables in Q and disjunctions in T . Motivated by this observation, we consider the problem of computing datalog rewritings of ground queries (i.e., queries whose answers must map all the variables in Q to constants) over non-Horn ontologies. Apart from allowing us to overcome the negative result by Lutz and Wolter [2012], this also allows us to compute a rewriting of T that can be used to answer an arbitrary ground query. Such queries form the basis of SPARQL, which makes our results practically relevant. We summarise our results as follows.

In Section 3, we revisit the limits of datalog rewritability for a language as a whole and show that non-rewritability of ELU ontologies is independent from any complexitytheoretic assumptions. More precisely, we present an ELU ontology T for which query answering cannot be decided by a family of monotone circuits of polynomial size, which contradicts the results by Afrati et al. [1995], who proved that fact entailment in a fixed datalog program can be decided using monotone circuits of polynomial size. Thus, instead of relying on complexity arguments, we compare the lengths of proofs in ELU and datalog and show that the proofs in ELU may be considerably longer than the proofs in datalog.

In Section 4, we present a three-step procedure that takes a SHI-ontology T and attempts to rewrite T into a datalog program. First, we use a novel technique to rewrite T into a TBox ΩT without transitivity axioms while preserving entailment of all ground atoms; this is in contrast to the standard techniques (see, e.g., [Hustadt et al., 2007]), which preserve entailments only of unary facts and binary facts with roles not having transitive subroles. Second, we use the algorithm by Hustadt et al. [2007] to rewrite ΩT into a disjunctive datalog program DD(ΩT ). Third, we adapt the knowledge compilation technique by del Val [2005] and Selman and Kautz [1996] to transform DD(ΩT ) into a datalog program. The final step is not guaranteed to terminate in general; however, if it terminates, the resulting program is a rewriting of T .

In Section 4.4, we show that our procedure always terminates if T is a DL-LiteH,+ bool -ontology-a practically-relevant language that extends OWL 2 QL with transitive roles and Boolean connectives. Artale et al. [2009] proved that the data complexity of concept queries in this language is tractable (i.e., NLOGSPACE-complete). We extend this result to all ground queries and thus obtain a goal-oriented rewriting algorithm that may be suitable for practical use.

Our technique, as well as most rewriting techniques known in the literature, is based on a sound inference system and thus produces only strong rewritings-that is, rewritings entailed by the original ontology. In Section 5 we show that non-Horn ontologies exist that can be rewritten into datalog, but that have no strong rewritings. This highlights the limits of techniques based on sound inferences. It is also surprising since all known rewriting techniques for Horn fragments of OWL 2 DL known to us produce only strong rewritings.

The proofs of all of our technical results are given in the accompanying technical report [Cuenca Grau et al., 2013].

2 Preliminaries

We consider first-order logic without equality and function symbols. Variables, terms, (ground) atoms, literals, formulae, sentences, interpretations I = (∆I , ·I ), models, and entailment (|=) are defined as usual. We call a finite set of facts (i.e., ground atoms) an ABox. We write ϕ(⃗x) to stress that a first-order formula ϕ has free variables ⃗x = x1, . . . , xn.

Resolution Theorem Proving

We use the standard notions of (Horn) clauses, substitutions (i.e., mappings of variables to terms), and most general unifiers (MGUs). We often identify a clause with the set of its literals. Positive factoring (PF) and binary resolution (BR) are as follows, where σ is the MGU of atoms A and B:

A clause C is a tautology if it contains literals A and ¬A. A clause C subsumes a clause D if a substitution σ exists such that each literal in Cσ occurs in D. Furthermore, C

θ-subsumes D if C subsumes D and C has no more literals than D. Finally, C is redundant in a set of clauses S if C is a tautology or if C is θ-subsumed by another clause in S.

Datalog and Disjunctive Datalog

A disjunctive rule r is a function-free first-order sentence of the form ∀⃗x∀⃗z.[ϕ(⃗x, ⃗z) →ψ(⃗x)], where tuples of variables ⃗x and ⃗z are disjoint, ϕ(⃗x, ⃗z) is a conjunction of atoms, and ψ(⃗x) is a disjunction of atoms. Formula ϕ is the body of r, and formula ψ is the head of r. For brevity, we often omit the quantifiers in a rule. A datalog rule is a disjunctive rule where ψ(⃗x) is a single atom. A (disjunctive) datalog program P is a finite set of (disjunctive) datalog rules. Rules obviously correspond to clauses, so we sometimes abuse our definitions and use these two notions as synonyms. The evaluation of P over an ABox A is the set P(A) of facts entailed by P ∪ A.

Ontologies and Description Logics

A DL signature is a disjoint union of sets of atomic concepts, atomic roles, and individuals. A role is an atomic role or an inverse role R- for R an atomic role; furthermore, let inv(R) = R- and inv(R-) = R. A concept is an expression of the form ⊤, ⊥, A, ¬C, C1 ⊓C2, C1 ⊔C2, ∃R.C, ∀R.C, or ∃R.self, where A is an atomic concept, C(i) are concepts, and R is a role. Concepts ∃R.self correspond to atoms R(x, x) and are typically not included in SHI; however, we use this minor extension in Section 4.1. A SHI-TBox T , often called an ontology, is a finite set of axioms of the form R1 ⊑ R2 (role inclusion axioms or RIAs), Tra(R) (transitivity axioms), and C1 ⊑ C2 (general concept inclusions or GCIs), where R(i) are roles and C(i) are concepts. Axiom C1 ≡ C2 abbreviates C1 ⊑ C2 and C2 ⊑ C1. Relation ⊑∗T is the smallest reflexively-transitively closed relation such that R ⊑∗T S and inv(R) ⊑∗T inv(S) for each R ⊑ S ∈ T . A role R is transitive in T if Tra(R) ∈ T or Tra(inv(R)) ∈ T . Satisfaction of a SHI-TBox T in an interpretation I = (∆I , ·I ), written I |= T , is defined as usual [Baader et al., 2003].

An ALCHI-TBox is a SHI-TBox with no transitivity axioms. An ELU-TBox is an ALCHI-TBox with no role inclusion axioms, inverse roles, concepts ∃R.self, or symbols ⊥, ∀, and ¬. A DL-LiteH,+ bool -TBox is a SHI-TBox that does not contain concepts of the form ∀R.C, and where C = ⊤ for each concept of the form ∃R.C. The notion of acyclic TBoxes is defined as usual [Baader et al., 2003].

A SHI-TBox T is normalised if ∀ does not occur in T , and ∃ occurs in T only in axioms of the form ∃R.C ⊑ A, ∃R.self ⊑ A, A ⊑ ∃R.C, or A ⊑ ∃R.self. Each SHI-TBox T can be transformed in polynomial time into a normalised SHI-TBox that is a model-conservative extension of T .

Queries and Datalog Rewritings

A ground query (or just a query) Q(⃗x) is a conjunction of function-free atoms. A substitution σ mapping ⃗x to constants is an answer to Q(⃗x) w.r.t. a set F of first-order sentences and an ABox A if F ∪ A |= Q(⃗x)σ; furthermore, cert(Q, F, A) is the set of all answers to Q(⃗x) w.r.t. F and A.

Let Q be a query. A datalog program P is a Q-rewriting of a finite set of sentences F if cert(Q,F,A) = cert(Q,P,A) for each ABox A. The program P is a rewriting of F if P

is a Q-rewriting of F for each query Q. Such rewritings are strong if, in addition, we also have F |= P.

3 The Limits of Datalog Rewritability

Datalog programs can be evaluated over an ABox A in polynomial time in the size of A; hence, a co-NP-hard property of A cannot be decided by evaluating a fixed datalog program over A unless PTIME = NP. Krisnadhi and Lutz [2007] showed that answering ground queries is co-NP-hard in data complexity even for acyclic TBoxes expressed in ELU-the simplest non-Horn extension of the basic description logic EL. Thus, under standard complexity-theoretic assumptions, an acyclic ELU-TBox and a ground query Q exist for which there is no Q-rewriting of T . In this section, we show that this holds even if PTIME = NP.

Theorem 1. An acyclic ELU-TBox T and a ground CQ Q exist such that T is not Q-rewritable.

Our proof uses several notions from circuit complexity [Wegener, 1987], and results of this flavour compare the sizes of proofs in different formalisms; thus, our result essentially says that proofs in ELU can be significantly longer than proofs in datalog. Let < be the ordering on Boolean values defined by f < t; then, a Boolean function f with n inputs is monotone if f(x1, . . . , xn) ≤ f(y1, . . . , yn) holds for all n-tuples of Boolean values x1, . . . , xn and y1, . . . , yn such that xi ≤ yi for each 1 ≤ i ≤ n. A decision problem can be seen as a family of Boolean functions {fn}, where fn decides membership of each n-bit input. If each function fn is monotone, then fn can be realised by a monotone Boolean circuit Cn (i.e., a circuit with n input gates where all internal gates are AND- or OR-gates with unrestricted fan-in); the size of Cn is the number of its edges. The family of circuits {Cn} corresponding to {fn} has polynomial size if a polynomial p(x) exists such that the size of each Cn is bounded by p(n).

We recall how non-3-colorability of an undirected graph G with s vertices corresponds to monotone Boolean functions. The maximum number of edges in G is m(s) = s(s - 1)/2, so graph G is encoded as a string ⃗x of m(s) bits, where bit xi,j , 1 ≤ i < j ≤ s, is t if and only if G contains an edge between vertices i and j. The non-3-colorability problem can then be seen as a family of Boolean functions {fm(s)}, where function fm(s) handles all graphs with s vertices and it evaluates to t on an input ⃗x iff the graph corresponding to ⃗x is non-3-colourable. Functions fn such that n ̸=m(s) for all s are irrelevant since no graph is encoded using that many bits.

We prove our claim using a result by Afrati et al. [1995]: if a decision problem cannot be solved using a family of monotone circuits of polynomial size, then the problem also cannot be solved by evaluating a fixed datalog program, regardless of the problem's complexity. We restate the result as follows.

Theorem 2. [Adapted from Afrati et al. 1995]

1. Let P be a fixed datalog program, and let α be a fixed fact. Then, for an ABox A, deciding P ∪ A |= α can be solved by monotone circuits of polynomial size.
2. The non-3-colorability problem cannot be solved by monotone circuits of polynomial size.

To prove Theorem 1, we present a TBox T and a ground CQ Q that decide non-3-colorability of a graph encoded as an ABox. Next, we present a family of monotone Boolean functions {gn(u)} that decide answering Q w.r.t. T an arbitrary ABox A. Next, we show that a monotone circuit for arbitrary fm(s) can be obtained by a size-preserving transformation from a circuit for some gn(u); thus, by Item 2 of Theorem 2, answering Q w.r.t. T cannot be solved using monotone circuits of polynomial size. Finally, we show that existence of a rewriting for Q and T contradicts Item 1 of Theorem 2.

4 Computing Rewritings via Resolution

Theorem 1 is rather discouraging since it applies to one of the simplest non-Horn languages. The theorem's proof, however, relies on a specific TBox T that encodes a hard problem (i.e., non-3-colorability) that is not solvable by monotone circuits of polynomial size. One can expect that non-Horn TBoxes used in practice do not encode such hard problems, and so it might be possible to rewrite such TBoxes into datalog.

We illustrate this intuition using the TBox Tex shown in Table 1. Axioms γ4-γ6 correspond to datalog rules, whereas axioms γ1-γ3 represent disjunctive and existentially quantified knowledge and thus do not correspond to datalog rules. We will show that Tex can, in fact, be rewritten into datalog using a generic three-step method that takes a normalised SHI-TBox T and proceeds as follows.

• S1 Eliminate the transitivity axioms from T by transforming T into an ALCHI-TBox ΩT and a set of datalog rules ΞT such that facts entailed by T ∪A and ΩT ∪ΞT (A) coincide for each ABox A. This step extends the known technique to make it complete for facts with roles that have transitive subroles in T .
• S2 Apply the algorithm by Hustadt et al. [2007] to transformΩT into a disjunctive datalog programDD(ΩT ).
• S3 Transform DD(ΩT ) into a set of datalog rules PH using a variant of the knowledge compilation techniques by Selman and Kautz [1996] and del Val [2005].

Step S3 may not terminate for an arbitrary SHI-TBox T ; however, if it terminates (i.e., if PH is finite), then PH ∪ΞT is a rewriting of T . Furthermore, in Section 4.4 we show that step S3 always terminates if T is a DL-LiteH,+ bool -TBox. We thus obtain what is, to the best of our knowledge, the first goal-oriented rewriting algorithm for a practically-relevant non-Horn fragment of OWL 2 DL.

4.1 Transitivity

We first recapitulate the standard technique for eliminating transitivity axioms from SHI-TBoxes.

Definition 3. Let T be a normalised SHI-TBox, and let ΘT be obtained from T by removing all transitivity axioms. If T is a DL-LiteH,+ bool -TBox, then let ΥT = ΘT ; otherwise, let ΥT be the extension of ΘT with axioms

for each axiom ∃S.A ⊑ B ∈ T and each transitive role R in T such that R ⊑∗T S, where CB,R is a fresh atomic concept unique for B and R.

This encoding preserves entailment of all facts of the form C(c) and U(c, d) if U has no transitive subroles: this was proved by Artale et al. [2009] for DL-LiteH,+ bool , and by Simancik [2012] for SHI. Example 4, however, shows that the encoding is incomplete if U has transitive subroles.

Example 4. Let T be the TBox below, and let A = {A(a)}.

Then, ΥT = T \ {Tra(R)}, and one can easily verify that T ∪A |= R(a, a), but ΥT ∪A ̸|= R(a, a). Note, however, that the missing inference can be recovered by extending ΥT with the axiom A ⊑ ∃R.self, which is a consequence of T .

The intuitions from Example 4 are formalised in Definition 5. Roughly speaking, we transform the transitivity and role inclusion axioms in T into a datalog program ΞT , which we apply to A 'first'-that is, we compute ΞT (A) independently from any GCIs. To recoup the remaining consequences of the form R(a, a), we extend ΥT with sufficiently many axioms of the form A ⊑ ∃R.self that are entailed by T ; this is possible since we assume that T is normalised.

Definition 5. Let T be a normalised SHI-TBox. Then, ΩT is the TBox obtained by extending ΥT with an axiom A ⊑ ∃R.self for each atomic concept A and each atomic role R such that R is transitive in T , and A ⊑ ∃S.B ∈ T for some concept B and role S with S ⊑∗T R and S ⊑∗T R-. Furthermore, ΞT is the set of datalog rules corresponding to the role inclusion and transitivity axioms in T .

Theorem 6. Let T be a normalised SHI-TBox, let A be an ABox, and let α be a fact. Then, T ∪A |= α if and only if ΩT ∪ΞT (A) |= α.

Note that, if T is normalised, so is ΩT . Furthermore, to ensure decidability, roles involving transitive subroles are not allowed occur in T in number restrictions, and so Theorem 6 holds even if T is a SHOIQ-TBox.

4.2 FromDLs to Disjunctive Datalog

Step S2 of our rewriting algorithm uses the technique by Hustadt et al. [2007] for transforming anALCHI-TBox T into a disjunctive datalog program DD(T ) such that, for each ABox A, the facts entailed by T ∪A and DD(T ) ∪A coincide. By eliminating the existential quantifiers in T , one thus reduces a reasoning problem in T ∪A to a reasoning problem in DD(T ) ∪ A. The following definition summarises the properties of the programs produced by the transformation.

Definition 7. A disjunctive datalog program P is nearlymonadic if its rules can be partitioned into two disjoint sets, P m and P r , such that

1. each rule r ∈ P m mentions only unary and binary predicates and each atom in the head of r is of the form A(z) or R(z, z) for some variable z, and
2. each rule r ∈ P r is of the form R(x, y) →S(x, y) or R(x, y) → S(y, x).

A disjunctive rule r is simple if there exists a variable x such that each atom in the body of r is of the form Ai(x), Ri(x, x), Si(x, yi), or Ti(yi, x), each atom in the head of r is of the form Ui(x, x) or Bi(x), and each variable yi occurs in r at most once. Furthermore, a nearly-monadic program P is simple if each rule in P m is simple.

Theorem 8 follows mainly from the results by Hustadt et al. [2007]; we just argue that concepts ∃R.self do not affect the algorithm, and that DD(T ) satisfies property 1.

Theorem8. For T a normalisedALCHI-TBox, DD(T ) satisfies the following:

1. programDD(T ) is nearly-monadic; furthermore, if T is a DL-LiteH,+ bool -TBox, then DD(T ) is also simple;
2. T |= DD(T ); and
3. cert(Q, T ,A) = cert(Q,DD(T ),A) for each ABox A and each ground query Q.

Example 9. When applied to the TBox Tex in Table 1, this algorithm produces the disjunctive program DD(Tex) shown (as clauses) in Table 2. In particular, axiom γ3 is eliminated since it contains an existential quantifier, but its effects are compensated by clause C3. Clauses C1-C2 and C4-C6 are obtained from axioms γ1-γ2 and γ4-γ6, respectively.

4.3 FromDisjunctive Datalog to Datalog

Step S3 of our rewriting algorithm attempts to transform the disjunctive program obtained in Step S2 into a datalog program such that, for each ABox A, the two programs entail the same facts. This is achieved using known knowledge compilation techniques, which we survey next.

Resolution-Based Knowledge Compilation

In their seminal paper, Selman and Kautz [1996] proposed an algorithm for compiling a set of propositional clauses S into a set of Horn clauses SH such that the Horn consequences of S and SH coincide. Subsequently, del Val [2005] generalised this algorithm to the case when S contains first-order clauses, but without any termination guarantees; Procedure 1 paraphrases this algorithm. The algorithm applies to S binary resolution and positive factoring from resolution theorem proving, and it keeps only the consequences that are not redundant according to Definition 10. Unlike standard resolution, the algorithm maintains two sets SH and SH of Horn

Procedure 1 Compile-Horn

Input: S: set of clauses Output: SH: set of Horn clauses 1: SH := {C ∈ S | C is a Horn clause and not a tautology} 2: SH := {C ∈ S | C is a non-Horn clause and not a tautology} 3: repeat 4: Compute all relevant consequences of 〈SH, SH 〉 5: for each relevant consequence C of 〈SH, SH 〉 do 6: Delete from SH and SH all clauses θ-subsumed by C 7: if C is Horn then SH := SH ∪ {C} 8: else SH := SH ∪ {C} 9: until there is no relevant consequence of 〈SH, SH 〉 10: return SH

and non-Horn clauses, respectively; furthermore, the algorithm never resolves two Horn clauses.

Definition 10. Let SH and SH be sets of Horn and non-Horn clauses, respectively. A clause C is a relevant consequence of 〈SH, SH 〉 if

• C is not redundant in SH ∪ SH , and
• C is a factor of a clause C1 ∈ SH , or a resolvent of clauses C1 ∈ SH and C2 ∈ SH ∪ SH.

Theorem 11 recapitulates the algorithm's properties. It essentially shows that, even if the algorithm never terminates, each Horn consequence of S will at some point during algorithm's execution become entailed by the set of Horn clauses SH computed by the algorithm. The theorem was proved by showing that each resolution proof of a consequence of S can be transformed to 'postpone' all resolution steps between two Horn clauses until the end; thus, one can 'precompute' set SH of all consequences of S derivable using a non-Horn clause.

Theorem 11. ([del Val, 2005]) Let S be a set of clauses, and let C be a Horn clause such that S |= C, and assume that Procedure 1 is applied to S. Then, after some finite number of iterations of the loop in lines 3-9, we have SH |= C.

ABox-Independent Compilation

Compiling knowledge into Horn clauses and computing datalog rewritings are similar in spirit: both transform one theory into another while ensuring that the two theories are indistinguishable w.r.t. a certain class of queries. There is, however, an important difference: given a disjunctive program P and a fixed ABox A, one could apply Procedure 1 to S = P ∪ A to obtain a datalog program SH, but such SH would not necessarily be independent from the specific ABox A. In contrast, a rewriting of P is a datalog program PH that can be freely combined with an arbitrary ABox A. We next show that a program PH satisfying the latter requirement can be obtained by applying Procedure 1 to P only.

Towards this goal, we generalise Theorem 11 and show that, when applied to an arbitrary set of first-order clauses N , Procedure 1 computes a set of Horn clauses NH such that the Horn consequences of N ∪A and NH ∪A coincide for an arbitrary ABox A. Intuitively, this shows that, when Procedure 1 is applied to S = N ∪ A, all inferences involving facts in A can be 'moved' to end of derivations.

Theorem 12. Let N be a set of clauses, let A be an ABox, let C be a Horn clause such that N ∪ A |= C, and assume that Procedure 1 is applied to N. Then, after some finite number of iterations of the loop in lines 3-9, we have NH ∪A |= C.

Rewriting Nearly-Monadic Disjunctive Programs

The final obstacle to obtaining a datalog rewriting of a SHITBox T is due to Theorem 6: the rules in ΞT should be applied 'before' ΩT . While this allows us to transformΩT into P = DD(ΩT ) and PH without taking ΞT into account, this also means that Theorems 6, 8, and 12 only imply that the facts entailed by T ∪A and PH ∪ΞT (A) coincide. To obtain a 'true' rewriting, we show in Lemma 13 that program PH is nearly-monadic. We use this observation in Theorem 14 to show that each binary fact obtained by applying PH to ΞT (A) is of the formR(c, c), and so it cannot 'fire' the rules in ΞT ; hence, PH ∪ΞT is a rewriting of T .

Lemma 13. Let P be a nearly-monadic program, and assume that Procedure 1 terminates when applied to P and returns PH. Then, PH is a nearly-monadic datalog program.

Theorem 14. Let P = DD(ΩT ) for T an SHI-TBox. If, when applied to P, Procedure 1 terminates and returns PH, then PH ∪ΞT is a rewriting of T .

Please note that our algorithm (just like all rewriting algorithms we are aware of) computes rewritings using a sound inference system and thus always produces strong rewritings.

Example 15. When applied to the program P = DD(Tex) from Table 2, Procedure 1 resolves C2 and C5 to derive (1), C2 and C6 to derive (2), and C1 and C6 to derive (3).

Resolving (2) and C1, and (3) and C2 produces redundant clauses, after which the procedure terminates and returns the set PH consisting of clauses C3-C6, (2), and (3). By Theorem 14, PH is a strong rewriting of Tex.

4.4 Termination

Procedure 1 is not a semi-decision procedure for either strong non-rewritability (cf. Example 16) or strong rewritability (cf. Example 17) of nearly-monadic programs.

Example 16. Let P be defined as follows.

Clauses (5) and (6) are mutually recursive, but they are also Horn, so Procedure 1 never resolves them directly.

Clauses (5) and (6), however, can interact through clause (4). Resolving (4) and (5) on ¬G(x0) produces (7); and resolving (6) and (7) on B(x1) produces (8). By further resolving (8) alternatively with (5) and (6), we obtain (9) for each even n. By resolving (6) and (9) on B(x0), we obtain (10). Finally, by factoring (10), we obtain (11) for each even n.

Procedure 1 thus derives on P an infinite set of Horn clauses, and Theorem 22 shows that no strong rewriting of P exists.

Example 17. Let P be defined as follows.

When applied to P, Procedure 1 will eventually compute infinitely many clauses Cn of the following form:

However, for each n > 1, clause Cn is a logical consequence of clause C1, so the program consisting of clauses (12), (13), and C1 is a strong rewriting of P.

Example 18 demonstrates another problem that can arise even if P is nearly-monadic and simple.

Example 18. Let P be the following program:

Now resolving (15) and (17) produces (18); and resolving (16) and (18) produces (19).

Clause (19) contains more variables than clauses (15) and (16), which makes bounding the clause size difficult.

Notwithstanding Example 18, we believe one can prove that Procedure 1 terminates if P is nearly-monadic and simple. However, apart frommaking the termination proof more involved, deriving clauses such as (19) is clearly inefficient. We therefore extend Procedure 1 with the condensation simplification rule, which eliminates redundant literals in clauses such as (19). A condensation of a clause C is a clause D with the least number of literals such that D ⊆ C and C subsumes D. A condensation of C is unique up to variable renaming, so we usually speak of the condensation of C. We next show that Theorems 11 and 12 hold even with condensation.

Lemma 19. Theorems 11 and 12 hold if Procedure 1 is modified so that, after line 5, C is replaced with its condensation.

One can prove that all relevant consequences of nearlymonadic and simple clauses are also nearly-monadic and simple, so by using condensation to remove redundant literals, we obtain Lemma 20, which clearly implies Theorem 21.

Lemma 20. If used with condensation, Procedure 1 terminates when applied to a simple nearly-monadic program P.

Theorem 21. Let P = DD(ΩT ) for T a DL-LiteH,+ bool -TBox. Procedure 1 with condensation terminates when applied to P and returns PH; furthermore, PH ∪ ΞT is a rewriting of T .

We thus obtain a tractable (w.r.t. data complexity) procedure for answering queries over DL-LiteH,+ bool -TBoxes. Furthermore, given a ground query Q and a nearly-monadic and simple program PH obtained by Theorem 21, it should be possible to match the NLOGSPACE lower complexity bound by Artale et al. [2009] as follows. First, one should apply backward chaining to Q and PH to compute a UCQ Q′ such that cert(Q,PH, ΞT (A)) = cert(Q′ , ∅, ΞT (A)); since all nearly-monadic rules in PH are simple, it should be possible to show that such 'unfolding' always terminates. Second, one should transform ΞT into an equivalent piecewise-linear datalog program Ξ′T . Although these transformations should be relatively straightforward, a formal proof would require additional machinery and is thus left for future work.

5 Limits to Strong Rewritability

We next show that strong rewritings may not exist for rather simple non-Horn ELU-TBoxes that are rewritable in general. This is interesting because it shows that an algorithm capable of rewriting a larger class of TBoxes necessarily must depart from the common approaches based on sound inferences.

Theorem 22. The ELU-TBox T corresponding to the program P from Example 16 and the ground CQ Q = G(x1) are Q-rewritable, but not strongly Q-rewritable.

The proof of Theorem 22 proceeds as follows. First, we show that, for each ABox A encoding a directed graph, we have cert(Q, T ,A) ̸= ∅ iff the graph contains a pair of vertices reachable by both an even and an odd number of edges. Second, we show that latter property can be decided using a datalog program that uses new relations not occurring in T . Third, we construct an infinite set of rules R entailed by each strong rewriting of T . Fourth, we show that R′ ̸|=R holds for each finite datalog programR′ such that T |=R′ .

Since our procedure from Section 4 produces only strong rewritings, it cannot terminate on a TBox that has no strong rewritings. This is illustrated in Example 16, which shows that Procedure 1 does not terminate when applied to (the clausification of) the TBox from Theorem 22.

6 Outlook

Our work opens many possibilities for future research. On the theoretical side, we will investigate whether one can decide existence of a strong rewriting for a given SHI-TBox T , and to modify Procedure 1 so that termination is guaranteed. Bienvenue et al. [2013] recently showed that rewritability of unary ground queries over ALC-TBoxes is decidable; however, their result does not consider strong rewritability or binary ground queries. On the practical side, we will investigate whether Procedure 1 can be modified to use ordered resolution instead of unrestricted resolution. We will also implement our technique and evaluate its applicability.