In the database literature it has been proposed to resort to active integrity constraints in order to restore database integrity. Such active integrity constraints 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 preferred updates of atomic concepts. We resort to a dynamic logic framework in order to provide an account of active TBox-based ABox repairs.
Introduction
In Description Logics (DLs) the TBoxes are finite sets of axioms, i.e., general
inclusions 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 [
Now, applying the same idea to the DL setting requires the extension of the TBox
axioms with update actions. Note that our perspective di ers 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
constraints. The authors have already investigated this research avenue in [20], which
proposes 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
criteria. The dynamic logic framework also allows us to lift the approach of [
We consider that TBoxes are composed of concept inclusion axioms in the language 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 : fSibling v Brother t Sister; 8hasSibling:? v OnlyChildg An active TBox extending T then is aT = f 1; 2g where: ; 1 : hSibling u :Brother u :Sister v ? f Siblinggi
Through these enhanced concept inclusions, we can be more specific in the update actions 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 someone 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 formulas and programs. In Section 3 we prove decidability through reduction axioms eliminating 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
[
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 j fag j ? j ' ! ' j 9r:' j U' j h i' j h i '
F +A(a) j A(a) j ; j [ j j '? where A 2 Con, a 2 Ind, and r 2 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 8 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(fag ! '). Finally, r(a; b) abbreviates the formula U(fag ! 9r:fbg).
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: ^ U C ! D CvD2T and a:C2A ^(a : C) ^ ^ r(a; b) r(a;b)2A
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 2 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 i it does not contain both +A(a) and A(a) for some assertion A(a).
fagI = faIg ' ! ?I = ;
I = 9r:' I = f 2 U' I = <>8> I > >:; [ 'I0 h i' I = (I;I0)2k k
[ 'I0 h ic ' I = (I0;I)2k k
I n 'I [
I if 'I = I otherwise
I j there is 0 2 I such that ( ; 0) 2 rI and 0 2 'Ig Definition 1. Let U be a consistent set of update actions. The update of the interpretation I by U, denoted by I U, is the interpretation I0 such that:
I0 = I AI0 = AI [ faI j +A(a) 2 Ug n faI j A(a) 2 Ug rI0 = rI aI0 = 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: while the semantics of programs is:
I0 = I f+A(a)g (I; I0) 2 jj + A(a) jj i
A(a) jj i (I; I0) 2 jj I0 = I f A(a)g
(I; I0) 2 jj 1; 2 jj i there exists I00 such that (I; I00) 2 jj 1 jj and (I00; I0) 2 jj 2 jj (I; I0) 2 jj 1 [ 2 jj i (I; I0) 2 jj 1 jj [ jj 2 jj (I; I0) 2 jj '? jj i I0 = I and 'I = I (I; I0) 2 jj jj i (I; I0) 2 [ jj jjk
k2N0
An interpretation I is a model of a formula ' i 'I = I. We say that ' is (globally) satisfiable i there exists a model of '. We say that ' is valid i 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
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
set A U equals the set of interpretations satisfying h U ic A, where U is the program
that applies the update actions of U.
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 [
h 1; 2i ' $ h 1ih 2i ' h 1 [ 2i ' $ h 1i ' _ h 2i ' h i ' $ h h ?i ' $ U 2n i ' ^ ' where n = card(Con( )) card(Ind( )).
Observe that, contrarily to PDL and just as in DL-PA [
: h A(a)i fbg $ fbg h A(a)i:' $ :h A(a)i' if A = B otherwise if A = B otherwise h A(a)i (' _ ) $ h A(a)i ' _ h A(a)i h A(a)i9r:' $ 9r:h A(a)i' h A(a)iU' $ Uh A(a)i' where A; B 2 Con, r 2 R and a; b 2 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: h+A(a)ic ' $ (a : A) ^ ' _ h A(a)i' h A(a)ic ' $ (a : :A) ^ ' _ h+A(a)i'
c c c h 1; 2i ' $ h 2i h 1i '
c c c h 1 [ 2i ' $ h 1i ' _ h 2i '
c 2n c h i ' $ h 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 set A U by reducing the formula h U ic A to a static one containing no programs. Example 1 ([18]). Let A = fJohn : 9hasChild:Happy; Mary : Happy u Cleverg and U = f Happy(Mary)g. Applying the reduction axioms to:
h Happy(Mary)ic (John : 9hasChild:Happy) ^ (Mary : Happy ^ Clever) we obtain the static formula: which accurately represents A
John : 9hasChild:(Happy _ fMaryg) ^ Mary : :Happy ^ Clever
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 [
Active Inclusion Axioms in ALC TBoxes In this section we import the idea behind active integrity constraints into DL and examine 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 inclusion. uCn v ? is called a static concept
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 2 V then there exists Ci = :A with A 2 Con.
if A 2 V then there exists Ci = A with A 2 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 ) = fstatic( ) : 2 aT g and active(aT ) = [ active( ). We say that aT extends T i T is equivalent to static(aT ). 2aT
Going back to the example of Section 1, we observe that the active TBox aT conforms 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 consistent. An ABox A is inconsistent with respect to T i 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 [
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) 2 U there exists an 2 aT such that:
I U is a model of static( ) I (U n f A(a)g) 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 U0) is unsatisfiable for all U0 U, then U is a founded repair of A.
The following simple example showcases this definition.
Example 2. Consider the TBox T = fBorn v Alive; > v Alive t Deadg. Consider also the following active TBox which extends T :
aT = fhBorn u :Alive v ?; f+Alivegi; h:Alive u :Dead v ?; f+Deadgig Furthermore, consider the ABox A = fJohn : Born u :Alive u :Deadg which is inconsistent with T . The set f+Alive(John)g is the only founded weak repair of A. Indeed, the second update action in f+Alive(John); +Dead(John)g 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:
Founded = ^
a : A+ _ a : A 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? A2Con a2Ind 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) [ Summing up, we use the above to create the formula:
Minimal(A) = : h gotoAltInt(A) ; [ redo(A(a)) ; 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 2 Con and a 2 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 i there exists an I such that: (I; I U) 2
A^
^ :(a : A+)^:(a : A ) ?; foundedWeakRepair; makeFalse U is a founded repair of A i there exists an I such that: (I; I U) 2
A^ ^ :(a : A+)^:(a : A ) ? ; foundedRepair(A) ; makeFalse
Going back to Example 2, we can now witness how, taking I to be a model of fJohn : Born u :Alive u :Deadg, the set f+Alive(John)g satisfies both of the conditions of Theorem 3. On the other hand, the set f+Alive(John); +Dead(John)g doesn’t satisfy them for any interpretation I. a = : a : static( ) ? ; [ A(a)
A2active( ) + a = [
Definition 6. Let static(aT ) ^ A be unsatisfiable. A consistent set of update actions U is a dynamic weak repair of A i there exists an I such that: (I; I
U) 2
A ? ; while :T do
aT = fhBorn u :Alive v ?; f+Alivegi; h:Alive u :Dead v ?; f+Deadgig and the ABox A = fJohn : Born u :Alive u :Deadg, whose only founded weak repair was f+Alive(John)g. There are two dynamic weak repairs of A, namely U1 = f+Alive(John)g and U2 = f+Alive(John); +Dead(John)g. 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 [ a ; Minimal(A) ? a2Ind 2aT 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 i there exists an I such that: (I; I
U) 2
A ^
^ :(a : A+) ^ :(a : A ) ? ; dynamicRepair(A) ; makeFalse
Going back to Example 3 this time we can witness how, taking I to be a model of fJohn : Born u :Alive u :Deadg, only the set f+Alive(John)g satisfies the condition of Theorem 4 whereas the set f+Alive(John); +Dead(John)g does not, for any I.
Discussion and Conclusion We have seen how di erent 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) 2 jj foundedRepair(A) jj or (I; I0) 2 jj dynamicRepair(A) jj, respectively, and setting U = f+A(a) : a : A+ I0 = I0 g [ f A(a) : a : A I0 = I0 g. The dynamic logic 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: either extract A U by reducing the formula h U ic 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 di erent 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,
we can decide the existence of each one by checking whether the formula hrepairic A
is satisfiable, where A is the initial ABox. Indeed, any interpretation that satisfies the
formula hrepairic A will be a model of at least one repaired ABox. Our approach also
comes close to the work presented in [
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 according to Definition 3, the TBox T = f9hasFather:Female v ?g can be only extended to the active TBox aT = f h9hasFather:Female v ?; ;i g. 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 powerful 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. 17. Lembo, D., Lenzerini, M., Rosati, R., Ruzzi, M., Savo, D.F.: Inconsistency-tolerant semantics for description logics. In: Web Reasoning and Rule Systems - Fourth International Conference, 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 constraints. In: Artale, A., Glimm, B., Kontchakov, R. (eds.) Proceedings of the 30th International Workshop on Description Logics, Montpellier, France, July 18-21, 2017. CEUR Workshop 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 Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press (2010), http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1931