=Paper=
{{Paper
|id=Vol-2211/paper-17
|storemode=property
|title=A Dynamic Extension of ALCO for Repairing via Preferred Updates
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-17.pdf
|volume=Vol-2211
|authors=Guillaume Feuillade,Andreas Herzig,Christos Rantsoudis
|dblpUrl=https://dblp.org/rec/conf/dlog/FeuilladeHR18
}}
==A Dynamic Extension of ALCO for Repairing via Preferred Updates==
https://ceur-ws.org/Vol-2211/paper-17.pdf
A Dynamic Extension of ALCO for Repairing via
Preferred Updates
Guillaume Feuillade, Andreas Herzig, and Christos Rantsoudis
IRIT, Univ. Toulouse, France
Abstract. In the database literature it has been proposed to resort to active in-
tegrity constraints in order to restore database integrity. Such active integrity con-
straints consist of a classical constraint together with a set of preferred update
actions that can be triggered when the constraint is violated. In this paper, we
adapt this idea to Description Logics: we extend TBox axioms by a set of pre-
ferred updates of atomic concepts. We resort to a dynamic logic framework in
order to provide an account of active TBox-based ABox repairs.
Keywords: ABox Repairs · Active Constraints · Dynamic Logic
1 Introduction
In Description Logics (DLs) the TBoxes are finite sets of axioms, i.e., general inclu-
sions or definitions, that are viewed as non-contingent knowledge: knowledge that is
typically stable in time. The ABoxes on the other hand contain contingent knowledge
that typically changes more frequently than that of the TBox. Such changes may lead
to inconsistencies w.r.t. TBoxes. Repairing an ABox that is inconsistent w.r.t. a TBox
is a standard task [17, 5, 6]. The notion comes from the database literature: whenever
a database does not conform to a set of integrity constraints it has to be repaired. This
is usually called database integrity maintenance [9, 10, 4]. Active integrity constraints
were proposed to provide preferred ways, out of all the possible ones, to restore the
integrity of a database [13, 7, 8]. The idea was to enhance each integrity constraint with
update actions indicating the preferred repair in case of inconsistency. For example,
the integrity constraint (∀X)[Bachelor(X) ∧ Married(X) → ⊥] which says that no one
should be identified as bachelor and married at the same time can be turned into the ac-
tive constraint (∀X)[Bachelor(X) ∧ Married(X) → ⊥, {−Bachelor(X)}], whose meaning
is that when there is a person in the database who has both the status of being a bachelor
and the status of being married then the preferred repair is to remove from the database
the bachelor status (as opposed to removing the married status) since married status can
be achieved from being bachelor but not the other way. In this way, the possible repairs
are narrowed down as well as better match designer preferences when maintaining the
database.
Now, applying the same idea to the DL setting requires the extension of the TBox
axioms with update actions. Note that our perspective differs from [19, 21] since we
do not want to single out integrity constraints from the TBox. The resulting extended
TBoxes are called active TBoxes in accordance with the nomenclature of active con-
straints. The authors have already investigated this research avenue in [20], which pro-
poses a syntactic approach. Here we take a semantic approach and investigate how the
various definitions of repairs from the database literature behave in the DL setting. We
represent update actions as atomic dynamic logic programs and show that repairs can
be represented as complex programs. The main reason for using this framework is to
account for dynamic repairing procedures that check in multiple steps the status of a
possible repair and terminate once consistency with the TBox has been achieved. This
comes in contrast with methods used for active integrity constraints where the update
is applied in one go and later checked if it follows the active axioms using certain cri-
teria. The dynamic logic framework also allows us to lift the approach of [12] from
propositional databases to DLs.
We consider that TBoxes are composed of concept inclusion axioms in the lan-
guage of ALC, without the unique name assumption. Unfortunately, there exist ALC
ABoxes that when semantically updated cannot be expressed in ALC [18]. It is for that
reason that our ABoxes may contain nominals. Both the TBox and the ABox can be
represented in our language by single formulas.
Before moving on let us showcase an example of an active TBox that we will be
able to construct and work with. First, consider the following TBox T :
{Sibling v Brother t Sister, ∀hasSibling.⊥ v OnlyChild}
An active TBox extending T then is aT = {η1 , η2 } where:
η1 : hSibling u ¬Brother u ¬Sister v ⊥, {−Sibling}i
η2 : h∀hasSibling.⊥ u ¬OnlyChild v ⊥, {+OnlyChild}i
Through these enhanced concept inclusions, we can be more specific in the update ac-
tions that we prefer when repairing an ABox that is inconsistent with T : the active
axioms of aT ‘dictate’ that an individual who is neither a brother nor a sister of some-
one should drop their sibling status, whereas an individual who has no siblings should
change its status and be an only child.
The paper is structured as follows. Section 2 presents syntax and semantics of for-
mulas and programs. In Section 3 we prove decidability through reduction axioms elim-
inating programs from formulas. Section 4 is the main contribution of the paper where
we import the idea behind active integrity constraints to DL. We then adapt the notions
of founded repairs and dynamic repairs to the DL setting and use the programs of our
language to constructively represent them. We conclude in Section 5.
2 Syntax and Semantics
We introduce the basics of DLs and Propositional Dynamic Logic PDL, referring to
[2] and [14, 15] for more details. The update of an ABox will be represented with the
help of PDL programs. Their behavior is identical with the programs of PDL, with
formulas of the form hπiϕ expressing that ϕ is true after some possible execution of
the program π. The main difference is at the atomic level: whereas PDL has abstract
atomic programs, the atomic programs of our language have the form ±A(a) where
A(a) is an atomic assertion. This makes a big difference: the programs of our language
can be eliminated and every formula is reducible to a static formula, i.e., a formula
without programs. This is crucial in acquiring a unique representation of the update of
an ABox through a static formula. We note that the models of our logic are different
from (and quite simpler than) the Kripke models of PDL: the familiar interpretations of
Description Logic suffice.
2.1 Language
Let Con be a countable set of atomic concepts, R a countable set of roles and Ind a
countable set of individual names. The language of formulas and programs is defined
by the following grammar:
c
ϕ F A | {a} | ⊥ | ϕ → ϕ | ∃r.ϕ | Uϕ | hπiϕ | hπi ϕ
π F +A(a) | −A(a) | π; π | π ∪ π | π∗ | ϕ?
where A ∈ Con, a ∈ Ind, and r ∈ R. Atomic programs have the form +A(a) and
−A(a). Sometimes we will use the expression ±A(a) to talk about both. The operators
of sequential and nondeterministic composition, the Kleene star and the test are familiar
from PDL. Uϕ expresses the fact that ϕ is true for every individual of an interpretation.
The logical connectives ¬, >, ∧, ∨ and ↔ as well as the universal quantifier ∀
are abbreviated in the usual way. The expression πn abbreviates the program π; . . . ; π
where π appears n times, and π≤n abbreviates the program π ∪ >? n . We also define
π+ to be π; π∗ . Furthermore, while ϕ do π abbreviates the program (ϕ?; π)∗ ; ¬ϕ? and
a : ϕ abbreviates the formula U({a} → ϕ). Finally, r(a, b) abbreviates the formula
U({a} → ∃r.{b}).
We use the language of the basic description logic ALC for TBoxes and that of
its extension ALCO with nominals for ABoxes. The TBoxes are composed of concept
inclusion axioms and the ABoxes contain concept assertions a : C and role assertions
r(a, b) where C is any concept description in ALCO, r is a role and a, b are individuals.
We will identify a TBox T and an ABox A, respectively, with the formulas:
^ ^ ^
UC→D and (a :C) ∧ r(a, b)
CvD∈T a:C∈A r(a,b)∈A
Finally, Con(π) denotes the set of all atomic concepts occurring in the program π.
Similarly, Ind(π) denotes the set of all individuals occurring in π.
2.2 Interpretations and their Updates
Interpretations are couples I = (∆I , ·I ) where ∆I is the domain and ·I maps each
atomic concept A to a subset of ∆I , each role r to a binary relation on ∆I and each
individual name a to an element of ∆I , i.e., AI ⊆ ∆I , rI ⊆ ∆I × ∆I and aI ∈ ∆I .
An indexical update action is an expression of the form +A or −A, where A is an
atomic concept. A (non-indexical) update action is an expression of the form +A(a) or
−A(a), where A is an atomic concept and a an individual. A set of update actions U is
consistent iff it does not contain both +A(a) and −A(a) for some assertion A(a).
Definition 1. Let U be a consistent set of update actions. The update of the interpreta-
tion I by U, denoted by I U, is the interpretation I0 such that:
0
• ∆I = ∆I
0
• AI = AI ∪ {aI | +A(a) ∈ U} \ {aI | −A(a) ∈ U}
0
• rI = rI
I0
• a = aI
Note that a consistent U can be identified with a program πU , supposing that the
update actions of U are applied in sequence (where, thanks to consistency, the order
does not matter).
2.3 Semantics
The extension of ·I to complex formulas is defined inductively as follows:
{a}I = {aI }
⊥I = ∅
ϕ → ψ I = ∆I \ ϕI ∪ ψI
∃r.ϕ I = {δ ∈ ∆I | there is δ0 ∈ ∆I such that (δ, δ0 ) ∈ rI and δ0 ∈ ϕI }
I ∆I if ϕI = ∆I
Uϕ =
∅
otherwise
I [ I0
hπiϕ = ϕ
(I,I0 )∈k π k
c I [ 0
hπi ϕ = ϕI
(I0 ,I)∈k π k
while the semantics of programs is:
(I, I0 ) ∈ || + A(a) || iff I0 = I {+A(a)}
(I, I0 ) ∈ || − A(a) || iff I0 = I {−A(a)}
(I, I0 ) ∈ || π1 ; π2 || iff there exists I00 such that (I, I00 ) ∈ || π1 || and (I00 , I0 ) ∈ || π2 ||
(I, I0 ) ∈ || π1 ∪ π2 || iff (I, I0 ) ∈ || π1 || ∪ || π2 ||
(I, I0 ) ∈ || ϕ? || iff I0 = I and
[ϕ = ∆
I I
(I, I ) ∈ || π || iff (I, I ) ∈
0 ∗ 0
|| π ||k
k∈N0
An interpretation I is a model of a formula ϕ iff ϕI = ∆I . We say that ϕ is (globally)
satisfiable iff there exists a model of ϕ. We say that ϕ is valid iff every interpretation is
a model of ϕ. We call the logic that is built using this syntax and semantics dynALCO.
The update of an ABox A by a consistent set of update actions U is the set:
A U = {I U | I is a model of A}
This is a semantic definition. A U has also at least one syntactic representation, but it
is not unique: there are many ABoxes that can be used to describe it. In particular, the
c
set A U equals the set of interpretations satisfying hπU i A, where πU is the program
that applies the update actions of U.
3 Reduction Axioms and Decidability
We now show how to convert any dynALCO formula to an equivalent static formula,
i.e., a formula without programs. We first reduce complex programs to atomic programs
and then eliminate atomic programs from formulas. This is familiar e.g. from Dynamic
Epistemic Logics, see [11]. We start with the reduction axioms for complex programs.
Proposition 1. The following equivalences are valid:
hπ1 ; π2 i ϕ ↔ hπ1 ihπ2 i ϕ
hπ1 ∪ π2 i ϕ ↔ hπ1 i ϕ ∨ hπ2 i ϕ
n
hπ∗ i ϕ ↔ hπ≤2 i ϕ
hψ?i ϕ ↔ Uψ ∧ ϕ
where n = card(Con(π)) × card(Ind(π)).
Observe that, contrarily to PDL and just as in DL-PA [3], the Kleene star can be
eliminated. The next proposition shows how to reduce atomic programs.
Proposition 2. The following equivalences are valid:1
{a} ∨ B
if A = B
h+A(a)iB ↔
B
otherwise
¬{a} ∧ B if A = B
h−A(a)iB ↔
B
otherwise
h±A(a)i {b} ↔ {b}
h±A(a)i¬ϕ ↔ ¬h±A(a)iϕ
h±A(a)i (ϕ ∨ ψ) ↔ h±A(a)i ϕ ∨ h±A(a)i ψ
h±A(a)i∃r.ϕ ↔ ∃r.h±A(a)iϕ
h±A(a)iUϕ ↔ Uh±A(a)iϕ
where A, B ∈ Con, r ∈ R and a, b ∈ Ind.
Finally, the reduction axioms for the converse operator follow.
1
Note that we have used the logical connectives ¬ and ∨ in the place of ⊥ and → since they are
easier to present.
Proposition 3. The following equivalences are valid:
c
h+A(a)i ϕ ↔ (a : A) ∧ ϕ ∨ h−A(a)iϕ
c
h−A(a)i ϕ ↔ (a : ¬A) ∧ ϕ ∨ h+A(a)iϕ
c c c
hπ1 ; π2 i ϕ ↔ hπ2 i hπ1 i ϕ
c c c
hπ1 ∪ π2 i ϕ ↔ hπ1 i ϕ ∨ hπ2 i ϕ
c n c
hπ∗ i ϕ ↔ hπ≤2 i ϕ
c
hψ?i ϕ ↔ hψ?i ϕ
Using now Propositions 1, 2 and 3 we obtain the following theorem.
Theorem 1. Every formula of dynALCO is equivalent to a static formula.
Through Theorem 1 we can now obtain a unique syntactical representation of the
c
set A U by reducing the formula hπU i A to a static one containing no programs.
Example 1 ([18]). Let A = {John : ∃hasChild.Happy, Mary : Happy u Clever} and
U = {−Happy(Mary)}. Applying the reduction axioms to:
c
h−Happy(Mary)i (John : ∃hasChild.Happy) ∧ (Mary : Happy ∧ Clever)
we obtain the static formula:
John : ∃hasChild.(Happy ∨ {Mary}) ∧ Mary : ¬Happy ∧ Clever
which accurately represents A U.
Last but not least, decidability of global satisfiability in dynALCO follows from,
first, the fact that any static formula can be mapped to an ALCO(U)-concept and vice
versa, where ALCO(U) denotes the language ALCO together with the universal role,
and, second, the fact that concept satisfiability in ALCO(U) is decidable [16]. Thus,
(global) satisfiability checking of the static fragment of our logic can be reduced to the
satisfiability problem of ALCO(U). We then obtain the following theorem.
Theorem 2. Global satisfiability in the logic dynALCO is decidable.
4 Active Inclusion Axioms in ALC TBoxes
In this section we import the idea behind active integrity constraints into DL and exam-
ine dynamic ways an ABox can be repaired via the preferred update actions suggested
by the active axioms. To do this we first have to enrich concept inclusions with update
actions, indicating the preferred ways to be repaired in case of inconsistency.
We start with the definitions of static and active concept inclusions.
Definition 2. A concept inclusion of the form C1 u· · ·uCn v ⊥ is called a static concept
inclusion.
Note that in ALC, any concept inclusion axiom is equivalent to a static concept
inclusion.
Definition 3. Let ρ = C1 u · · · uCn v ⊥ be a static concept inclusion. An active concept
inclusion is of the form h ρ, V i where V is a set of indexical update actions such that:
• if +A ∈ V then there exists Ci = ¬A with A ∈ Con.
• if −A ∈ V then there exists Ci = A with A ∈ Con.
An active TBox, denoted by aT , is a set of active concept inclusions.
For an active concept inclusion η = h ρ, V i we let static(η) = ρ and active(η) =
V. Note that active(η) can be empty. For [ an active TBox aT we let static(aT ) =
{static(η) : η ∈ aT } and active(aT ) = active(η). We say that aT extends T
iff T is equivalent to static(aT ). η ∈ aT
Going back to the example of Section 1, we observe that the active TBox aT con-
forms to the above definitions. Note also that static(aT ) is equivalent to T .
From now on we consider some fixed finite sets Con of atomic concepts and Ind
of individuals. Furthermore, we consider a fixed consistent TBox T and a fixed active
TBox aT extending T . Finally, we suppose that all ABoxes we work with are consis-
tent. An ABox A is inconsistent with respect to T iff there is no interpretation satisfying
both A and T . Note that in dynALCO this amounts to unsatisfiability of the formula
T ∧ A.
In the next two subsections, we define the notions of founded and dynamic repairs of
an ABox A with respect to aT , which choose among the update actions in active(aT )
and modify the ABox such that A is consistent with the concept inclusion axioms of
T . The former are based on [7, 8] while the latter are based on [12].
4.1 Founded Weak Repairs and Founded Repairs
We start with the notion of foundedness, which is a key condition that a repair should
satisfy for its update actions to be supported by the active concept inclusions.
Definition 4. Let I be an interpretation. A set of update actions U is founded with
respect to aT and I if for every ±A(a) ∈ U there exists an η ∈ aT such that:
• ±A ∈ active(η)
• I U is a model of static(η)
• I (U \ {±A(a)}) is not a model of static(η)
Based on this, the definitions of a founded weak repair and a founded repair follow.
Definition 5. Let static(aT ) ∧ A be unsatisfiable. A founded weak repair of A is a
consistent set of update actions U such that (1) T ∧ (A U) is satisfiable and (2)
there is a model I of A such that U is founded with respect to aT and I. If moreover
T ∧ (A U 0 ) is unsatisfiable for all U 0 ⊂ U, then U is a founded repair of A.
The following simple example showcases this definition.
Example 2. Consider the TBox T = {Born v Alive, > v Alive t Dead}. Consider also
the following active TBox which extends T :
aT = {hBorn u ¬Alive v ⊥, {+Alive}i, h¬Alive u ¬Dead v ⊥, {+Dead}i}
Furthermore, consider the ABox A = {John : Born u ¬Alive u ¬Dead} which is
inconsistent with T . The set {+Alive(John)} is the only founded weak repair of A.
Indeed, the second update action in {+Alive(John), +Dead(John)} cannot be founded
on the second active axiom of aT . It is also the only founded repair.
We now extend the set of atomic concepts Con by new concepts A+ and A− uniquely
associated with each concept A. They allow us to keep track of the concepts that are
added to or removed from an ABox. We use these then to define the following program:
toggle± (A(a)) = ¬ (a : A+ ) ∧ ¬ (a : A− ) ? ; (+A(a) ; +A+ (a)) ∪ (−A(a) ; +A− (a))
which is intuitively the program +A(a) ∪ −A(a) but enhanced with update operations
that keep track of any changes.
Next, in order to find a founded weak repair we have to ensure that the foundedness
condition of Definition 4 holds after the update actions of the toggle± (A(a)) program.
To do this, we define the following formula:
^ _
a : A+ ∨ a : A− →
Founded = + A(a) ∪ −A(a) ¬static(η)
A∈Con η∈aT
a∈Ind ±A∈active(η)
which does exactly that: it checks for all concepts that have been added to or removed
from an assertion that they belong to the active part of some concept inclusion and
that, without them, the static part of this same concept inclusion is violated. Using the
aforementioned we can now define the program that searches for founded weak repairs:
[ ∗
foundedWeakRepair = toggle± (A(a)) ; T ?; Founded?
A∈Con
a∈Ind
The next step is to define the program:
undo(A(a)) = (a : A+ ) ? ; −A(a) ; −A+ (a) ∪ (a : A− ) ? ; +A(a) ; −A− (a)
which, as the name suggests, will undo any change that was imposed on an assertion.
Now, in order to redo any changes that are stored through A+ and A− to an alternative
interpretation, we use the program:
redo(A(a)) = (a : A+ ) ? ; +A(a) ∪ (a : A− ) ? ; −A(a)
The last step in checking minimality is to define a program that visits all models
of the original ABox A. This will allow us to check whether we can obtain a founded
weak repair using less update actions. It is easy to see that this can be achieved through
the program: [ ∗
gotoAltInt(A) = + A(a) ∪ −A(a) ; A ?
A∈Con
a∈Ind
Summing up, we use the above to create the formula:
[ ∗ [ +
Minimal(A) = ¬ h gotoAltInt(A) ; redo(A(a)) ; undo(A(a)) i T
A∈Con A∈Con
a∈Ind a∈Ind
which is the key ingredient in checking if a repair is minimal with respect to other
repairs. Note that the redo(A(a)) program may not actually reapply all of the update
actions that may have been stored earlier through the toggle± (A(a)) program: it does
not need to, as reapplying only some of them is equivalent to reapplying all of them and
undoing all those that were left out.
We can now define the program that searches for founded repairs:
foundedRepair(A) = foundedWeakRepair ; Minimal(A) ?
Last but not least, let makeFalse± abbreviate the program which falsifies all the
assertions of the form A+ (a) and A− (a) for all A ∈ Con and a ∈ Ind. The program
makeFalse± will be used in the final step to make sure that none of the new concepts
that were used for storing purposes survive in the repair.
We showcase all of the above in the following theorem, which completes the picture.
Theorem 3. Let A be inconsistent with respect to static(aT ) and let U be a consistent
set of update actions. Furthermore, let no atomic concept A+ or A− appear in any of
them.
• U is a founded weak repair of A iff there exists an I such that:
^
¬(a : A+ )∧¬(a : A− ) ?; foundedWeakRepair; makeFalse±
(I, IU) ∈ A∧
A∈Con
a∈Ind
• U is a founded repair of A iff there exists an I such that:
^
¬(a : A+ )∧¬(a : A− ) ? ; foundedRepair(A) ; makeFalse±
(I, IU) ∈ A∧
A∈Con
a∈Ind
Going back to Example 2, we can now witness how, taking I to be a model of
{John : Born u ¬Alive u ¬Dead}, the set {+Alive(John)} satisfies both of the conditions
of Theorem 3. On the other hand, the set {+Alive(John), +Dead(John)} doesn’t satisfy
them for any interpretation I.
4.2 Dynamic Weak Repairs and Dynamic Repairs
We will now investigate dynamic repairs which exploit even better the programs and
the setting of Dynamic Logic in order to provide a different view of repairs. We begin
with some definitions.
For every active concept inclusion η ∈ aT and individual a, the programs πaη and
πη are defined as follows:
± a
[
πaη = ¬ a : static(η) ? ; ±A(a)
±A∈active(η)
[
+ a
πη = + A(a) ; +A+ (a)
+A∈active(η)
[
πη =
− a
− A(a) ; +A− (a)
−A∈active(η)
πη = ¬ a : static(η) ? ; + πaη
± a
∪ − πaη
Intuitively, the program πaη will check for each active concept inclusion η and indi-
vidual a whether the static concept inclusion in η is violated at a, and if so, will try to
repair it using only update actions that are specified by η. The program ± πaη furthermore
stores the concepts that have been changed.
Using the program πaη we can now formally define dynamic weak repairs and dy-
namic repairs.
Definition 6. Let static(aT ) ∧ A be unsatisfiable. A consistent set of update actions U
is a dynamic weak repair of A iff there exists an I such that:
[
(I, I U) ∈ A ? ; while ¬T do πaη
a∈Ind
η∈aT
If T ∧ (A U 0 ) is unsatisfiable for all U 0 ⊂ U, then U is a dynamic repair of A.
It is worth noting that dynamic weak repairs are not necessarily founded. The next
example showcases this.
Example 3 (Example 2, ctd.). Consider again the active TBox:
aT = {hBorn u ¬Alive v ⊥, {+Alive}i, h¬Alive u ¬Dead v ⊥, {+Dead}i}
and the ABox A = {John : Born u ¬Alive u ¬Dead}, whose only founded weak
repair was {+Alive(John)}. There are two dynamic weak repairs of A, namely U1 =
{+Alive(John)} and U2 = {+Alive(John), +Dead(John)}. Only U1 is a dynamic repair.
We will use now the program ± πaη together with the formula Minimal(A) to show
how a dynamic repair can be extracted using the familiar procedure of the previous
theorem. Defining:
[
dynamicRepair(A) = while ¬T do πη ; Minimal(A) ?
± a
a∈Ind
η∈aT
we have the following theorem.
Theorem 4. Let A be inconsistent with respect to static(aT ) and let U be a consistent
set of update actions. Furthermore, let no atomic concept A+ or A− appear in any of
them. U is a dynamic repair of A iff there exists an I such that:
^
¬(a : A+ ) ∧ ¬(a : A− ) ? ; dynamicRepair(A) ; makeFalse±
(I, I U) ∈ A ∧
A∈Con
a∈Ind
Going back to Example 3 this time we can witness how, taking I to be a model of
{John : Born u ¬Alive u ¬Dead}, only the set {+Alive(John)} satisfies the condition of
Theorem 4 whereas the set {+Alive(John), +Dead(John)} does not, for any I.
5 Discussion and Conclusion
We have seen how different repairing methods based on preferred update actions of
the database literature translate into Description Logics. We have defined a repair to
be a set of update actions U such that, when applied to an ABox, the outcome is a
repaired ABox that follows the active axioms of—and is consistent with—the active
TBox. The way to find such a U is the following: starting with a model I of an ABox
A, we can extract a founded or dynamic repair U of A by finding an I0 such that
(I, I0 ) ∈ || foundedRepair(A) || or (I, I0 ) ∈ || dynamicRepair(A) ||, respectively, and
0 0
setting U = {+A(a) : a : A+ I = ∆I } ∪ {−A(a) : a : A− I = ∆I }. The dynamic logic
0 0
framework on which we rely is useful for not only representing the various repairs
but also for constructing them. Constructing the repaired ABox then would amount to:
c
either extract A U by reducing the formula hπU i A as in Example 1 or immediately
apply the update U in the initial ALCO ABox and characterize A U via a semantic
update of A by U.
A slightly different route, more in line with Description Logic, would be to define
a repair to be any repaired ABox A0 and, given an ABox A, evaluate if A0 is indeed a
repair of A by checking if the formula A∧hrepairi A0 is satisfiable, where repair is any
of the repair programs defined in the previous section and used in Theorems 3 and 4. Of
course we then would have to guess such a repair A0 , but the satisfiability check could
also be used for assertions instead of whole ABoxes, in order to check if something
more specific follows from repairing the initial ABox under the active axioms of an
active TBox.
Deciding the existence of founded and dynamic repairs also amounts to satisfiability
checking. More specifically, taking repair to be once again any of the repair programs,
c
we can decide the existence of each one by checking whether the formula hrepairi A
is satisfiable, where A is the initial ABox. Indeed, any interpretation that satisfies the
c
formula hrepairi A will be a model of at least one repaired ABox. Our approach also
comes close to the work presented in [1] where dynamic problems on graph-structured
data are reduced to static DL reasoning. Apart from the difference in the Dynamic Logic
framework presented here and the fact that we are not restricted to finite interpretations,
the main differentiation between the two works is the fact that we introduce and work
mainly with active TBoxes as well as adapt the various repairs found in the database
literature of active integrity constraints to the DL setting.
A limitation of our approach comes from the boolean nature of the active concept
inclusions and the fact that complex concepts cannot be paired with a preferred update
action in the active part of a concept inclusion. For instance, it is easy to see that ac-
cording to Definition 3, the TBox T = {∃hasFather.Female v ⊥} can be only extended
to the active TBox aT = { h∃hasFather.Female v ⊥, ∅i }. At first sight, going through
roles to apply the atomic programs or add/remove roles between individuals seems to
make the logic undecidable, mainly because of the interplay between these more pow-
erful programs and the Kleene star, but the fine details are left for future work.
Summing up, we have taken a semantic approach to repairing ABoxes with regard
to active TBoxes, the latter being an extension of regular TBoxes with update actions.
To that end we have exploited a dynamic logic framework on which various repairing
procedures are introduced and discussed.
References
1. Ahmetaj, S., Calvanese, D., Ortiz, M., Simkus, M.: Managing change in graph-structured
data using description logics. ACM Trans. Comput. Log. 18(4), 27:1–27:35 (2017), http:
//doi.acm.org/10.1145/3143803
2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The
Description Logic Handbook: Theory, Implementation, and Applications. Cambridge Uni-
versity Press, New York, NY, USA (2003)
3. Balbiani, P., Herzig, A., Troquard, N.: Dynamic logic of propositional assignments: a well-
behaved variant of PDL. In: Kupferman, O. (ed.) Logic in Computer Science (LICS). IEEE
(2013)
4. Bertossi, L.: Database Repairing and Consistent Query Answering. Morgan & Claypool Pub-
lishers (2011)
5. Bienvenu, M., Bourgaux, C., Goasdoué, F.: Querying inconsistent description logic knowl-
edge bases under preferred repair semantics. In: Proceedings of the Twenty-Eighth AAAI
Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada.
pp. 996–1002 (2014), http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/
view/8231
6. Bienvenu, M., Bourgaux, C., Goasdoué, F.: Query-driven repairing of inconsistent dl-lite
knowledge bases. In: Proceedings of the Twenty-Fifth International Joint Conference on Ar-
tificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016. pp. 957–964 (2016),
http://www.ijcai.org/Abstract/16/140
7. Caroprese, L., Greco, S., Zumpano, E.: Active integrity constraints for database consistency
maintenance. IEEE Trans. Knowl. Data Eng. 21(7), 1042–1058 (2009)
8. Caroprese, L., Truszczynski, M.: Active integrity constraints and revision programming.
TPLP 11(6), 905–952 (2011)
9. Ceri, S., Fraternali, P., Paraboschi, S., Tanca, L.: Automatic generation of production rules
for integrity maintenance. ACM Trans. Database Syst. 19(3), 367–422 (Sep 1994), http:
//doi.acm.org/10.1145/185827.185828
10. Chomicki, J., Marcinkowski, J.: Minimal-change integrity maintenance using tuple dele-
tions. Inf. Comput. 197(1-2), 90–121 (Feb 2005), http://dx.doi.org/10.1016/j.ic.
2004.04.007
11. Ditmarsch, H.v., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Springer Publishing
Company, Incorporated, 1st edn. (2007)
12. Feuillade, G., Herzig, A.: A dynamic view of active integrity constraints. In: Fermé, E.,
Leite, J. (eds.) Logics in Artificial Intelligence - 14th European Conference, JELIA 2014,
Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings. Lecture Notes in Com-
puter Science, vol. 8761, pp. 486–499. Springer (2014), https://doi.org/10.1007/
978-3-319-11558-0
13. Flesca, S., Greco, S., Zumpano, E.: Active integrity constraints. In: Moggi, E., Warren, D.S.
(eds.) PPDP. pp. 98–107. ACM (2004)
14. Harel, D.: Dynamic logic. In: Gabbay, D.M., Günthner, F. (eds.) Handbook of Philosophical
Logic, vol. II, pp. 497–604. D. Reidel, Dordrecht (1984)
15. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
16. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty, P., My-
lopoulos, J., Welty, C.A. (eds.) Proceedings, Tenth International Conference on Principles
of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June
2-5, 2006. pp. 57–67. AAAI Press (2006), http://www.aaai.org/Library/KR/2006/
kr06-009.php
17. Lembo, D., Lenzerini, M., Rosati, R., Ruzzi, M., Savo, D.F.: Inconsistency-tolerant seman-
tics for description logics. In: Web Reasoning and Rule Systems - Fourth International Con-
ference, RR 2010, Bressanone/Brixen, Italy, September 22-24, 2010. Proceedings. pp. 103–
117 (2010), http://dx.doi.org/10.1007/978-3-642-15918-3_9
18. Liu, H., Lutz, C., Milicic, M., Wolter, F.: Foundations of instance level updates in expressive
description logics. Artificial Intelligence 175(18), 2170–2197 (2011)
19. Motik, B., Horrocks, I., Sattler, U.: Bridging the gap between OWL and relational databases.
J. Web Sem. 7(2), 74–89 (2009), https://doi.org/10.1016/j.websem.2009.02.001
20. Rantsoudis, C., Feuillade, G., Herzig, A.: Repairing ABoxes through active integrity con-
straints. In: Artale, A., Glimm, B., Kontchakov, R. (eds.) Proceedings of the 30th Interna-
tional Workshop on Description Logics, Montpellier, France, July 18-21, 2017. CEUR Work-
shop Proceedings, vol. 1879. CEUR-WS.org (2017), http://ceur-ws.org/Vol-1879/
paper41.pdf
21. Tao, J., Sirin, E., Bao, J., McGuinness, D.L.: Integrity constraints in OWL. In: Fox, M.,
Poole, D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Artificial In-
telligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press (2010),
http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1931