=Paper=
{{Paper
|id=Vol-1350/paper-25
|storemode=property
|title=Polynomial
Horn Rewritings for Description Logics Ontologies
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-25.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/KaminskiG15
}}
==Polynomial
Horn Rewritings for Description Logics Ontologies==
https://ceur-ws.org/Vol-1350/paper-25.pdf
Polynomial Horn Rewritings for
Description Logics Ontologies?
Mark Kaminski and Bernardo Cuenca Grau
Department of Computer Science, University of Oxford, UK
Abstract. 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 equi-
satisfiable when extended with any dataset. After showing undecidability
whenever L1 extends ALCF, we focus on devising efficiently checkable
conditions that ensure existence of a Horn rewriting. By lifting existing
Datalog rewriting techniques for Disjunctive Datalog programs to first-
order 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.
1 Introduction
Reasoning over ontology-enriched datasets is a key requirement in many appli-
cations. Standard reasoning tasks are, however, of high worst-case complexity.
Satisfiability checking is 2NExpTime-complete for the DL SROIQ underpin-
ning OWL 2 and NExpTime-complete for SHOIN , which underpins OWL
DL [13]. Reasoning is also co-NP-hard in data complexity—a key measure of
complexity for applications involving large amounts of instance data [9].
Tractability in data complexity is typically associated with Horn DLs, where
ontologies correspond to first-order Horn clauses [18, 9]. The more favourable
computational properties of Horn DLs make them a natural choice for data-
intensive applications, but they also come at the expense of a loss in expressive
power. In particular, Horn DLs cannot capture disjunctive axioms, i.e., state-
ments such as “every X is either a Y or a Z”. Disjunctive axioms are common
in real-world ontologies, like the NCI Thesaurus or the ontologies underpinning
the EBI linked data platform (see http://www.ebi.ac.uk/rdf/platform).
In this paper we are interested in Horn rewritability of description logic on-
tologies; that is, whether an ontology O1 in a DL L1 can be restated as an ontol-
ogy O2 in a Horn DL L2 such that O1 and O2 are equisatisfiable when extended
with an arbitrary dataset. Ontologies admitting such rewritings are amenable to
more efficient reasoning techniques that are tractable in data complexity.
Horn rewritability of DL ontologies is strongly related to the rewritability of
Disjunctive Datalog programs into Datalog, where both the source and target
?
Work supported by the Royal Society, the EPSRC projects Score!, MaSI3 and
DBOnto, and the FP7 project Optique.
languages for rewriting are function-free. Kaminski et al. [12] characterised Dat-
alog rewritability of Disjunctive Datalog programs in terms of linearity: a restric-
tion that requires each rule to contain at most one body atom that is IDB (i.e.,
whose predicate also occurs in head position in the program). It was shown that
every linear Disjunctive Datalog program can be rewritten into plain Datalog
(and vice versa) by means of program transposition—a polynomial transforma-
tion in which rules are “inverted” by shuffling all IDB atoms between head and
body while replacing their predicates by auxiliary ones. Subsequently, Kaminski
et al. [11] proposed the class of markable Disjunctive Datalog programs, where
the linearity requirement is relaxed so that it applies only to a subset of “marked”
atoms. Every markable program can be polynomially rewritten into Datalog by
exploiting a variant of transposition where only marked atoms are affected.
Our contributions in this paper are as follows. In Section 3, we show undecid-
ability of Horn rewritability for ontologies in ALCF. This is in consonance with
the related undecidability results by Bienvenu et al. [3] and Lutz and Wolter [17].
In Section 4, we lift the markability condition and the transposition transforma-
tion in [11] for Disjunctive Datalog to first-order programs with function symbols.
We then show that all markable programs admit Horn rewritings of polynomial
size. This result is rather general and has potential implications in areas such
as theorem proving [19] and knowledge compilation [5]. The notion of markabil-
ity for first-order programs easily transfers to ontologies via the standard FOL
translation of DLs [2]. This is, however, of limited practical value since Horn
programs obtained via transposition may not be expressible using standard DL
constructors. In Section 5, we introduce an alternative satisfiability-preserving
translation from ALCHIF ontologies to first-order programs and show in Sec-
tion 6 that the corresponding transposed programs can be translated back into
Horn-ALCHIF ontologies. Finally, we focus on complexity and show that rea-
soning over markable L-ontologies is ExpTime-complete in combined complexity
and PTime-complete w.r.t. data for each DL L between ELU and ALCHIF.
All our results immediately extend to DLs with transitive roles (e.g., SHIF) by
exploiting standard transitivity elimination techniques [2].
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 Preliminaries
We assume standard first-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 (first-order) rule is a sentence ∀x∀z.[ϕ(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. Quantifiers are omitted for brevity, and safety is assumed
dn Fm Vn Wm
T 1. i=1 Ai v j=1 Cj i=1 Ai (x) → j=1 Cj (x)
T 2. ∃R.A v C at(R, x, y) ∧ A(y) → C(x)
T 3. A v ∃R.B A(x) → at(R, x, f (x)); A(x) → B(f (x))
T 4. A v ∀R.C A(x) ∧ at(R, x, y) → C(y)
T 5. SvR S(x, y) → at(R, x, y)
T 6. A v ≤ 1 R.B A(z) ∧ at(R, z, x1 ) ∧ at(R, z, x2 ) ∧ B(x1 ) ∧ B(x2 ) → x1 ≈ x2
Table 1. Normalised DL axioms. A, B are named or >; C named or ⊥; role S is named
and R is a (possibly inverse) role.
(all variables in the rule occur in the body). We define the following sets of rules
>
for a finite signature Σ: (i) PΣ consists of a rule P (x1 , . . . , xn ) → >(xi ) for
each predicate P ∈ Σ and each 1 ≤ i ≤ n and a rule → >(a) for each constant
⊥
a ∈ Σ; (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 finite 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 finite 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 ∪ {R− | R ∈ ΣR }. The
function inv is defined over roles as follows, where R ∈ Σ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 finite 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 reflexive and transitive relation over roles in O s.t.
R1 v∗ R2 and inv(R1 ) v∗ inv(R2 ) hold whenever R1 v R2 ∈ O.
We refer to the DL where only axioms T1–T3 are available and inverse roles
are disallowed as ELU. The logic ALC extends ELU 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 EL if it is ELU 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 define π(O) as the smallest program containing π(α) for each axiom α in O.
Given a dataset D, we say that O ∪ D is satisfiable iff so is π(O) ∪ D in FOL.
3 Horn Rewritability
Our focus is on satisfiability-preserving rewritings. Standard reasoning tasks
in DLs are reducible to unsatisfiability checking [2], which makes our results
practically relevant. We start by formulating our general notion of rewriting.
Definition 1. Let F, F 0 be sets of rules. Then F 0 is a rewriting of F if it holds
that F ∪D is satisfiable iff so is F 0 ∪D for each dataset D over predicates from F.
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: satisfiability checking is co-NP-complete in data complexity
even for the basic logic ELU [14], whereas data complexity is tractable even for
highly expressive Horn languages such as Horn-SROIQ [18]. Horn rewritability
for DLs can be formulated as a decision problem as follows:
Definition 2. The (L1 , L2 )-Horn rewritability problem for DLs L1 and L2 is to
decide whether a given L1 -ontology admits a rewriting expressed in Horn-L2 .
Our first result establishes undecidability whenever the input ontology con-
tains at-most cardinality restrictions and thus equality. This result fits in with
the related undecidability results by Bienvenu et al. [3] and Lutz and Wolter [17]
for Datalog rewritability and non-uniform data complexity for ALCF ontologies.
Theorem 3. (L1 , L2 )-Horn rewritability is undecidable for L1 = ALCF and L2
any DL between ELU and ALCHIF. This result holds if PTime6=NP.
Intractability results in data complexity rely on the ability of non-Horn DLs
to encode co-NP-hard problems, such as non-3-colourability [14, 9]. In practice,
however, it can be expected that ontologies do not encode such problems. Thus,
our focus from now onwards will be on identifying classes of ontologies that
admit (polynomial size) Horn rewritings.
4 Program Markability and Transposition
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 shuffling 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. [11] for Disjunctive Datalog to first-order programs with function symbols.
To illustrate our definitions throughout this section, we use an example pro-
gram Pex consisting of the following rules:
A(x) → B(x) B(x) → C(x) ∨ D(x)
C(x) → ⊥(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 for-
malised using the standard notion of a dependency graph in logic programming.
Definition 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 ∈
µ(P, Q) whenever r ∈ P, P is in the body of r, and Q is in the head of r; and
(iii) (P, Q) ∈ E whenever µ(P, Q) 6= ∅. A predicate Q depends on r ∈ 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 transposi-
tion of P where only marked atoms are shuffled between head and body results
in a Horn program.
Definition 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 ∈ M and P is
reachable from Q in GP , then P ∈ 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 = {C, ⊥} and M2 = {C, D, ⊥}.
Markability can be efficiently checked via a 2-SAT reduction, where we assign
to each predicate Q in P a variable
Vn XQ andWencode the constraints in Def. 5 as
m
2-clauses. For each rule ϕ ∧ i=1 Pi (si ) → j=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 defining transposition, we illustrate the main intuitions
using program Pex and marking M1 .
The first 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 ∈ {A, B, C, D} and a rule ⊥(x) → ⊥(f (x)) for the unique function symbol
f in Pex . The first 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 shuffling 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 affect rules containing only
Horn predicates, e.g., rule A(x) → B(x) is included unchanged.
Definition 6. Let M be a marking of a program P. For each disjunctive pred-
icate 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:
Vm Vn
1. ϕ> ∧ ϕ ∧ j=1 Qj (tj ) ∧ i=1 P i (si ) → Q(t) for each rule in P of the form ϕ ∧
Vm Wn
Q(t) ∧ j=1 Qj (tj ) → i=1 Pi (si ) where Q(t) is the only marked body atom;
Vm Vn
2. ⊥(x) ∧ ϕ ∧ j=1 Qj (tj ) ∧ i=1 P i (si ) → ⊥(x), where x a fresh variable, for
Vm Wn
each rule in P of the form ϕ ∧ j=1 Qj (tj ) → i=1 Pi (si ), with no marked
bodyVatoms and no V unmarked head atoms;
m n
3. ϕ ∧ j=1 Qj (tj ) ∧ i=1 P i (si ) → P (s) for each rule in P of the form ϕ ∧
Vm Wn
j=1 Qj (tj ) → P (s)∨ i=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 unsatisfiable when extended with fact A(a). To see that ΞM1 (Pex )∪
{A(a)} is also unsatisfiable, 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 first use ⊥(x) → ⊥(f (x)),
which ensures that ⊥ holds for f (a), and then ⊥(x) → C(x).
Theorem 7. Let M be a marking of a program P. Then ΞM (P) is a polynomial-
size Horn rewriting of P.
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
equisatisfiable for every set of facts D. This result is rather general and has
potential applications in first-order theorem proving, as well as in knowledge
compilation, where Horn clauses are especially relevant [5, 6].
5 Markability of DL Ontologies
The notion of markability is applicable to first-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) AuB vC
α2 B v ∃R.D B(x) → D(fR,D (x)) D(fR,D (x)) → B(x) ∃RD .D v B
α3 ∃R.D v D R(x, y) ∧ D(y) → D(x) R(x, y) ∧ D(x) → D(y) D v ∀R.D
D(fR,D (x)) → D(x) D(x) → D(fR,D (x)) D v ∀RD D
D(fR,B (x)) → D(x) D(x) → D(fR,B (x)) D v ∀RB D
α4 C v ∃R.B C(x) → B(fR,B (x)) ⊥(z) ∧ C(x) ∧ B(fR,B (x)) → ⊥(z) C u ∃RB .B v ⊥
α5 D u E v ⊥ D(x) ∧ E(x) → ⊥(x) E(x) ∧ ⊥(x) → D(x) Eu⊥vD
X(x) → ⊥(x), X ∈ {A, B, C, D, E} X v⊥
R(x1 , x2 ) → ⊥(xi ), 1 ≤ i ≤ 2 > v ∀R.⊥, ∃R.> v ⊥
⊥(x) → ⊥(fR,Y (x)), Y ∈ {B, D} ⊥ v ∃RY .⊥
Table 2. Rewriting the example ELU ontology Oex into a Horn-ALC ontology using
the marking Mex = {B, D, ⊥}.
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 ∃R.A v B and any marking M involv-
ing 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.
Definition 8. Let O be an ontology. For each concept ∃R.B in an axiom of type
T3, let fR,B be a unary function symbol, and Φ the set of all such symbols. We
define ξ(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 [20].
– A(fR0 ,Y (x)) → C(x) for each axiom T2 and R0 , Y s.t. fR0 ,Y ∈ Φ and R0 v∗ R;
– A(finv(R0 ),Y (x)) → C(x) for each ax. T4 and R0 , Y s.t. finv(R0 ),Y ∈ Φ, R0 v∗ R;
– A(x) ∧ Y (finv(R0 ),Y (x)) → C(finv(R0 ),Y (x)) for each axiom T2 and R0 , Y s.t.
finv(R0 ),Y ∈ Φ 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 ∈ Φ
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 ∈ Φ 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 ∈ Φ 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 ∈ Φ 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. {finv(R10 ),Y1 , fR20 ,Y2 } ⊆ Φ and Ri0 v∗ R.
The translation ξ(Oex ) of our example ontology Oex is given in the second column
of Table 2. Clearly, Oex is unsatisfiable when extended with A(a) and E(a). We
can check that ξ(Oex ) ∪ {A(a), E(a)} is also unsatisfiable.
Theorem 9. For every ontology O and dataset D over predicates in O we have
that O ∪ D is satisfiable iff so is ξ(O) ∪ D.
This translation has a clear benefit for markability checking: in contrast to
π(O), binary predicates in ξ(O) do not belong to any minimal marking. In
particular, Mex = {B, D, ⊥} 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 define markability of ontologies in terms of ξ rather than π. We can
check that π(Oex ) is not markable, whereas ξ(Oex ) admits the marking Mex .
Definition 11. An ontology O is markable if so is ξ(O).
We conclude this section with the observation that markability of an ontology
O can be efficiently checked by first computing the program ξ(O) and then
exploiting the 2-SAT encoding sketched in Section 4.
6 Rewriting Markable Ontologies
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 specified on the left-hand side of Table 3.
T 7. ⊥(z) ∧ B(x) ∧ R(x, y) ∧ A(y) → ⊥(z) B u ∃R.A v ⊥
T 8. ⊥(z) ∧ A(fR,Y (x)) ∧ B(x) → ⊥(z) B u ∃RY .A v ⊥
T 9. ⊥(x) → ⊥(fR,Y (x)) ⊥ v ∃RY .⊥
T 10. B(x) → A(fR,Y (x)) B v ∀RY .A if A 6= ⊥ or B 6= ⊥
T 11. B(fR,Y (x)) → A(x) ∃RY .B v A
T 12. A(x) ∧ B(fR,Y (x)) → C(fR,Y (x)) A u ∃RY .B v ∀RY .C
T 13. ⊥(z) ∧ A(x) ∧ B(fR,Y (x)) ∧ C(fR,Y (x)) → ⊥(z) A u ∃RY (B u C) v ⊥
T 14. B(fR,Y (x)) ∧ C(fR,Y (x)) → A(x) ∃RY (B u C) v A
0
T 15. A(z) ∧ B(fR0 ,Y (z)) ∧ at(R, z, x) ∧ B(x) RY v S{R0 ,R} , R v S{R0 ,R} ,
Y Y
→ fR0 ,Y (z) ≈ x A v ≤1S{R0 ,R} .B
Y
0
T 16. A(fR0 ,Y (x)) ∧ B(x) ∧ at(R, fR0 ,Y (x), y) ∧ B(y) R̃Y v S{R̃0 ,R} , R v S{R̃0 ,R} ,
Y Y
0 0
→x≈y A v ≤1S{R̃0 ,R} .B, R̃Y ≡ inv(RY )
Y
0
T 17. A(z) ∧ B(fR,Y (z)) ∧ B(fR0 ,Z (z)) RY v S{R 0 , RZ v S{R ,R0 } ,
Y ,RZ } Y Z
→ fR,Y (z) ≈ fR0 ,Z (z) A v ≤1S{R 0 .B
Y ,RZ }
0
T 18. A(fR,Y (x)) ∧ B(x) ∧ B(fR0 ,Z (fR,Y (x))) R̃Y v S{R̃ 0 , RZ v S{R̃ 0 ,
Y ,RZ } Y ,RZ }
→ x ≈ fR0 ,Z (fR,Y (x)) A v ≤1S{R̃ 0 .B, R̃Y ≡ inv(RY )
Y ,RZ }
T 19. R(x, y) → ⊥(x) ∃R.> v ⊥
T 20. R(x, y) → ⊥(y) > v ∀R.⊥
Table 3. Transformation Ψ from transposed rules to DLs. Role names R̃ are fresh for
every R, and S{R,R0 } for every {R, R0 }.
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 Ψ that allows us to translate rules
T7–T20 in Table 3 back into DL axioms.
Definition 13. We define Ψ 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 quantified
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 ∃RY .⊥ instead of ∀RY .⊥ (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 in-
troduce 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 ap-
proach 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 ELU 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 ELU ontology is polynomially rewritable into Horn-ALC.
We conclude by establishing the complexity of satisfiability checking over
markable ontologies. We first show that the problem is ExpTime-hard for mark-
able ELU ontologies, which implies that it is not possible to polynomially rewrite
every markable ELU ontology into EL. Thus, our rewriting approach is optimal
for ELU in the sense that introducing universal restrictions (or equivalently in-
verse roles) in the rewriting is unavoidable.
Lemma 16. Satisfiability checking over markable ELU is ExpTime-hard.
All Horn DLs from ALC to ALCHIF are ExpTime-complete in combined
complexity and PTime-complete in data complexity [15]. By Theorem 15, the
same holds for markable ontologies in DLs from ALC to ALCHIF. Finally,
Lemma 16 shows that these results extend to markable ELU ontologies.
Theorem 17. Let L be in-between ELU and ALCHIF. Satisfiability checking
over markable L-ontologies is ExpTime-complete and PTime-complete in data.
7 Related Work
Horn logics are common target languages for knowledge compilation [5]. Selman
and Kautz [21] proposed an algorithm for compiling a set of propositional clauses
into a set of Horn clauses s.t. their Horn consequences coincide. This approach
was generalised to FOL by Del Val [6], without termination guarantees.
Bienvenu et al. [3] showed undecidability of Datalog rewritability for ALCF
and decidability in NExpTime for SHI. Cuenca Grau et al. [4] and Kamin-
ski et al. [11] proposed practical techniques for computing Datalog rewritings
of SHI ontologies based on a two-step process. First, O is rewritten using a
resolution calculus Ω into a Disjunctive Datalog program Ω(O) of exponential
size [10]. Second, Ω(O) is rewritten into a Datalog program P. For the second
step, Kaminski et al. [11] propose the notion of markability of a Disjunctive Dat-
alog program and show that P can be polynomially computed from Ω(O) using
transposition whenever Ω(O) is markable. In contrast to our work, Kaminski
et al. [11] focus on Datalog as target language for rewriting (rather than Horn
DLs). Furthermore, their Datalog rewritings may be exponential w.r.t. the input
ontology and cannot generally be represented in DLs.
Gottlob et al. [8] showed tractability in data complexity of fact entailment
for the class of first-order rules with single-atom bodies, which is sufficient to
capture most DLs in the DL-Litebool family [1].
Lutz and Wolter [17] investigated (non-uniform) data complexity of query
answering w.r.t. fixed ontologies. They studied the boundary of PTime and
co-NP-hardness and established a connection with constraint satisfaction prob-
lems. Finally, Lutz et al. [16] studied model-theoretic rewritability of ontologies
in a DL L1 into a fragment L2 of L1 . These rewritings are equivalence-preserving;
this is in contrast to our approach, which requires only satisfiability preservation.
8 Proof of Concept
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 Li-
brary, BioPortal (http://bioportal.bioontology.org/), the corpus by Gardiner et
al. [7], and the EBI linked data platform (http://www.ebi.ac.uk/rdf/platform).
To check markability, we have implemented the 2-SAT reduction in Section 4
and a simple 2-SAT solver.
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 Re-
actome (http://www.ebi.ac.uk/rdf/services/reactome/). When using π as first-
order 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 Conclusion and Future Work
We have presented the first 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 significantly speed up satisfiability checking
in practice. Second, we will investigate relaxations of markability that would
allow us to capture a wider range of ontologies.
References
1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family
and relations. J. Artif. Intell. Res. 36, 1–69 (2009)
2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.: The
Description Logic Handbook: Theory, Implementation, and Applications. Cam-
bridge University Press (2003)
3. Bienvenu, M., ten Cate, B., Lutz, C., Wolter, F.: Ontology-based data access: A
study through disjunctive datalog, CSP, and MMSNP. ACM Tans. Database Syst.
39(4), 33 (2014)
4. Cuenca Grau, B., Motik, B., Stoilos, G., Horrocks, I.: Computing datalog rewritings
beyond Horn ontologies. In: IJCAI. pp. 832–838 (2013)
5. Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17,
229–264 (2002)
6. Del Val, A.: First order LUB approximations: Characterization and algorithms.
Artif. Intell. 162(1-2), 7–48 (2005)
7. Gardiner, T., Tsarkov, D., Horrocks, I.: Framework for an automated comparison
of description logic reasoners. In: ISWC. pp. 654–667 (2006)
8. Gottlob, G., Manna, M., Morak, M., Pieris, A.: On the complexity of ontological
reasoning under disjunctive existential rules. In: MFCS. pp. 1–18 (2012)
9. Hustadt, U., Motik, B., Sattler, U.: Data complexity of reasoning in very expressive
description logics. In: IJCAI. pp. 466–471 (2005)
10. Hustadt, U., Motik, B., Sattler, U.: Reasoning in description logics by a reduction
to disjunctive datalog. J. Autom. Reasoning 39(3), 351–384 (2007)
11. Kaminski, M., Nenov, Y., Cuenca Grau, B.: Computing datalog rewritings for
disjunctive datalog programs and description logic ontologies. In: RR. pp. 76–91
(2014)
12. Kaminski, M., Nenov, Y., Cuenca Grau, B.: Datalog rewritability of disjunctive
datalog programs and its applications to ontology reasoning. In: AAAI. pp. 1077–
1083 (2014)
13. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: KR. pp. 274–284 (2008)
14. Krisnadhi, A., Lutz, C.: Data complexity in the EL family of description logics.
In: LPAR. pp. 333–347 (2007)
15. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of Horn description logics.
ACM Trans. Comput. Log. 14(1) (2013)
16. Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: Model-theoretic charac-
terizations and rewritability. In: IJCAI. pp. 983–988 (2011)
17. Lutz, C., Wolter, F.: Non-uniform data complexity of query answering in descrip-
tion logics. In: KR. pp. 297–307 (2012)
18. Ortiz, M., Rudolph, S., Simkus, M.: Query answering in the Horn fragments of the
description logics SHOIQ and SROIQ. In: IJCAI. pp. 1039–1044 (2011)
19. Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier
(2001)
20. Rudolph, S., Krötzsch, M., Hitzler, P.: All elephants are bigger than all mice. In:
DL (2008)
21. Selman, B., Kautz, H.: Knowledge compilation and theory approximation. J. ACM
43(2), 193–224 (1996)