=Paper=
{{Paper
|id=Vol-1350/paper-29
|storemode=property
|title=Conservative
Rewritability of Description Logic TBoxes: First Results
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-29.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/KonevLWZ15
}}
==Conservative
Rewritability of Description Logic TBoxes: First Results==
https://ceur-ws.org/Vol-1350/paper-29.pdf
Conservative Rewritability of Description Logic
TBoxes: First Results
Boris Konev1 , Carsten Lutz2 , Frank Wolter1 , and Michael Zakharyaschev3
1
Department of Computer Science, University of Liverpool, U.K.
2
Fachbereich Informatik, Universität Bremen, Germany
3
Department of Computer Science and Information Systems, Birkbeck, University of
London, U.K.
Abstract. We want to understand when a given TBox T in a descrip-
tion logic L can be rewritten into a TBox T 0 in a weaker description
logic L0 . Two notions of rewritability are considered: model-conservative
rewritability (T 0 entails T and all models of T can be expanded to
models of T 0 ) and L-conservative rewritability (T 0 entails T and ev-
ery L-consequence of T 0 in the signature of T is a consequence of T )
and investigate rewritability of TBoxes in ALCI to ALC, ALCQ to
ALC, ALC to EL⊥ , and ALCI to DL-Litehorn . We compare conservative
rewritability with equivalent rewritability, give model-theoretic charac-
terizations of conservative rewritability, prove complexity results for de-
ciding rewritability, and provide some rewriting algorithms.
Over the past 30 years, a multitude of different description logics (DLs) have
been designed, investigated, and used in practice as ontology languages. The
introduction of new DLs has been driven both by the need for additional ex-
pressive power (such as transitive roles in the 1990s) and by applications that
require efficient reasoning of a novel type (such as ontology-based data access in
the 2000s). While the resulting flexibility in choosing DLs has had the positive
effect of making DLs available for a large number of domains and applications,
it has also led to the development of ontologies with language constructors that
are not really required to axiomatize their knowledge. For a constructor to be
‘not required’ can mean different things here, ranging from the high-level ‘this
domain can be represented in an adequate way in a weaker DL’ to the very
concrete ‘this ontology is logically equivalent to an ontology in a weaker DL’. In
this paper, we take the latter understanding as our starting point. Equivalent
rewritability of a given DL ontology (TBox) to a weaker DL has been inves-
tigated in [17], where model-theoretic characterizations and the complexity of
deciding rewritability were investigated. For example, equivalent rewritability of
an ALC TBox to an EL⊥ TBox has been characterized in terms of preservation
under products and global equisimilations, and a NExpTime upper bound for
deciding equivalent rewritability has been established. Equivalent rewritability
is a very strong notion, however, that appears to apply to a very small num-
ber of real-world TBoxes. A more practically relevant notion we propose in this
paper is conservative rewritability, which allows one to use new concept and
role names when rewriting a given ontology into a weaker DL. In this case, we
clearly cannot demand that the new TBox is logically equivalent to the original
one, but only that it entails the original TBox. To avoid uncontrolled additional
consequences of the new TBox, we can also require that (i ) it does not entail any
new consequences in the language of the original TBox, or even that (ii ) every
model of the original TBox can be expanded a model of the new TBox. The lat-
ter type of conservative extension is known as model-conservative extension [16],
and we call a TBox T model-conservatively L-rewritable if a model-conservative
rewriting of T in the DL L exists. The former type of conservative extension
is known as a language-conservative extension or deductive conservative exten-
sion [12] and, given a DL L in which T is formulated and a weaker DL L0 , we
call T L-conservatively L0 -rewritable if there is a TBox T 0 in L0 such that T 0
has the same L-consequences as T in the signature of T . Model-conservative
rewritability is the more robust notion as it is language-independent and does
not only leave unchanged the entailed concept inclusions of the original TBox
but also, for example, certain answers if the ontologies are used to access data.
The main result of this paper is that there are important DLs for which
model-conservative and L-conservative rewritability can be transparently char-
acterized, effectively decided, and for which rewriting algorithms can be de-
signed. This is in contrast to the undecidability of the problem whether one
TBox is a model-conservative extension of another one even for weak DLs such
as EL [18, 16]. In particular, we show that, given an ALCI TBox, one can com-
pute in polynomial time its model-conservative ALC-rewriting provided that
such a rewriting exists, which can be decided in ExpTime. We characterize
model-conservative ALC-rewritability in terms of preservation under generated
subinterpretations and show that ALCI-conservative ALC-rewritability coin-
cides with model-conservative one. For ALCQ TBoxes, we show that model-
conservative ALC-rewritability coincides with equivalent rewritability, but is
different from ALCQ-conservative rewritability. The latter can be characterized
using bounded morphisms, and all these notions of rewritability are decidable
in 2ExpTime. Unlike the ALCI case, we currently do not have polynomial
rewritings for ALCQ TBoxes. As to rewritability from ALCI to DL-Litehorn ,
we observe that all our notions of rewritability coincide and are ExpTime-
complete. In contrast, for rewritability from ALC to EL⊥ they are all distinct
and, in fact, rather intricate and difficult to analyse. We prove decidability of
model-conservative rewritability and give necessary semantic conditions for both
ALC-conservative and model-conservative EL⊥ -rewritability.
Related work. Conservative rewritings of TBoxes are ubiquitous in the DL
research. For example, many rewritings of TBoxes into normal forms are model-
conservative [14, 4]. Regarding rewritability of TBoxes into weaker DLs, the fo-
cus has been on polynomial satisfability preserving rewritings as a pre-processing
step to reasoning [11, 9, 8] or to prove complexity results for reasoning [10]. Such
rewritings are mostly not conservative. There has been significant work on rewrit-
ings of ontology-mediated queries (pairs of ontologies and queries), which pre-
serve their certain answers, into datalog or ontology-mediated queries based on
weaker DLs [13, 5]. It seems, however, that this problem is different from TBox
conservative rewritability. In [2], the expressive power of DLs and corresponding
notions of rewritability are introduced based on a variant of model-conservative
extension, and the relationship to L-conservative extensions is discussed.
For omitted proofs, see http://cgi.csc.liv.ac.uk/∼ frank/publ/publ.html.
1 Conservative Rewritability
We consider the standard description logics ALC, ALCI, ALCQ, EL⊥ , and
DL-Litehorn [3, 4, 7, 1], where EL⊥ is EL extended with the concept ⊥, and
DL-Litehorn is DL-Litecore extended with conjunctions of basic concepts on the
left-hand side of concept inclusions. As usual, the alphabet of DLs consists of
countably infinite sets NC of concept names and NR of role names. By a signa-
ture, Σ, we mean any set of concept and role names. The signature sig(T ) of a
TBox T is the set of concept and role names occurring in T .
Before introducing our notions of conservative rewritability, we remind the
reader of a simpler notion of TBox rewritability. Suppose L and L0 are DLs; we
typically assume that L is more expressive than L0 .
Definition 1 (equivalent L-to-L0 rewritability). An L0 TBox T 0 is called
an equivalent L0 -rewriting of an L TBox T if T |= T 0 and T 0 |= T (in other
words, if T and T 0 have the same models). An L TBox is called equivalently
L0 -rewritable if it has an equivalent L0 -rewriting.
Equivalent L-to-L0 rewritability has been studied in [17], where semantic
characterizations are given and complexity results for deciding equivalent re-
writability are obtained for various DLs L and L0 . For example, if L is ALCI or
ALCQ and L0 is ALC, then an L TBox T is equivalently L0 -rewritable just in
case its class of models is preserved under global bisimulations, which are defined
as follows. Given interpretations Ii = (∆Ii , ·Ii ), for i = 1, 2, and a signature Σ,
we call a relation S ⊆ ∆I1 × ∆I2 a Σ-bisimulation between I1 and I2 if
– for any A ∈ Σ, whenever (d1 , d2 ) ∈ S then d1 ∈ AI1 iff d2 ∈ AI2 ;
– for any r ∈ Σ and (d1 , d2 ) ∈ S,
if (d1 , e1 ) ∈ rI1 then there is e2 such that (e1 , e2 ) ∈ S and (d2 , e2 ) ∈ rI2 ,
if (d2 , e2 ) ∈ rI2 then there is e1 such that (e1 , e2 ) ∈ S and (d1 , e1 ) ∈ rI1 .
S is a global Σ-bisimulation between I1 and I2 if ∆I1 is the domain of S and ∆I2
its range. I1 and I2 are globally Σ-bisimilar if there is a global Σ-bisimulation
I1
between them, in which case we write I1 ∼Σ ALC I2 . For d1 ∈ ∆ and d2 ∈ ∆I2 ,
we say that (I1 , d1 ) is Σ-bisimilar to (I2 , d2 ) if there is a Σ-bisimulation S
between I1 and I2 such that (d1 , d2 ) ∈ S. If Σ = NC ∪ NR , we omit Σ, write
I1 ∼ALC I2 and say simply ‘(global) bisimulation.’
Example 1. The ALCI TBox {∃r− .B v A} can be equivalently rewritten to the
ALC TBox {B v ∀r.A}. However, the ALCI TBox T = {∃r− .B u ∃s− .B v A}
is not equivalently ALC-rewritable. Indeed, the interpretation on the right-hand
side in the picture below is a model of T and globally bisimilar to the interpre-
tation on the left-hand side, which is not a model of T .
r s r s
B B B B
We now introduce two subtler notions of TBox rewritability, which allow the
use of fresh concept and role names in rewritings. For an interpretation I and
signature Σ, the Σ-reduct of I is the interpretation I|Σ coinciding with I on the
names in Σ and having X I|Σ = ∅ for all X ∈ / Σ. We say that interpretations I
and J coincide on Σ and write I =Σ J if the Σ-reducts of I and J coincide. A
TBox T 0 is a model-conservative extension of T if an interpretation I is a model
of T just in case there is a model I 0 of T 0 such that I =sig(T ) I 0 .
Definition 2 (model-conservative L-to-L0 -rewritability). An L0 TBox T 0
is called a model-conservative L0 -rewriting of an L TBox T if T 0 is a model-
conservative extension of T . An L TBox T is model-conservatively L0 -rewritable
if a model-conservative L0 -rewriting of T exists.
Clearly, any equivalent L0 -rewriting of a TBox T is also a model-conservative
L0 -rewriting of T . The next example shows that the converse does not hold.
Example 2. The ALCI TBox T = {∃r− .B u ∃s− .B v A} from Example 1 is
model-conservatively ALC-rewritable to
T 0 = {B v ∀r.B∃r− .B , B v ∀s.B∃s− .B , B∃r− .B u B∃s− .B v A},
where B∃r− .B , B∃s− .B are fresh concept names.
A TBox T 0 is called an L-conservative extension of T if T 0 |= T and T 0 |= C v D
implies T |= C v D, for every L-concept inclusion C v D formulated in sig(T ).
Definition 3 (L-conservative L0 -rewritability). An L0 TBox T 0 is called an
L-conservative L0 -rewriting of an L TBox T if T 0 is an L-conservative extension
of T . An L TBox T is L-conservatively L0 -rewritable if an L-conservative L0 -
rewriting of T exists.
It should be clear that every model-conservative L0 -rewriting of an L TBox T
is also an L-conservative L0 -rewriting of T . The next example shows that the
converse implication does not hold.
Example 3. The ALCQ TBox T = {A v ≥ 2 r.B} is ALCQ-conservatively ALC-
rewritable to T 0 = {A v ∃r.C, A v ∃r.D, C v ¬D, C t D v B}, where C and
D are fresh concept names. However, T 0 is not a model-conservative rewriting
of T because the model of T shown below is not the sig(T )-reduct of any model
of T 0 . Note that T is not equivalently ALC-rewritable.
B B B
r r
r r
A A A
In our examples so far, we have used fresh concept names but no fresh role names.
This is no accident: it turns out that, for the DLs considered in this paper, fresh
role names in conservative rewritings are not required. More precisely, we call a
model-conservative or L-conservative L0 -rewriting T 0 of T a model-conservative
or, respectively, L-conservative L0 -concept rewriting of T if sigR (T ) = sigR (T 0 ),
where sigR (T ) is the set of role names in T .
S L reflects disjoint unions if, for any L TBox T , whenever the
Say that a DL
disjoint union i∈I Ii of interpretations Ii is a model of T , then each Ii , i ∈ I,
is also a model of T . All the DLs considered in this paper reflect disjoint unions.
Theorem 1. Let L be a DL reflecting disjoint unions, T an L TBox, and let
L0 ∈ {ALC, EL⊥ , DL-Litehorn }. Then T is model-conservatively (or L-conserva-
tively) L0 -rewritable if and only if it is model-conservatively (or, respectively,
L-conservatively) L0 -concept rewritable.
2 ALCI-to-ALC Rewritability
Equivalent ALCI-to-ALC rewritability was studied in [17], where the characteri-
zation in terms of global bisimulations was used to design a 2ExpTime algorithm
for checking this property. Here, we give a characterization of model-conservative
ALC rewritability of ALCI TBoxes in terms of generated subinterpretations
and use it to show that (i ) model-conservative ALCI-to-ALC rewritings are of
polynomial size and can be constructed in polynomial time (if they exist), and
that (ii ) deciding model-conservative ALCI-to-ALC rewritability is ExpTime-
complete. We also observe that ALCI-conservative ALC-rewritability coincides
with model-conservative rewritability.
We remind the reader that an interpretation I is a subinterpretation of an
interpretation J if ∆I ⊆ ∆J , AI = AJ ∩ ∆I for all concept names A, and
rI = rJ ∩ (∆I × ∆I ) for all role names r. I is a generated subinterpretation of J
if, in addition, whenever d ∈ ∆I and (d, d0 ) ∈ rJ , r a role name, then d0 ∈ ∆I .
We say that a TBox T is preserved under generated subinterpretations if every
generated subinterpretation of a model of T is also a model of T . As well known,
every ALC TBox is preserved under generated subinterpretations.
Suppose we want to find a model-conservative ALC-rewriting of an ALCI
TBox T . Without loss of generality, we assume that T = {> v CT } and CT
is built using ¬, u and ∃ only. Let sub(T ) be the closure under single negation
of the set of (subconcepts) of concepts in T . For every role name r in T , we
take a fresh role name r̄ and, for every ∃r.C in sub(T ) (where r is a role name
or its inverse), we take a fresh concept name B∃r.C . Denote by D] the ALC-
concept obtained from any D ∈ sub(T ) by replacing every top-most occurrence
of a subconcept of the form ∃r.C in it with B∃r.C . Now, let T † be an ALC TBox
comprised of the following concept inclusions, for r ∈ NR : > v CT] ,
C ] v ∀r̄.B∃r.C , B∃r.C ≡ ∃r.C ] , for every ∃r.C ∈ sub(T ),
]
C v ∀r.B∃r− .C , ]
B∃r− .C ≡ ∃r̄.C , for every ∃r− .C ∈ sub(T ).
Clearly, T † can be constructed in polynomial time in the size of T .
Theorem 2. An ALCI TBox T is model-conservatively ALC-rewritable iff T
is preserved generated subinterpretations. Moreover, if T is model-conservatively
ALC-rewritable, then T † is its model-conservative ALC-rewriting.
It is now easy to show that model-conservative ALCI-to-ALC rewritability is
decidable in ExpTime. By Theorem 2, this amounts to deciding whether T † is
a model-conservative extension of T . In general, this is an undecidable problem.
It is, however, easy to see that, for every model I of T , there is a model I 0 of T †
such that I =sig(T ) I 0 . It thus remains to decide whether every interpretation I
with I =sig(T ) I 0 , for some model I 0 of T † , is a model of T . In other words, this
means to decide whether T † |= T , which can be done in ExpTime. A matching
lower bound is easily obtained by reducing satisfiability in ALC.
Corollary 1. The problem of deciding model-conservative ALCI-to-ALC rewri-
tability is ExpTime-complete.
ALCI-conservative ALC-rewritability of ALCI TBoxes coincides with model-
conservative ALC-rewritability. This can be proved using the characterization
via subinterpretations and robustness under replacement of ALCI TBoxes, an
important property in the context of modular ontology design [15, Theorem 4].
Theorem 3. An ALCI TBox T is ALCI-conservatively ALC-rewritable iff T
is model-conservatively ALC-rewritable.
3 ALCQ-to-ALC Rewritability
Equivalent ALCQ-to-ALC rewritability was characterized in [17] in terms of
preservation under global bisimulations. Below, we use this characterization to
give a 2ExpTime algorithm for checking equivalent ALC-rewritability.
We first prove a characterization of ALCQ-conservative ALC-rewritability
in terms of preservation under inverse bounded morphisms and use it to show
that one can (i ) decide ALCQ-conservative ALC-rewritability in 2ExpTime
and (ii ) construct effectively an ALCQ-conservative rewriting if it exists. We
also show that, unlike ALCI-to-ALC-rewritability, model-conservative ALC-
rewritability of ALCQ TBoxes coincides with equivalent rewritability.
A bounded Σ-morphism from an interpretation I1 to an interpretation I2 is
a global Σ-bisimulation S between I1 and I2 such that S is a function from
∆I1 to ∆I2 . A class K of interpretations is preserved under inverse bounded Σ-
morphisms if whenever there is a bounded Σ-morphism from an interpretation
I1 to some I2 ∈ K, then I1 ∈ K. The following lemma provides the fundamental
property of bounded morphisms:
Lemma 1. Suppose f : I1 → I2 is a bounded Σ-morphism, where I2 is a model
of an ALC TBox T and sigR (T ) ⊆ Σ. Then there is J1 |= T such that J1 =Σ I1 .
Proof. We define J1 in the same way as I1 except that B J1 := f −1 (B I2 ) for
all concept names B ∈ sig(T1 ) \ Σ. Then f is a bounded sig(T )-morphism from
J1 to I2 . Thus, J1 is a model of T since I1 is a model of T . o
An interpretation I is a directed tree interpretation if rI ∩ sI = ∅, for r 6= s, and
the directed
S graph with nodes ∆I and edges E defined by setting (d, d0 ) ∈ E iff
0 I
(d, d ) ∈ r∈NR r is a directed tree. We start our investigation with the obser-
vation that ALCQ-conservative ALCQ-to-ALC rewritability can be regarded as
a principled approximation of model-conservative rewritability:
Lemma 2. An ALC TBox T 0 is an ALCQ-conservative rewriting of an ALCQ
TBox T iff T 0 is a model-conservative rewriting of T over the class of directed
tree interpretations of finite outdegree.
Suppose we want to find an ALCQ-conservative ALC-rewriting of an ALCQ
TBox T . Without loss of generality, we assume that T is of the form {> v CT }
and that CT is built using ¬, u, (> n r C) only. Construct a TBox T † as follows.
Take fresh concept names BD , B1D , . . . , BnD for every D = (> n r C) ∈ sub(T ).
We use Σ to denote sig(T ) extended with all fresh concept names of the form
BiD . For each C ∈ sub(T ), C ] denotes the ALC-concept that results from C by
replacing all top-most occurrences of any D = (> n r C) in T with BD . Now,
define T † to be the infinite TBox that consists of the following inclusions:
– > v CT] ,
– BD v ∃r.(C ] u B1D ) u · · · u ∃r.(C ] u BnD ),
– BiD v ¬BjD , for i 6= j, and
– for all ALC-concepts C1 , . . . , Cn in Σ and all D = (> n r C) ∈ sub(T ),
u (∃r.(C ] u Ci] u j6u
1≤i≤n =i
¬Cj] )) v BD .
The next theorem characterizes ALCQ-conservative ALC-rewritability.
Theorem 4. An ALCQ TBox T is ALCQ-conservatively ALC-rewritable iff T
is preserved under inverse bounded sig(T )-morphisms. Moreover, if T is ALCQ-
conservatively ALC-rewritable, then T † is an (infinite) rewriting.
The semantic characterization of Theorem 4 can be employed to prove the fol-
lowing complexity result using a type elimination argument. We assume that
numbers in number restrictions are given in unary.
Theorem 5. For ALCQ TBoxes, ALCQ-conservative ALC-rewritability is de-
cidable in 2 ExpTime.
It follows that, given an ALCQ TBox T , one can first decide ALCQ-conservative
ALC-rewritability and then, in case of a positive answer, effectively construct a
rewriting by going through the finite subsets of T † in a systematic way until a
finite T 0 ⊆ T † with T 0 |= T is reached. By compactness, such a set T 0 exists.
We finally show that every model-conservatively ALC-rewritable ALCQ TBox
is equivalently ALC-rewritable.
Theorem 6. An ALCQ TBox is model-conservatively ALC-rewritable iff it is
equivalently ALC-rewritable, which is decidable in 2 ExpTime.
4 ALCI-to-DL-Litehorn and ALC-to-EL⊥ Rewritability
We first observe that all notions of rewritability introduced in this paper coin-
cide in the case of ALCI-to-DL-Litehorn rewritability. Deciding rewritability is
ExpTime-complete in all cases since deciding equivalent ALCI-to-DL-Litehorn
rewritability is ExpTime-complete [17]:
Theorem 7. For ALCI TBoxes, equivalent DL-Litehorn -rewritability, model-
conservative DL-Litehorn -rewritability, and ALCI-conservative DL-Litehorn -rew-
ritability coincide and are ExpTime-complete.
We now provide separating examples for all three notions of ALC-to-EL⊥ re-
writability and then prove decidability of model-conservative EL⊥ -rewritability.
While we have not yet been able to find purely model-theoretic characteriza-
tions of model- and ALC-conservative EL⊥ -rewritability, we then give necessary
model-theoretic conditions for these two notions of rewritability.
Equivalent ALC-to-EL⊥ rewritability has been characterized in [17] in terms
of preservation under products and global equisimulations. A simulation between
interpretations I and J is a relation S ⊆ ∆I × ∆J such that, for any A ∈ NC ,
r ∈ NR and (d1 , d2 ) ∈ S, if d1 ∈ AI1 then d2 ∈ AI2 , and if (d1 , e1 ) ∈ rI then
there exists e2 with (e1 , e2 ) ∈ S and (d2 , e2 ) ∈ rJ . (I, d) is simulated by (J , e)
if there is a simulation S between I and J such that (d, e) ∈ S. Interpretations
I and J are globally equisimilar if, for any d ∈ ∆I , there exists e ∈ ∆J such
that (I, d) is simulated by (J , e) and (J , e) is simulated by (I, d). According
to [17, Theorem 17], an ALC TBox is equivalently EL⊥ -rewritable if its models
are preserved under products and global equisimulations.
Example 4. The TBox T = {∃r.A u ∃r.B u ∀r.(A t B) v E t F, A u B v ⊥} is
not equivalently EL⊥ -rewritable because its models are not preserved under
global equisimulations. Indeed, the interpretation I shown below is clearly a
model of T . However, by removing the rightmost r-arrow from I, we obtain an
interpretation which is globally equisimilar to I but not a model of T .
A B
r r r
On the other hand, the EL⊥ TBox
{∃r.A u ∃r.B v ∃r.G, ∃r.(G u A) v E, ∃r.(G u B) v F, A u B v ⊥}
is easily seen to be an ALC-conservative EL⊥ rewriting of T . We now show that T
is not model-conservatively EL⊥ -rewritable. For suppose T has such a rewriting
T 0 given in standard normal form (with inclusions of the form A1 u. . .uAn v B,
∃r.B v A, or A v ∃r.B where A1 , . . . , An , A, B ∈ NC ∪{⊥}). Consider the model
I of T depicted below, and let I 0 be a model of T 0 such that I =sig(T ) I 0 .
a b
A B
r r
r
E F
x y
0 0
Let J be the same as I 0 except that x, y ∈ M J iff both x ∈ M I and y ∈ M I ,
for every M ∈ NC . Since x ∈ / E J and y ∈/ F J , J is not a model of T 0 . Since the
restriction of I to {a, b} is a model of T 0 , and the restrictions of I 0 to {a, b, x}
0
and {a, b, y} coincide, there is (C v D) ∈ T 0 such that x, y ∈ C J but x, y 6∈ DJ .
As I 0 is a model of T 0 , which is in standard normal form, and by the definition
0
of J , D must be a concept name. Since clearly x, y ∈ C I , we must also have
I0 J
x, y ∈ D , and so x, y ∈ D , which is a contradiction.
The following modified version of T
Tm = {∃r.A u ∃r.B u ∀r.(A t B) v ∃r.(A u E) t ∃r.(B u F ), A u B v ⊥}
is not equivalently EL⊥ -rewritable, but has a model-conservative EL⊥ -rewriting
Tm0 = {∃r.A u ∃r.B v ∃r.M, ∃r.(M u A) v ∃r.(M u E),
∃r.(M u B) v ∃r.(M u F ), A u B v ⊥}.
The difference from the previous example is that if d is an instance of ∃r.Au∃r.B,
then we can place the ‘marker’ M onto an r-successor of d which is either in
A u E or in B u F , whereas in the previous example the decision on where to
put the ‘marker’ G was not determined by the r-successors of d but by d itself.
We now prove that if there exists an EL⊥ -rewriting of an ALC TBox T , then
there is one without any ‘recursion’ for the newly introduced symbols. Let Σ =
sig(T ). We say that an EL⊥ TBox T 0 is in Σ-layered form of depth n if there
are mutually disjoint sets Γ0 , . . . , Γn of concept names such that Γi ∩ Σ = ∅
(0 ≤ i ≤ n) and the inclusions of T 0 take the following form, where r ∈ Σ:
level i atom inclusions: A1 u · · · u An v B, for A1 , . . . , An , B ∈ Σ ∪ Γi ∪ {⊥},
level i right-atom inclusions: ∃r.A v B for A ∈ Σ ∪ Γi+1 , B ∈ Σ ∪ Γi ∪ {⊥},
level i left-atom inclusions: A v ∃r.B, for A ∈ Σ ∪ Γi , B ∈ Σ ∪ Γi+1 ∪ {⊥}.
The depth of a concept C is the maximal number of nestings of existential
restrictions in C. The depth of a TBox is the maximal depth of its concepts.
Lemma 3. If an ALC TBox T of depth n is model- (or ALC-) conservatively
EL⊥ -rewritable, then there exists a model- (respectively, ALC-) conservative
EL⊥ -rewriting T 0 of T in sig(T )-layered form of depth n.
We use Lemma 3 to prove decidability of model-conservative EL⊥ -rewritability.
An ALC ABox A is a finite set of assertions of the form C(a) and r(a, b), where
C is an ALC concept and a, b are individual names. The set of individual names
that occur in an ABox A is denoted by ind(A). When interpreting ABoxes, we
adopt the standard name assumption: aI = a, for all a ∈ ind(A).
Let T be an ALC TBox of depth n > 0 (the case n = 0 is trivial). By
subn−1 (T ) we denote the closure under single negation of the set of subconcepts
of concepts in T of depth at most n − 1. By Θn−1 (T ) we denote the set of
maximal subsets t of subn−1 (T ) that are satisfiable in a model of T . A T -ABox
is an ABox such that tA (a) = {D | D(a) ∈ A} ∈ Θn−1 (T ) for all a ∈ ind(A).
Let A be a directed tree ABox of depth at most n (that is, all nodes in it are
at distance ≤ n from the root). We say that A is n-strongly satisfiable w.r.t. T
if there is a model I of A and T such that the rI -successors of aI , for every
a ∈ ind(A) of depth < n in A, coincide with the r-successors of a in A.
We now define inductively (T , i)-bisimilarity relations ∼i,T between pairs
(A1 , a1 ) and (A2 , a2 ), where the Ai are T -ABoxes and ai ∈ ind(Ai ):
– (A1 , a1 ) ∼0,T (A2 , a2 ) if tA1 (a1 ) = tA2 (a2 );
– (A1 , a1 ) ∼i+1,T (A2 , a2 ) if (A1 , a1 ) ∼0,T (A2 , a2 ) and, for every r ∈ sig(T ),
if r(d1 , e1 ) ∈ A1 then there is r(d2 , e2 ) ∈ A2 such that (A1 , e1 ) ∼i,T (A2 , e2 ),
and vice versa.
For every i ≥ 0, one can determine a finite set ATi of finite directed tree T -
ABoxes A with root ρA and of depth ≤ i such that:
– for every I |= T and every d ∈ ∆I , (I, d) is (T , i)-bisimilar to exactly one
(A, ρA ) ∈ ATi ;4
– every A ∈ ATi is strongly i-satisfiable w.r.t. T .
We assume that all ABoxes in AT0 , . . . , ATn have mutually distinct roots. We
define the canonical ABox AT with individuals {ρA | A ∈ ATi , i ≤ n} as follows:
– for Ai ∈ ATi , Ai+1 ∈ ATi+1 and r ∈ sig(T ), we have r(ρAi+1 , ρAi ) ∈ AT if
there exists r(ρAi+1 , b) ∈ Ai+1 such that the subtree of Ai+1 rooted at b is
(i, T )-bisimilar to Ai ;
– for Ai ∈ ATi and A ∈ sig(T ), we have A(ρAi ) ∈ AT iff A(ρAi ) ∈ Ai .
Note that AT is acyclic (but not a directed tree ABox).
Lemma 4. Let T be an ALC TBox of depth n. An EL⊥ TBox T 0 in sig(T )-
layered form of depth n is a model-conservative EL⊥ -rewriting of T iff
– T 0 |= T and
– there exists A0 =sig(T ) AT such that, for all i = 0, . . . , n, A0 satisfies all level
i inclusions in T 0 at all ρAi with Ai ∈ ATn−i .
Theorem 8. Model-conservative EL⊥ -rewritability of ALC TBoxes is decidable.
Proof. Given an ALC TBox T , we first construct the canonical ABox AT . If an
EL⊥ TBox T 0 in Σ-layered form of depth n satisfies the conditions of Lemma 4,
then there exists such a TBox with at most 2|AT | distinct fresh concept names.
As the number of such EL⊥ TBoxes is finite, one can check for each of them
whether the conditions of Lemma 4 are satisfied. o
4
Here we identify I with the ABox with assertions r(a, b), for (a, b) ∈ rI , and D(a),
for D ∈ subn−1 (T ) and a ∈ DI .
We now give necessary conditions for ALC-conservative EL⊥ -rewritability of
ALC TBoxes. First, we still have the preservation under products:
Theorem 9. Every ALC-conservatively EL⊥ -rewritable ALC TBox is preserved
under products.
Theorem 9 can be used to show that TBoxes such as {A v B t E} are not
ALC-conservatively EL⊥ -rewritable. To separate equivalently rewritable TBoxes
from ALC-conservatively rewritable TBoxes, we generalize the construction of
Example 4. In that case, we removed an r-arrow (d0 , d) from a tree-shaped model
I of T and obtained a model that is globally equisimilar to the original model
but not a model of T . It turns out that ALC-conservatively EL⊥ -rewritable ALC
TBoxes of depth 1 are preserved under the inverse of this operation. We say that
(I, d) is ⊆1 -simulated by (J , e) if (i ) d ∈ AI iff e ∈ AJ , for all A ∈ NC ; (ii )
for all r ∈ NR , if (e, e0 ) ∈ rJ then there exists d0 with (d, d0 ) ∈ rI and, for all
A ∈ NC , if e0 ∈ AJ then d0 ∈ AI ; (iii ) for all r ∈ NR , if (d, d0 ) ∈ rI then there
exists e0 with (e, e0 ) ∈ rJ and, for all A ∈ NC , we have d0 ∈ AI iff e0 ∈ AJ . Say
that I is globally ⊆1 -simulated by J if, for every e ∈ ∆J , there exists d ∈ ∆I
such that (I, d) is ⊆1 -simulated by (J , e). An ALC TBox is preserved under
⊆1 -simulations if every interpretation that globally ⊆1 -simulates a model of T
is a model of T .
Theorem 10. Every ALC-conservatively EL⊥ -rewritable ALC TBox of depth 1
is preserved under global ⊆1 -simulations.
This result can be used to show, for example, that T = {A v ∀r.B} is not
ALC-conservatively EL⊥ -rewritable. For the interpretation below is not a model
B
r r
A
of T , but by removing from it the rightmost r-arrow, we obtain an interpretation
which is globally ⊆1 -simulated by J and is a model of T . It remains open whether
preservation under products and global ⊆1 -simulations is sufficient for an ALC
TBox of depth 1 to be ALC-conservatively EL⊥ -rewritable.
5 Conclusion
Conservative rewritings of ontologies provide more flexibility than equivalent
rewritings and are more natural in practice. However, they are also techni-
cally much more challenging to analyse. For future work, we are particularly
interested in better understanding conservative rewritings to EL and related
logics. For example, can we find transparent model-theoretic characterizations
and explicit axiomatizations of the rewritten TBoxes? The results in Section 4
should provide a good starting point. Another challenging problem could be to
investigate rewritability to OWL 2 QL—essentially DL-Litecore extended with
role inclusions—which preserves answers to conjunctive queries over all possible
ABoxes. (Recall [6] that conjunctive query inseparability for OWL 2 QL TBoxes
is ExpTime-complete.)
References
1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family
and relations. Journal of Artificial Intelligence Research 36, 1–69 (2009)
2. Baader, F.: A formal definition for the expressive power of terminological knowl-
edge representation languages. Journal of Logic and Computation 6(1), 33–54
(1996)
3. Baader, F.: The description logic handbook: Theory, implementation, and appli-
cations. Cambridge University Press, Cambridge (2007)
4. Baader, F., Brandt, S., Lutz, C.: Pushing the EL Envelope. In: Proceedings of
IJCAI. pp. 364–369 (2005)
5. Bienvenu, M., ten Cate, B., Lutz, C., Wolter, F.: Ontology-based data access:
A study through disjunctive datalog, CSP, and MMSNP. ACM Transactions of
Database Systems 39(4), 33 (2014)
6. Botoeva, E., Kontchakov, R., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Query
inseparability for description logic knowledge bases. In: Proceedings of KR (2014)
7. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable
reasoning and efficient query answering in description logics: The DL-Lite family.
Journal of Automated Reasoning 39(3), 385–429 (2007)
8. Carral, D., Feier, C., Grau, B.C., Hitzler, P., Horrocks, I.: EL-ifying ontologies. In:
Proceedings of IJCAR. pp. 464–479 (2014)
9. Carral, D., Feier, C., Romero, A.A., Grau, B.C., Hitzler, P., Horrocks, I.: Is your
ontology as hard as you think? Rewriting ontologies into simpler DLs. In: Proceed-
ings of DL. pp. 128–140 (2014)
10. De Giacomo, G.: Decidability of Class-Based Knowledge Representation For-
malisms. Ph.D. thesis, Università di Roma (1995)
11. Ding, Y., Haarslev, V., Wu, J.: A new mapping from ALCI to ALC. In: Proceedings
of DL (2007)
12. Ghilardi, S., Lutz, C., Wolter, F.: Did I damage my ontology? A case for conser-
vative extensions in description logics. In: Proceedings of KR. pp. 187–197 (2006)
13. Kaminski, M., Grau, B.C.: Sufficient conditions for first-order and datalog
rewritability in ELU. In: Proceedings of DL. pp. 271–293 (2013)
14. Kazakov, Y.: Consequence-driven reasoning for horn SHIQ ontologies. In: Proceed-
ings of IJCAI. pp. 2040–2045 (2009)
15. Konev, B., Lutz, C., Walther, D., Wolter, F.: Formal properties of modularisa-
tion. In: Modular Ontologies: Concepts, Theories and Techniques for Knowledge
Modularization, pp. 25–66 (2009)
16. Konev, B., Lutz, C., Walther, D., Wolter, F.: Model-theoretic inseparability and
modularity of description logic ontologies. Artificial Intelligence 203, 66–103 (2013)
17. Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: Model-theoretic charac-
terizations and rewritability. In: Proceedings of IJCAI (2011)
18. Lutz, C., Wolter, F.: Deciding inseparability and conservative extensions in the
description logic EL. Journal of Symbolic Computation pp. 194–228 (2010)
19. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in ex-
pressive description logics. In: Proceedings of IJCAI. pp. 989–995 (2011)