We study the problem of rewriting an ontology O1 in a DL L1 into an ontology O2 in a Horn DL L2 such that O1 and O2 are equisatis able when extended with any dataset. After showing undecidability whenever L1 extends ALCF , we focus on devising e ciently checkable conditions that ensure existence of a Horn rewriting. By lifting existing Datalog rewriting techniques for Disjunctive Datalog programs to rstorder programs with function symbols, we identify a class of ontologies that admit Horn rewritings of polynomial size. Our experiments indicate that many real-world ontologies admit such polynomial Horn rewritings.
languages for rewriting are function-free. Kaminski et al. [
Our contributions in this paper are as follows. In Section 3, we show
undecidability of Horn rewritability for ontologies in ALCF . This is in consonance with
the related undecidability results by Bienvenu et al. [
We have implemented markability checking and evaluated our techniques on a large ontology repository. Our results indicate that many real-world ontologies are markable and thus admit Horn rewritings of polynomial size.
All proofs are deferred to an extended version (see arXiv:1504.05150). 2
We assume standard rst-order syntax and semantics. We treat the universal truth > and falsehood ? symbols as well as equality ( ) as ordinary predicates of arity one (> and ?) and two ( ), the meaning of which will be axiomatised. Programs A ( rst-order) rule is a sentence 8x8z:['(x; z) ! (x)] where variables x and z are disjoint, '(x; z) is a conjunction of distinct atoms over x [ y, and (x) is a disjunction of distinct atoms over x. Formula ' is the body of r, and is the head. Quanti ers are omitted for brevity, and safety is assumed T 1: din=1 Ai v Fjm=1 Cj T 2: 9R:A v C T 3: A v 9R:B T 4: A v 8R:C T 5: S v R T 6: A v 1 R:B
Vin=1 Ai(x) ! Wjm=1 Cj(x) at(R; x; y) ^ A(y) ! C(x) A(x) ! at(R; x; f(x)); A(x) ! B(f(x)) A(x) ^ at(R; x; y) ! C(y) S(x; y) ! at(R; x; y) A(z) ^ at(R; z; x1) ^ at(R; z; x2) ^ B(x1) ^ B(x2) ! x1 (all variables in the rule occur in the body). We de ne the following sets of rules for a nite signature : (i) P> consists of a rule P (x1; : : : ; xn) ! >(xi) for each predicate P 2 and each 1 i n and a rule ! >(a) for each constant a 2 ; (ii) P? consists of the rule with ?(x) in the body and an empty head; and (iii) P consists of the standard axiomatisation of as a congruence over . A program is a nite set of rules P = P0 [ P> [ P? [ P with the signature of P0, where we assume w.l.o.g. that the body of each rule in P0 does not mention ? or , and the head is non-empty and does not mention >. We omit for the components of P and write P>, P? and P . A rule is Horn if its head consists of at most one atom, and a program is Horn if so are all of its rules. Finally, a fact is a ground, function-free atom, and a dataset is a nite set of facts. Ontologies A signature consists of disjoint countable sets of concept names
C and role names R. A role is an element of R [ fR j R 2 Rg. The function inv is de ned over roles as follows, where R 2 R: inv(R) = R and inv(R ) = R. W.l.o.g., we consider normalised axioms as on the left-hand side of Table 1. An ALCHIF ontology O is a nite set of axioms of type T1-T6 in Table 1. An ontology is Horn if it contains no axiom T1 where m 2. Given O, we write v for the minimal re exive and transitive relation over roles in O s.t. R1 v R2 and inv(R1) v inv(R2) hold whenever R1 v R2 2 O.
We refer to the DL where only axioms T1{T3 are available and inverse roles are disallowed as E LU . The logic ALC extends E LU with axioms T4. We then use standard naming conventions for DLs based on the presence of inverses (I), axioms T5 (H) and axioms T6 (F ). An ontology is E L if it is E LU and Horn.
Table 1 also provides the standard translation from normalised axioms into rules, where at(R; x; y) stands for R(x; y) if R is named and S(y; x) if R = S . We de ne (O) as the smallest program containing ( ) for each axiom in O. Given a dataset D, we say that O [ D is satis able i so is (O) [ D in FOL. 3
Our focus is on satis ability-preserving rewritings. Standard reasoning tasks
in DLs are reducible to unsatis ability checking [
We are especially interested in computing Horn rewritings of ontologies|
that is, rewritings where the given ontology O1 is expressed in a DL L1 and the
rewritten ontology O2 is in a Horn DL L2 (where preferably L2 L1). This is not
possible in general: satis ability checking is co-NP-complete in data complexity
even for the basic logic E LU [
Our rst result establishes undecidability whenever the input ontology
contains at-most cardinality restrictions and thus equality. This result ts in with
the related undecidability results by Bienvenu et al. [
Intractability results in data complexity rely on the ability of non-Horn DLs
to encode co-NP-hard problems, such as non-3-colourability [
In this section, we introduce the class of markable programs and show that
every markable program can be rewritten into a Horn program by means of a
polynomial transformation, which we refer to as transposition. Roughly speaking,
transposition inverts the rules in a program P by moving certain atoms from head
to body and vice versa while replacing their corresponding predicates with fresh
ones. Markability of P ensures that we can pick a set of predicates (a marking )
such that, by shu ing only atoms with a marked predicate, we obtain a Horn
rewriting of P. Our results in this section generalise the results by Kaminski et
al. [
To illustrate our de nitions throughout this section, we use an example program Pex consisting of the following rules:
A(x) ! B(x) C(x) ! ?(x)
B(x) ! C(x) _ D(x)
D(x) ! C(f (x)) Markability. The notion of markability involves a partitioning of a program's predicates into Horn and disjunctive: the extension of Horn predicates for all datasets depends only on the Horn rules in the program while the extension of disjunctive predicates may depend on a disjunctive rule. This intuition can be formalised using the standard notion of a dependency graph in logic programming. De nition 4. The dependency graph GP = (V; E; ) of a program P is the smallest edge-labeled digraph such that: (i) V contains all predicates in P; (ii) r 2 (P; Q) whenever r 2 P, P is in the body of r, and Q is in the head of r; and (iii) (P; Q) 2 E whenever (P; Q) 6= ;. A predicate Q depends on r 2 P if GP has a path ending in Q and involving an r-labeled edge. Predicate Q is Horn if it depends only on Horn rules; otherwise, Q is disjunctive.
For instance, predicates C, D, and ? are disjunctive in our example program Pex, whereas A and B are Horn. We can now introduce the notion of a marking |a subset of the disjunctive predicates in a program P ensuring that the transposition of P where only marked atoms are shu ed between head and body results in a Horn program.
De nition 5. A marking of a program P is a set M of disjunctive predicates in P satisfying the following properties, where we say that an atom is marked if its predicate is in M : (i) each rule in P has at most one marked body atom; (ii) each rule in P has at most one unmarked head atom; and (iii) if Q 2 M and P is reachable from Q in GP , then P 2 M . A program is markable if it has a marking.
Condition (i) in Def. 5 ensures that at most one atom is moved from body to head during transposition. Condition (ii) ensures that all but possibly one head atom are moved to the body. Finally, condition (iii) requires that all predicates depending on a marked predicate are also marked. We can observe that our example program Pex admits two markings: M1 = fC; ?g and M2 = fC; D; ?g.
Markability can be e ciently checked via a 2-SAT reduction, where we assign to each predicate Q in P a variable XQ and encode the constraints in Def. 5 as 2-clauses. For each rule ' ^ Vin=1 Pi(si) ! Wjm=1 Qj (tj ), with ' the conjunction of all Horn atoms in the head, we include clauses (i) :XPi _ :XPj for all 1 i < j n, which enforce at most one body atom to be marked; (ii) XQi _ XQj for 1 i < j m, which ensure that at most one head atom is unmarked; and (iii) :XPi _ XQj for 1 i n and 1 j m, which close markings under rule dependencies. Each model of the resulting clauses yields a marking of P. Transposition. Before de ning transposition, we illustrate the main intuitions using program Pex and marking M1.
The rst step to transpose Pex is to introduce fresh unary predicates C and ?, which stand for the negation of the marked predicates C and ?. To capture the intended meaning of these predicates, we introduce rules X(x) ! ?(x) for X 2 fA; B; C; Dg and a rule ?(x) ! ?(f (x)) for the unique function symbol f in Pex. The rst rules mimick the usual axiomatisation of > and ensure that an atom ?(c) holds in a Herbrand model of the transposed program whenever X(c) also holds. The last rule ensures that ? holds for all terms in the Herbrand universe of the transposed program|an additional requirement that is consistent with the intended meaning of ?, and critical to the completeness of transposition in the presence of function symbols. Finally, a rule ?(z) ^ C(x) ^ C(x) ! ?(z) ensures that the fresh predicate C behaves like the negation of C.
The key step of transposition is to invert the rules involving the marked predicates by shu ing marked atoms between head and body while replacing their predicate with the corresponding fresh one. In this way, rule B(x) ! C(x)_ D(x) yields B(x) ^ C(x) ! D(x), and C(x) ! ?(x) yields ?(x) ! C(x). Additionally, rule D(x) ! C(f (x)) is transposed as ?(z) ^ D(x) ^ C(f (x)) ! ?(z) to ensure safety. Finally, transposition does not a ect rules containing only Horn predicates, e.g., rule A(x) ! B(x) is included unchanged.
De nition 6. Let M be a marking of a program P. For each disjunctive predicate P in P, let P be a fresh predicate of the same arity. The M -transposition of P is the smallest program M (P) containing every rule in P involving only Horn predicates and all rules given next, where ' is the conjunction of all Horn atoms in a rule, '> is the least conjunction of ?-atoms making a rule safe: 1. 'Q>(t^) ^' ^VVmjm=1 Qj (tj ) ^ Vin=1 P i(si) ! Q(t) for each rule in P of the form ' ^ j=1 Qj (tj ) ! Win=1 Pi(si) where Q(t) is the only marked body atom; 2. ?(x) ^ ' ^ Vm
j=1 Qj (tj ) ^ Vin=1 P i(si) ! ?(x), where x a fresh variable, for each rule in P of the form ' ^ Vjm=1 Qj (tj ) ! Win=1 Pi(si), with no marked body atoms and no unmarked head atoms; 3. ' ^ Vm i=1 P i(si) ! P (s) for each rule in P of the form ' ^ j=1 Qj (tj ) ^ Vn Vm
j=1 Qj (tj ) ! P (s)_Win=1 Pi(si) where P (s) is the only unmarked head atom; 4. ?(z) ^ P (x) ^ P (x) ! ?(z) for marked predicate P ; 5. P (x1; : : : ; xn) ! ?(xi) for each P in P and 1 i n; 6. ?(x1)^: : :^?(xn) ! ?(f (x1; : : : ; xn)) for each n-ary function symbol f in P. Clearly, Pex is unsatis able when extended with fact A(a). To see that M1 (Pex)[ fA(a)g is also unsatis able, note that B(a) is derived by the unchanged rule A(x) ! B(x). Fact C(a) is derived using A(x) ! ?(x) and the transposed rule ?(x) ! C(x). We derive D(a) using B(x) ^ C(x) ! D(x). But then, to derive a contradiction we need to apply rule ?(z) ^ D(x) ^ C(f (x)) ! ?(z), which is not possible unless we derive C(f (a)). For this, we rst use ?(x) ! ?(f (x)), which ensures that ? holds for f (a), and then ?(x) ! C(x).
It follows that every markable set of non-Horn clauses N can be polynomially
transformed into a set of Horn clauses N 0 such that N [ D and N 0 [ D are
equisatis able for every set of facts D. This result is rather general and has
potential applications in rst-order theorem proving, as well as in knowledge
compilation, where Horn clauses are especially relevant [
The notion of markability is applicable to rst-order programs and hence can be seamlessly adapted to ontologies via the standard translation in Table 1. Ontology Oex Rule translation (Oex) Transposition Mex ( (Oex)) Horn DL rewriting 1 A v B t C A(x) ! B(x) _ C(x) A(x) ^ B(x) ! C(x) A u B v C 2 B v 9R:D B(x) ! D(fR;D(x)) D(fR;D(x)) ! B(x) 9RD:D v B 3 9R:D v D R(x; y) ^ D(y) ! D(x) R(x; y) ^ D(x) ! D(y) D v 8R:D D(fR;D(x)) ! D(x) D(x) ! D(fR;D(x)) D v 8RDD
D(fR;B(x)) ! D(x) D(x) ! D(fR;B(x)) D v 8RBD 4 C v 9R:B C(x) ! B(fR;B(x)) ?(z) ^ C(x) ^ B(fR;B(x)) ! ?(z) C u 9RB:B v ? 5 D u E v ? D(x) ^ E(x) ! ?(x) E(x) ^ ?(x) ! D(x) E u ? v D X(x) ! ?(x); X 2 fA; B; C; D; Eg X v ? R(x1; x2) ! ?(xi); 1 i 2 > v 8R:?; 9R:> v ? ?(x) ! ?(fR;Y (x)); Y 2 fB; Dg ? v 9RY :?
This, however, would be of limited value since the Horn programs resulting from transposition may not be expressible in Horn-ALCHIF .
Consider any ontology with an axiom 9R:A v B and any marking M involving R. Rule R(x; y) ^ A(y) ! B(x) stemming from would be transposed as B(x) ^ A(y) ! R(x; y), which cannot be captured in ALCHIF .1
To address this limitation we introduce an alternative translation from DL axioms into rules, which we illustrate using the example ontology Oex in Table 2. The key idea is to encode existential restrictions in axioms T3 as unary atoms over functional terms. For instance, axiom 2 in Oex would yield B(x) ! D(fR;D(x)), where the \successor" relation between an instance b of B and some instance of D in a Herbrand model is encoded as a term fR;D(b), instead of a binary atom of the form R(b; g(b)). This encoding has an immediate impact on markings: by marking B we are only forced to also mark D (rather than both R and D). In this way, we will ensure that markings consist of unary predicates only.
To compensate for the lack of binary atoms involving functional terms in Herbrand models, we introduce new rules when translating axioms T2, T4, and T6 using . For instance, ( 3) yields the following rules in addition to ( 3): a rule D(fR;D(x)) ! D(x) to ensure that all objects c with an R-successor fR;D(c) generated by ( 2) are instances of D; a rule D(fR;B(x)) ! D(x), which makes sure that an object whose R-successor generated by ( 4) is an instance of D is also an instance of D. Finally, axioms 1 and 5, which involve no binary predicates, are translated as usual.
De nition 8. Let O be an ontology. For each concept 9R:B in an axiom of type
T3, let fR;B be a unary function symbol, and the set of all such symbols. We
de ne (O) as the smallest program containing ( ) for each axiom of type
T1{T2 and T4{T6, as well as the following rules:
{ A(x) ! B(fR;B(x)) for each axiom T3;
1 Capturing such a rule would require a DL that can express products of concepts [
finv(R0);Y 2 and R0 v R; { A(x)^Y (fR0;Y (x)) ! C(fR0;Y (x)) for each axiom T4 and R0; Y s.t. fR0;Y 2 and R0 v R; { A(z) ^ B(fR0;Y (z)) ^ at(R; z; x) ^ B(x) ! fR0;Y (z) x for each ax. T6 and
R0; Y s.t. fR0;Y 2 and R0 v R; { A(finv(R0);Y (x)) ^ B(x) ^ at(R; finv(R0);Y (x); y) ^ B(y) ! x y for each axiom
T6 and R0; Y s.t. finv(R0);Y 2 and R0 v R; { A(z) ^ B(fR10;Y1 (z)) ^ B(fR20;Y2 (z)) ! fR10;Y1 (z) fR20;Y2 (z) for each axiom
T6 and fRi0;Yi 2 s.t. Ri0 v R; { A(finv(R10);Y1 (x))^B(x)^B(fR20;Y2 (finv(R10);Y1 (x))) ! x fR20;Y2 (finv(R10);Y1 (x)) for each axiom T6 and Ri0; Yi s.t. ffinv(R10);Y1 ; fR20;Y2 g and Ri0 v R. The translation (Oex) of our example ontology Oex is given in the second column of Table 2. Clearly, Oex is unsatis able when extended with A(a) and E(a). We can check that (Oex) [ fA(a); E(a)g is also unsatis able.
Theorem 9. For every ontology O and dataset D over predicates in O we have that O [ D is satis able i so is (O) [ D.
This translation has a clear bene t for markability checking: in contrast to (O), binary predicates in (O) do not belong to any minimal marking. In particular, Mex = fB; D; ?g is the only minimal marking of (Oex). Proposition 10. (i) If is Horn in (O) then so are all binary predicates in (O). (ii) If (O) is markable, it has a marking containing only unary predicates.
Thus, we de ne markability of ontologies in terms of rather than . We can check that (Oex) is not markable, whereas (Oex) admits the marking Mex.
We conclude this section with the observation that markability of an ontology O can be e ciently checked by rst computing the program (O) and then exploiting the 2-SAT encoding sketched in Section 4. 6
It follows from the correctness of transposition in Theorem 7 and in Theorem 9 that every ALCHIF ontology O admitting a marking M has a Horn rewriting of polynomial size given as the program M ( (O)). In what follows, we show that this rewriting can be expressed within Horn-ALCHIF .
Let us consider the transposition of (Oex) via the marking Mex, which is given in the third column of Table 2. The transposition of 1 and 5 corresponds directly to DL axioms via the standard translation in Table 1. In contrast, the transposition of all other axioms leads to rules that have no direct correspondence in DLs. The following lemma establishes that the latter rules are restricted to the types T7{T20 speci ed on the left-hand side of Table 3.
Lemma 12. Let O be an ontology and M a minimal marking of (O). Then
M ( (O)) contains only Horn rules of type T1{T2 and T4{T6 in Table 1 as well as type T7{T20 in Table 3.
We can now specify a transformation T7{T20 in Table 3 back into DL axioms. that allows us to translate rules De nition 13. We de ne as the transformation mapping (i) each Horn rule r of type T1{T2 and T4{T6 in Table 1 to the DL axiom 1(r) (ii) each rule T7{T20 on the left-hand side of Table 3 to the axioms on the right-hand side.2
Intuitively, works as follows: (i) Function-free rules are \rolled up" as usual into DL axioms (see e.g., T7). (ii) Unary atoms A(fR;Y (x)) with A 6= ? that involve a functional term are translated as existentially or universally quanti ed concepts depending on whether they occur in the body or in the head (e.g., T10, T11); in contrast, atoms ?(fR;Y (x)) in rules ?(x) ! ?(fR;Y (x)) are translated as 9RY :? instead of 8RY :? (T9). (iii) Rules T15{T18, which involve in the head and roles R0 and R in the body, are rolled back into axioms of type T6 over the \union" of R and R0, which is captured using fresh roles and role inclusions.
The ontology obtained by applying to our running example is given in the last column of Table 2. Correctness of and its implications for the computation of Horn rewritings are summarised in the following lemma. 2 For succinctness, axioms resulting from T7, T8, T12, T13, T14, T16 and T18 are not given in normal form.
Lemma 14. Let O be a markable ALCHIF ontology and let M be a marking of O. Then the ontology ( M ( (O))) is a Horn rewriting of O.
A closer look at our transformations reveals that our rewritings do not introduce constructs such as inverse roles and cardinality restrictions if these were not already present in the input ontology. In contrast, fresh role inclusions may originate from cardinality restrictions in the input ontology. As a result, our approach is language-preserving: if the input O1 is in a DL L1 between ALC and ALCHI, then its rewriting O2 stays in the Horn fragment of L1; furthermore, if L1 is between ALCF and ALCIF , then O2 may contain fresh role inclusions (H). A notable exception is when O1 is an E LU ontology, in which case axioms T2 and T3 in O1 may yield axioms of type T4 in O2. The following theorem follows from these observations and Lemma 14.
Theorem 15. Every markable L ontology is polynomially Horn-L rewritable whenever L is between ALC and ALCHI. If L is between ALCF and ALCHIF , every markable L ontology is polynomially rewritable into Horn-LH. Finally, every markable E LU ontology is polynomially rewritable into Horn-ALC.
We conclude by establishing the complexity of satis ability checking over markable ontologies. We rst show that the problem is ExpTime-hard for markable E LU ontologies, which implies that it is not possible to polynomially rewrite every markable E LU ontology into E L. Thus, our rewriting approach is optimal for E LU in the sense that introducing universal restrictions (or equivalently inverse roles) in the rewriting is unavoidable.
Lemma 16. Satis ability checking over markable E LU is ExpTime-hard.
All Horn DLs from ALC to ALCHIF are ExpTime-complete in combined
complexity and PTime-complete in data complexity [
Horn logics are common target languages for knowledge compilation [
Bienvenu et al. [
Gottlob et al. [
Lutz and Wolter [
To assess the practical implications of our results, we have evaluated whether
real-world ontologies are markable (and hence polynomially Horn rewritable).
We analysed 120 non-Horn ontologies extracted from the Protege Ontology
Library, BioPortal (http://bioportal.bioontology.org/), the corpus by Gardiner et
al. [
We found that a total of 32 ontologies were markable and thus rewritable into a Horn ontology, including some ontologies commonly used in applications, such as ChEMBL (see http://www.ebi.ac.uk/rdf/services/chembl/) and BioPAX Reactome (http://www.ebi.ac.uk/rdf/services/reactome/). When using as rstorder logic translation, we obtained 30 markable ontologies|a strict subset of the ontologies markable using . However, only 27 ontologies were rewritable to a Horn DL since in three cases the marking contained a role. 9
We have presented the rst practical technique for rewriting non-Horn ontologies into a Horn DL. Our rewritings are polynomial, and our experiments suggest that they are applicable to widely-used ontologies. We anticipate several directions for future work. First, we would like to conduct an extensive evaluation to assess whether the use of our rewritings can signi cantly speed up satis ability checking in practice. Second, we will investigate relaxations of markability that would allow us to capture a wider range of ontologies.