Guillaume Feuillade

Zhanhao Xiao

Maël Valais

Usman Younus

Ezgi Martin Dieguez

Iraz Su

Julien Hay

Julien Vianey

Arianna Novaro

Maryam Rostamigiv

David Fernández-Duque

Petar Iliev

Victor David

Saul Gonzalez

Elise Perrotin

Keywords: Active Integrity Constraints, Dynamic Logic, Description Logic, Inconsistency Management, Database Repairing

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 the first part of this thesis, we review the main repairing routes that have been proposed in the literature and capture them by means of Dynamic Logic programs. The main tool we employ for our investigations is the recently introduced logic DL-PA, which constitutes a variant of PDL. We then go on to explore a new, dynamic kind of database repairing whose computational complexity and general properties are compared to the previous established approaches.

In the second part of the thesis we leave the propositional setting and pursue to adapt the aforementioned ideas to higher level languages. More specifically, we venture into Description Logics and investigate extensions of TBox axioms by update actions that denote the preferred ways an ABox should be repaired in case of inconsistency with the axioms of the TBox. The extension of the TBox axioms with these update actions constitute new, active TBoxes. We tackle the problem of repairing an ABox with respect to such an active TBox both from a syntactic as well as a semantic perspective. Given an initial ABox, the syntactic approach allows us to construct a set of new ABoxes out of which we then identify the most suitable repairs. On the other hand, for the semantic approach we once again resort to a dynamic logic framework and view update actions, active inclusion axioms and repairs as programs. Given an active TBox aT , the framework allows to check (1) whether a set of update actions is able to repair an ABox according to the active axioms of aT by interpreting the update actions locally and (2) whether an ABox A is the repair of a given ABox A under the active axioms of aT using a bounded number of computations by interpreting the update actions globally. After discussing the strong points of each direction, we conclude by combining the syntactic and semantic investigations into a cohesive approach.

Résumé

Dans la littérature sur les bases de données, il a été proposé d'utiliser des contraintes d'intégrité actives afin de restaurer l'intégrité de la base. Ces contraintes d'intégrité actives consistent en une contrainte classique augmentée d'un ensemble d'actions de mise à jour préférées qui peuvent être déclenchées quand la contrainte est violée. Dans la première partie de cette thèse, nous passons en revue les principales stratégies de réparation qui ont été proposées dans la littérature et proposons une formalisation par des programmes de la Logique Dynamique. L'outil principal que nous employons dans notre recherche est la logique DL-PA, une variante de PDL récemment introduite. Nous explorons ensuite une nouvelle façon dynamique de réparer les bases de données et comparons sa complexité calculatoire et ses propriétés générales aux approches classiques.

Dans la seconde partie de la thèse nous abandonnons le cadre propositionnel et adaptons les idées susmentionnées à des langages d'un niveau supérieur. Plus précisément, nous nous intéressons aux Logiques de Description, et étudions des extensions des axiomes d'une TBox par des actions de mise à jour donnant les manières préférées par lesquelles une ABox doit être réparée dans le cas d'une inconsistance avec les axiomes de la TBox. L'extension des axiomes d'une TBox avec de telles actions de mise à jour constitue une nouvelle TBox, qui est active. Nous nous intéressons à la manière de réparer une ABox en rapport avec une telle TBox active, du point de vue syntaxique ainsi que du point de vue sémantique. Étant donnée une ABox initiale, l'approche syntaxique nous permet de construire un nouvel ensemble d'ABox dans lequel nous identifions les réparations les mieux adaptées. D'autre part, pour l'approche sémantique, nous faisons de nouveau appel au cadre de la logique dynamique et considérons les actions de mise à jour, les axiomes d'inclusion actives et les réparations comme des programmes. Étant donné une TBox active aT , ce cadre nous permet de vérifier (1) si un ensemble d'actions de mise à jour est capable de réparer une ABox en accord avec les axiomes actifs d'aT en effectuant une interprétation locale des actions de mise à jour et (2) si une ABox A est la réparation d'une ABox donnée A sous les axiomes actifs d'aT moyennant un nombre borné de calculs, en utilisant une interprétation globale des actions de mise à jour.

Après une discussion des avantages de chaque approche nous concluons en proposant une intégration des approches syntaxiques et sémantiques dans une approche cohésive.

Motivation

One of the most important (but notoriously difficult) issues in the database and AI literature is the problem of updating a database under a set of integrity constraints. The latter are usually expressed by logical formulas and their role is to impose conditions that every state of the database must satisfy. In the course of database maintenance several changes are applied to the databases and checking whether these constraints are still satisfied is of the highest priority. When a database fails to satisfy the integrity constraints, it has to be repaired in order to restore integrity. Given a database, the procedure of repairing and restoring its consistency with respect to a set of integrity constraints has been extensively studied in the last decades [Abiteboul, 1988, Ceri et al., 1994, Bertossi, 2011]. These approaches propose several possible repairs as candidates for integrity maintenance and it seems essential to identify which types of repairs are more suitable, given the fact that the number of all possible repairs can be remarkably large. Given this, the most preva-lent have become those that are based on the minimality of change principle [Winslett, 1990, Herzig and Rifi, 1999, Chomicki and Marcinkowski, 2005]. Despite this, however, the need to have 'more informed' ways of maintaining database integrity arose.

In light of this, active integrity constraints were proposed as an extension of integrity constraints (or static constraints) with update actions, each one suggesting the preferred update method when an inconsistency arises between the database and a constraint [START_REF] Flesca | Active integrity constraints[END_REF],Caroprese et al., 2009,Caroprese and Truszczynski, 2011,Cruz-Filipe, 2014]. For example, the integrity constraint (∀X)[Bachelor(X) ∧ Married(X) → ⊥]

which says that no one should have the property of being a bachelor and married at the same time can be turned into the active 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. In the propositional case, an active integrity constraint can be represented as a couple r = C(r), R(r) where C(r) is a boolean formula (called the static part of r and denoting a static constraint) and R(r) is a set of update actions, each of which is of the form +p or -p for some atomic formula p. The idea is that (1) when C(r) is false then the constraint r is violated and (2) a violated constraint can be repaired by performing one or more of the update actions in R(r). The two most prevalent types of repairs w.r.t. a set of active integrity constraints are the founded and the justified repairs. Note that while with these methods one can greatly reduce the number of possible repairs, different choices between update actions in R(r) can still lead to different repairing routes or even no repairs at all (for example when R(r) is the empty set).

Applying the same idea to the Description Logic setting would result in the extension of the TBox axioms with preferred update actions that 'dictate' the changes that should be imposed on an ABox in order to achieve consistency with a TBox and this has not yet been directly pursued in the DL literature. It seems very natural though that sometimes ontology engineers should be given the means to easily express such preferences without having to worry that unwanted 'repairing routes' will be followed in case there is an inconsistency between an ABox and a TBox. Consider for instance the following TBox: T = {Father Male Parent, OnlyChild ∀hasSibling.⊥} and an ontology engineer being able to 'enhance' it to two possible active TBoxes, viz.

aT 1 = {η 1 , η 2 } or aT 2 = {η 3 , η 4 } where: We can witness how, through these enhanced concept inclusions, one can be more specific in the update actions that s/he prefers when repairing an ABox that is inconsistent with T : the active axioms of aT 1 dictate that an individual who is a father should remain a father in case of inconsistency, whereas an individual who has siblings should change its status and not be an only child anymore. Similarly for aT 2 , where '-hasSibling. ' removes all relations between individuals that violate the axiom and individuals satisfying (i.e., all individuals), thus stating that an only child who has siblings should drop its 'sibling' relationship with everyone and stay an only child. In practice, consider the following ABox: A = {John : Male Father ¬Parent, Mary : OnlyChild, hasSibling(Mary, John)} A repaired ABox then according to aT 1 should be the following:

A 1 = {John : Male Father Parent, Mary : ¬OnlyChild, hasSibling(Mary, John)} whereas a repaired ABox according to aT 2 should be the following:

A 2 = {John : Male ¬Father ¬Parent, Mary : OnlyChild} During the course of this thesis, we will attempt to materialize the above intuitions in a number of different formats and examine how the various definitions of repairs from the database literature translate and behave in the DL setting.

Background and State of the Art

We begin by presenting some background that is needed for the later chapters. Meanwhile, we discuss the relevant state of the art of the areas that this thesis is based on.

More specifically, we give the basics of DL-PA, a variant of Propositional Dynamic Logic that Chapter 2 is based on, give a survey of the literature on Active Integrity Constraints from their origins to later developments, as well as recall the fundamental notions of Description Logics and the most prevalent methods that exist on repairing inconsistent DL knowledge bases.

Dynamic Logic of Propositional Assignments

Dynamic Logic [Pratt, 1976, Harel et al., 2000] extends modal logic with dynamic operators that are designed to reason about the behavior of (computer) programs: each modal operator has as argument a (computer) program and allows to express facts which hold after that program is executed. Propositional Dynamic Logic PDL [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] is the 'fragment' of Dynamic Logic that deals with propositional statements.

The first studies of assignments in the context of Dynamic Logic are due, among others, to Tiomkin and Makowski and van Eijck [START_REF] Tiomkin | [END_REF]Makowsky, 1985, van Eijck, 2000]. Dynamic Logic of Propositional Assignments DL-PA is a variant of PDL that was introduced in [START_REF] Herzig | A dynamic logic of normative systems[END_REF] and was further studied in [START_REF] Balbiani | Dynamic logic of propositional assignments: A well-behaved variant of PDL[END_REF], Balbiani et al., 2014]. Evidence for its widespread applicability was provided in several recent publications, including belief update and belief revision, argumentation, planning and reasoning about knowledge [Herzig, 2014, Doutre et al., 2014, Herzig et al., 2014, Herzig et al., 2016, Cooper et al., 2016, Charrier and Schwarzentruber, 2017]. We briefly recall syntax and semantics.

Language

Consider a countable set of propositional variables (alias atomic formulas) P = {p, q, . . .}.

An update action is of the form p ← and p ←⊥, for p ∈ P. The former is the insertion of p and the latter is the deletion of p. We denote the set of all update actions by U. A set of update actions U ⊆ U is consistent if it does not contain both p ← and p ←⊥, for some p. The language of DL-PA is defined by the following grammar:

ϕ ::= p | | ⊥ | ¬ϕ | ϕ ∨ ϕ | π ϕ π ::= α | π; π | π ∪ π | π * | π c | ϕ?
where p ranges over the set of atomic formulas P and α ranges over the set of update actions U. The other boolean connectives ∧, →, and ↔ are abbreviated in the usual way.

In DL-PA, update actions are singletons and are called atomic assignments. The operators of sequential composition ";", nondeterministic composition "∪", finite iteration (the socalled Kleene star) "(.) * " and test "(.)?" are the familiar operators of PDL. The operator "(.) c " is the converse operator. The formula π ϕ is read "there is an execution of π after which ϕ is true". So e.g. p ←⊥ c (p ∧ q) expresses that p ∧ q is true after some execution of p ←⊥ c , i.e., p ∧ q was true before p was set to false. The star-free fragment of DL-PA is the subset of the language made up of formulas without the Kleene star.

Let P ϕ denote the set of variables from P occurring in formula ϕ, and let P π denote the set of variables from P occurring in program π. For example, P p ← ∪ q ←⊥ = {p, q} = P p ←⊥ q . Moreover, a literal is an element of P or the negation of an element of P and a clause is a disjunction of literals.

Several program abbreviations are familiar from PDL. First, skip abbreviates ? and fail abbreviates ⊥?. Second, if ϕ then π 1 else π 2 is expressed by (ϕ?; π 1 ) ∪ (¬ϕ?; π 2 ).

Third, the loop while ϕ do π is expressed by (ϕ?; π) * ; ¬ϕ?. The nondeterministic composition α∈U α equals fail when U is empty. Furthermore, let π + abbreviate the program π; π * . Assignments of literals to variables are introduced by means of the following two abbreviations: p ←q = if q then p ← else p ←⊥ p ←¬q = if q then p ←⊥ else p ←

The former assigns to p the truth value of q, while the latter assigns to p the truth value of ¬q. In particular, the program p ←¬p flips the truth value of p. Note that both abbreviations have constant length, namely 14. Finally and as usual in modal logic, [π]ϕ abbreviates ¬ π ¬ϕ.

Semantics

Valuations are subsets of P and are denoted by V , V 1 , V 2 , etc. The set of all valuations is therefore V = 2 P . It will sometimes be convenient to write V (p) = instead of p ∈ V and V (p) = ⊥ instead of p ∈ V . A valuation determines the truth value of every boolean formula. The set of valuations where A is true is noted ||A||. We sometimes write V |= A instead of V ∈ ||A||. The update of a valuation V by a set of update actions U is defined as:

V U = V \ {p : p ←⊥ ∈ U } ∪ {p : p ← ∈ U }
So all the deletions are applied in parallel first, followed by the parallel application of all insertions. We could as well have chosen another order of application. When U is consistent then all of them lead to the same result. In particular:

Proposition 1.1. Let {α 1 , . . . , α n } be a consistent set of update actions. Let k 1 . . . k n be some permutation of 1 . . . n . Then V {α 1 , . . . , α n } = . . . (V {α k 1 }) . . . {α kn }.

DL-PA programs are interpreted as relations between valuations. The atomic programs α update valuations in the aforementioned way and complex programs are interpreted just as in PDL by mutual recursion. Figure 1.1 gives the interpretation of formulas and programs, where • is relation composition and (.) -1 is relation inverse.

A formula ϕ is DL-PA valid iff ||ϕ|| = 2 P = V. It is DL-PA satisfiable iff ||ϕ|| = ∅. For example, the formulas p ←⊥ , p ← ϕ ↔ ¬ p ← ¬ϕ, p ← p and p ←⊥ ¬p are all valid.

Observe that if p does not occur in ϕ then ϕ → p ← ϕ and ϕ → p ←⊥ ϕ are valid. This is due to the following semantical property that is instrumental in the proof of several results involving DL-PA. Proposition 1.2. Let P be a subset of P. Suppose that P ϕ ∩ P = ∅, i.e., none of the variables of P occurs in ϕ. Then V ∪ P ∈ ||ϕ|| iff V \ P ∈ ||ϕ||.

||p|| = {V : p ∈ V } ||α|| = V 1 , V 2 : V 2 = V 1 {α} || || = V = 2 P ||π; π || = ||π|| • ||π || ||⊥|| = ∅ ||π ∪ π || = ||π|| ∪ ||π || ||¬ϕ|| = 2 P \ ||ϕ|| ||π * || = ||π|| * ||ϕ ∨ ψ|| = ||ϕ|| ∪ ||ψ|| ||π c || = ||π|| -1 || π ϕ|| = V : ∃V 1 s.t. V , V 1 ∈ ||π|| ||ϕ?|| = V , V : V ∈ ||ϕ|| and V 1 ∈ ||ϕ||
The most distinguishing feature of DL-PA though is that its dynamic operators can be eliminated (which is not possible in PDL). Just as for QBF, the resulting formula may be exponentially longer than the original formula.

Theorem 1.1 ( [START_REF] Balbiani | Dynamic logic of propositional assignments: A well-behaved variant of PDL[END_REF], Theorem 1). For every DL-PA formula there is an equivalent boolean formula.

For example, the DL-PA formula p ←⊥ (¬p ∧ ¬q) is equivalent to the formula p ←⊥ ¬p ∧ p ←⊥ ¬q, which is in turn equivalent to ∧ ¬q. Therefore, the DL-PA formula p ←⊥ (¬p ∧ ¬q) reduces to the boolean formula ¬q.

Every assignment sequence α 1 ; . . . ; α n is a deterministic program that is always executable: for a given V , there is exactly one V such that V , V ∈ ||α 1 ; . . . ; α n ||.

Moreover, the order of the α i in a sequential composition is irrelevant when the set of update actions {α 1 , . . . , α n } is consistent. The following can be viewed as a reformulation of Proposition 1.1 in terms of the DL-PA operator of sequential composition.

Proposition 1.3. Let {α 1 , . . . , α n } be a consistent set of update actions. Let k 1 . . . k n be some permutation of 1 . . . n . Then V {α 1 , . . . , α n } equals the single V such that V , V ∈ ||α k 1 ; . . . ; α kn ||.

This entitles us to use consistent sets of update actions as programs: one may suppose that this stands for a sequential composition in some predefined order (based e.g. on the enumeration of the set of propositional variables).

Finally, we end by noting that both satisfiability and model checking problems of DL-PA are PSPACE-complete [START_REF] Balbiani | DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE[END_REF]. We will make extensive use of DL-PA in Chapter 2 whose results are based on the definitions and contents of this Background section. Furthermore, almost all of the logics defined in the remaining chapters are influenced and inspired by DL-PA.

Active Integrity Constraints

Active Integrity Constraints (AICs) originate from the observation that, in the course of database maintenance, a designer may want to express preferences between the various repairs that a database may be the subject of. Therefore, AICs were introduced in [START_REF] Flesca | Active integrity constraints[END_REF] as an extension of (static) integrity constraints with preferred update actions that enforce specific repairing routes when updating a database. For instance, the integrity constraint:

∀(E, S 1 , S 2 )[Employee(E, S 1 ) ∧ Employee(E, S 2 ) → S 1 = S 2 ]
which denotes the fact that every employee should only have one salary can be extended into the active constraint:

∀(E, S 1 , S 2 )[Employee(E, S 1 ) ∧ Employee(E, S 2 ) ∧ S 1 > S 2 → -Employee(E, S 1 )] which states that if there is an employee with two salaries then the preference is to remove the highest salary (instead of removing one randomly). In the paper the authors define founded repairs for the first time. The idea is that any update action applied to the database should be supported by the 'active part' of an AIC, i.e., by a preferred update action of a violated constraint. They also obtain complexity results for the problem of existence of founded repairs, both in the general case (Σ 2 P -complete) as well as in the case that AICs comprise 'single heads', i.e., only one preferred update action is allowed in each constraint (NP-complete). Recognizing that the existence of founded repairs is not always guaranteed though, they go on to define preferred repairs as an intermediate repairing route between founded and standard repairs that always exist. The complexity for the problem of existence of preferred repairs is shown to be Σ 2 P -complete. Further research on AICs also ensued [START_REF] Caroprese | Declarative semantics of production rules for integrity maintenance[END_REF], Caroprese et al., 2009] that reviewed and expanded upon the aforementioned results.

The first new definitions on repairing procedures that are based on preferences between update routes came in [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], an attempt to relate the seemingly different approaches to AICs and revision programming. There, the authors distinguish between the various repairs that they propose (standard repairs, founded repairs, justified repairs) and their weaker versions (weak repairs, founded weak repairs, justified weak repairs), with only the former complying to the minimality of change principle that the previous approaches took by default. The definitions of justified weak repairs and justified repairs were introduced as a response to the so-called circularity of support defect that founded repairs cannot evade and which the authors argue against. Furthermore, they leave the first-order setting of the previous papers and use a propositional one.

We will have a close and thorough look at all of these definitions in Chapter 2, which we'll examine from the perspective of DL-PA, and the propositional setting of [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF] will provide a valuable stepping stone to present and discuss our own approach. Another distinguishing feature in their work is that they investigate properties of normalization, i.e., 'breaking' all active integrity constraints into many copies such that each one has at most one preferred update action. They denote the differences that exist in these two different classes of AICs, both in practice (resulting in more or fewer repairs) as well as in the complexity of deciding the existence of repairs under normal AICs. The consensus on complexity results is very interesting, with all of the different kinds of repairs, being either weak or minimal, and being applied on either normal AICs or standard AICs, to fall either on the NP-complete or Σ 2 P -complete territory.

Last but not least, further approaches to refine or extend active integrity constraints have been investigated in [START_REF] Cruz-Filipe | Computing repairs from active integrity constraints[END_REF], Cruz-Filipe, 2014] with analyses of algorithms on trees, extensions to knowledge bases outside databases, as well as independence/precedence relations among active integrity constraints.

Description Logic

Description Logic (DL) is an important subfield of Logic-based Knowledge Representation (KR) that provides delicate ways to represent and reason about knowledge through the use of expressive but decidable families of languages [START_REF] Baader | The Description Logic Handbook: Theory, Implementation, and Applications[END_REF]. These logics lie between basic propositional logic and first-order logic, providing a balance between expressiveness of the language and complexity of the various reasoning tasks.

The decidable nature of DLs and the efficient algorithms that have been developed for reasoning with many of them play a vital role in plenty of applications that take advantage of their more expressive languages to deal with important real-life tasks, with an emphasis on medical ontologies [Baader et al., 2006, Rector andRogers, 2006] and the Semantic Web [START_REF] Baader | Description logics as ontology languages for the semantic web[END_REF]. Although not a new area of research, DLs enjoy an ever-increasing attention by researchers in the field of KR with new promising directions emerging and improving the state of the art continuously.

In Description Logics, a knowledge base KB = (T , A) consists of a TBox T and an ABox A. The TBox, also called the terminology, contains intensional knowledge, i.e, general knowledge, in the form of (inclusion) axioms that describe general properties of the concepts and their relationship. The ABox, also called the assertional box, contains extensional knowledge, i.e., specific knowledge, in the form of (assertional) axioms that describe specific properties of the individuals of the domain. It is important to note early from this stage that the axioms of the TBox are intended to describe 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. Modifications of the ABox may lead to inconsistencies with regard to TBoxes and repairing an ABox that is inconsistent with a TBox is a standard task [START_REF] Lembo | Inconsistency-tolerant semantics for description logics[END_REF], Bienvenu et al., 2014, Bienvenu et al., 2016].

We go on to present the syntax and semantics of some of the most important and wellstudied families of DL-languages, four of which will be the basis of our investigations in Chapters 3, 4 and 5. In DLs, the atomic elements from which the languages are built are the atomic concept names, the atomic role names and the individual names. Using these together with the concept and role constructors that each description language deploys, we can inductively build all complex concept and role descriptions available in the language. We begin with the basic description language AL, whose concept descriptions are built inductively by the following grammar:

C ::= A | | ⊥ | ¬A | C C | ∀r.C | ∃r.
where A is an atomic concept name and r is an atomic role name. The concept constructor ∀r.C is called value restriction while the concept constructor ∃r. is called limited existential quantification. Note that there are no individual names, no role constructors and that negation is only applied to atomic concept names. When it is applied to any arbitrary concept description, then the (more expressive) description language is called ALC (where C stands for complement). In ALC the union of concepts (C C) as well as full existential quantification (∃r.C) become expressible, since the former is an abbreviation of ¬(¬C ¬C) while the latter is an abbreviation of ¬∀r.¬C. Further concept constructors include the number restrictions ≥ nr (at-least restriction) and ≤ nr (at-most restriction)

for any natural number n and role r, the one-of constructor {a 1 , . . . , a n } where a 1 , . . . , a n are individual names, as well as the fills constructor r : a where r is a role and a an individual name. The language ALC extended with the one-of constructor is called ALCO and concepts of the form {a} for any individual name a are called nominals. Last but not least, important role constructors comprise the role inverse, usually written as r -but we will denote it by r c so as to keep the notation uniform with the converse operator of DL-PA throughout the chapters, as well as the intersection of roles r r, the union of roles r r, the complement of roles ¬r, the composition of roles r • r and finally the transitive closure of roles r + , where r is any atomic role name. We also mention the universal role r U which we will come across and use in later chapters. The languages ALC and ALCO extended with the role inverse constructor are called ALCI and ALCIO, respectively, whereas L(U) denotes any language L which also includes the universal role. For example, the concept descriptions of ALCIO(U) are built inductively by the following grammar:

C ::= A | | ⊥ | {a} | ¬C | C C | C C | ∀r.C | ∃r.
where A is an atomic concept name, a is an individual name and r is a (possibly inverse) atomic role name or the universal role r U .

Having given an overview of the various concept and role constructors that are used to build complex concept and role descriptions, the next step is to present the semantics of each one which provides a formal description of the job each constructor is intended to do. We begin by defining the interpretations I to comprise a non-empty set ∆ I , which denotes the domain or universe of the interpretation, and an interpretation function • I that maps each atomic concept A to a subset of the domain, each role r to a binary relation on the domain and each individual a to an element of the domain, i.e., A I ⊆ ∆ I , r I ⊆ ∆ I × ∆ I and α I ∈ ∆ I . We say that I has the unique name assumption (UNA) if α I = b I whenever a and b are distinct individual names. The extension of • I to complex concept descriptions for the basic description language AL is defined inductively as follows:

I = ∆ I ⊥ I = ∅ (¬A) I = ∆ I \ A I (C D) I = C I ∩ D I (∀r.C) I = {a ∈ ∆ I | for all b ∈ ∆ I , if (a, b) ∈ r I then b ∈ C I } (∃r. ) I = {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I }
whereas the remaining concept and role constructors have the following semantics:

(¬C) I = ∆ I \ C I (C D) I = C I ∪ D I (∃r.C) I = {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I and b ∈ C I } (≥ nr) I = {a ∈ ∆ I | card({b | (a, b) ∈ r I }) ≥ n} (≤ nr) I = {a ∈ ∆ I | card({b | (a, b) ∈ r I }) ≤ n} {a 1 , . . . , a n } I = {a I 1 , . . . , a I n } (r : a) I = {b ∈ ∆ I | (b, a I ) ∈ r I } (r c ) I = {(b, a) ∈ ∆ I × ∆ I | (a, b) ∈ r I } (r s) I = r I ∩ s I (r s) I = r I ∪ s I (¬r) I = ∆ I × ∆ I \ r I (r • s) I = {(a, c) ∈ ∆ I × ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I and (b, c) ∈ s I } (r + ) I = i≥1 (r I ) i r I U = ∆ I × ∆ I
The TBoxes are composed of terminological axioms which have two forms: either Apart from the syntax, semantics and reasoning tasks of the various DL languages, we now review some of the most widespread methods to repair inconsistencies in DL knowledge bases. As we will see in later chapters, our approach to the problem of repairing inconsistent KBs is by updating ABox assertions in order to comply with (preferred update actions indicated by) the TBox axioms, which is a research avenue that has not been directly pursued in the DL literature. The related (and most prominent) approaches to repairing KBs are mainly based on the so-called justifications, which are minimal subsets of the KB containing the terminological and assertional axioms from which an undesirable consequence is inferred. Axiom pinpointing through justifications became an important topic of research within the DL community and several results were quickly established [START_REF] Schlobach | Non-standard reasoning services for the debugging of description logic terminologies[END_REF], Kalyanpur et al., 2007, Suntisrivaraporn et al., 2008]. Both black-box [Schlobach et al., 2007, Baader andSuntisrivaraporn, 2008] and glass-box [START_REF] Parsia | Debugging OWL ontologies[END_REF], Meyer et al., 2006] methods emerged for computing justifications. The former have a more universal approach and are used independently of the reasoner at hand, while the latter have a more delicate construction that is tied to specific reasoners and usually require less calls. After computing all justifications of an undesirable consequence, the next step is to obtain a minimal hitting set [Reiter, 1987] made up of one axiom per justification and remove it from the knowledge base. More recent approaches though have focused on providing methods for weakening the axioms instead of removing them, since the latter can prove to be too big of a change [START_REF] Troquard | Repairing ontologies via axiom weakening[END_REF].

On another front, since we will be using dynamic procedures to obtain results in the DL setting, it is worth recalling the interplay between PDL (and various extensions) with Description Logics admitting regular expressions over roles. The mapping that established a translation from one to the other helped both disciplines in obtaining decidability and complexity results that were until then non-existent. For an overview on the matter see the handbook [START_REF] Baader | The Description Logic Handbook: Theory, Implementation, and Applications[END_REF]. More recent related work in reducing dynamic problems to static DL reasoning includes [START_REF] Ahmetaj | Managing change in graph-structured data using description logics[END_REF] which also makes use of integrity constraints in rich DLs. Speaking of integrity constraints, we end by mentioning that approaches to encode integrity constraints into TBoxes already exist, with the most prominent ones being based on extending the KBs with constraint axioms. These axioms however are used for validation purposes only and do not share the same semantics as regular TBox axioms [START_REF] Motik | Bridging the gap between OWL and relational databases[END_REF], Tao et al., 2010].

Contributions and Outline of the Thesis

As we have mentioned before, the main goal in this thesis is to apply the idea behind active integrity constraints in the Description Logic setting and, in particular, to provide extensions of TBox axioms so that they are able to suggest preferred repairing routes in case of inconsistencies. Before attempting this though, we begin in Chapter 2 with an overview of static and active integrity constraints, investigated through DL-PA in the propositional setting. We give the details of weak, founded and justified repairs that we skipped in Section 1.2.2 and present embeddings of each one into DL-PA. The most important contribution of the chapter though is the definition of dynamic repairs which constitute a new, dynamic way of integrity maintenance and which was recently proposed in [START_REF] Feuillade | A dynamic view of active integrity constraints[END_REF]. After an analysis of their properties and a comparison to the other established repairs of the literature, we provide complexity results for the problem of existence of these new repairs. We then take advantage of the dynamic framework that we use (the logic DL-PA) in order to explore an extension on databases with history and adjust the behavior of the various repairs so that they work in this setting. Finally, for all these definitions we provide DL-PA counterparts of reasoning and decision problems, such as the existence of a repair or the existence of a unique repair. Chapter 2 is based on [START_REF] Feuillade | A dynamic logic account of active integrity constraints[END_REF].

Lifting the idea behind AICs to Description Logics starts in Chapter 3, where the first definition of 'active' TBoxes is introduced. After a brief discussion on the differences and difficulties of leaving the propositional setting, we examine preliminary steps into repairing ABoxes syntactically so that they conform to the preferences denoted by the active axioms. These syntactic repairs are inspired by (and correspond to) the weak and founded repairs of the database literature. Proving to be quite impractical though, we suggest that a semantic approach seems more viable and venture into tackling the limitations of such a syntactic approach in the subsequent chapters. Chapter 3 is based on [START_REF] Rantsoudis | Repairing ABoxes through active integrity constraints[END_REF].

In the following two chapters we go on to pursue this semantic approach and, more specifically, investigate how the dynamic logic-based framework and methods used in Chapter 2 behave in the DL level. Chapter 4 uses a more local approach, where preferred update actions in the active axioms behave similarly to the update actions introduced before, i.e., they have the form ±A for an atomic concept A denoting either the addition or the removal of an individual from the set of individuals that have property A. This approach, although more expressive and well-behaved than the syntactic one of Chapter 3, still leaves a lot of repairing scenarios unattainable, mainly because of its boolean nature and close similarity to the repairs of the database literature. On the other hand, Chapter 5 introduces and discusses a more elaborate logic and techniques which apply changes globally, in the sense that preferred update actions of the form ±C can be applied to all individuals violating an axiom and C is not necessarily atomic. Again, both of these semantic approaches use a dynamic logic framework, influenced by the logic DL-PA already showcased in Chapter 2. Furthermore, although the resulting logics are extensions of ALCO and ALCIO respectively with dynamic operators, they are shown to be as expressive as their static counterparts (with the addition of the universal role). The results on Chapter 4 are based on [START_REF] Feuillade | A dynamic extension of ALCO for repairing via preferred updates[END_REF], whereas the results on Chapter 5 have not been published at the time of writing.

The thesis concludes in Chapter 6 with a summary of the work presented and a proposal to connect the approaches of the (syntactic) Chapter 3 and the (semantic) Chapter 5, thus completing the picture on active TBox-based ABox repairs. We also briefly discuss future work, with possible applications of the proposed repairing methods on nonmonotonic scenarios in an attempt to combine the results of this thesis with different areas of research that I've also been involved in (see the next section).

Other Contributions

In this section I briefly discuss research that I've conducted in parallel to what is reported in this thesis. The main theme of several research areas and applications, as well as of the work presented here, revolves around the search for consistency. Although we generally want consistency, it is true that in real life we tend to live with inconsistencies in the sense that a big part of the conclusions we draw is defeasible. The second line of work I was involved in deals with notions of defeasibility since one of my main interests lies on nonmonotonic reasoning and in particular on conditional logics of normality. Before delving into any details though, a general description of this research filed immediately follows.

Nonmonotonic Logics. One of the major goals in AI is to develop tools that bridge the gap between human commonsense reasoning and artificial reasoning of rational agents (like computers or robots). In this regard, nonmonotonic ways to reason about knowledge are extensively studied and developed since their connection with commonsense reasoning is apparent: it is true for a human agent that a seemingly plausible conclusion can be later retracted in the light of new information (defeasible inferences) and in most real-life scenarios reasoning is conducted with only incomplete information. Classical (Mathematical) Logic cannot deal with these situations since it is inherently monotonic. Thus, nonmonotonic logics (like autoepistemic or conditional logics) were devised to capture default reasoning in the way described above, extending classical logic and providing a formal mathematical framework through which knowledge can be represented and inferred using nonmonotonic procedures. An exciting and mature research field, it always remains relevant in the era that AI flourishes and its connection to emerging areas of research (like machine learning) looks promising and essential. [START_REF] Crocco | Conditionals: From Philosophy to Computer Science[END_REF] for a broad overview of applications); they represent different linguistic constructions with a common structural form ('if ... then') and the aim of the field is to provide a unifying formal logical account that accurately captures their essential meaning.

Conditional Logics of Normality. Artificial Intelligence has been interested in conditional logics for default reasoning already from the '80s (see the work of J. Delgrande [Delgrande, 1987,Delgrande, 1988]), in counterfactual conditionals (M. Ginsberg, [Ginsberg, 1986]) and in the 'normality conditionals' in nonmonotonic reasoning [Bell, 1990, Lamarre, 1991, Boutilier, 1992]. The reader is referred to the handbook article of J. Delgrande [Delgrande, 1998] for a broad overview of conditional logics for defeasible reasoning. The investigations on the intimate relation of conditional logics to nonmonotonic reasoning have been further triggered by the seminal work of S. Kraus, D. Lehmann and M.

Magidor [Kraus et al., 1990,Lehmann and[START_REF] Lehmann | [END_REF], whose framework (KLM) has become the 'industry standard' for nonmonotonic consequence relations. There exist various possible-worlds semantics for conditional logics (see [Nute, 1980,Delgrande, 1998])

and a connection to modal logic (known from D. Lewis' work [Lewis, 1973]) which has been further explored by the modal construction of 'normality conditionals' [Lamarre, 1991, Boutilier, 1992].

A logic of 'normality conditionals' for default reasoning attempts to pin down the principles governing the statements of the form 'if A, then normally B is the case'. 'Normally' is susceptible to a variety of interpretations. One is based on a 'normality' ordering between possible worlds: (A ⇒ B) is true if it happens that in the most 'normal' (least exceptional) A-worlds, B is also true [Lamarre, 1991, Boutilier, 1992]. Another, more recent one [Jauregui, 2008] interprets 'normally' as a 'majority' quantifier: (A ⇒ B) is true iff B is true in 'most' A-worlds. Questions of 'size' in preferential nonmonotonic reasoning have been firstly introduced by K. Schlechta [Schlechta, 1995, Schlechta, 1997];

the notion of 'weak filter' that emerged (as a 'core' definition of a collection of 'large' subsets) has been also employed in modal epistemic logics [START_REF] Askounis | Knowledge means 'all', belief means 'most[END_REF].

A majority-based account of default conditionals depends heavily on what counts as a 'majority' of alternative situations, what is a 'large' set of possible worlds. It is difficult to state a good definition that would work for both the finite and the infinite case; the notions of weak filters and weak ultrafilters that have been used capture the minimum requirements of such a notion [Schlechta, 1997, Jauregui, 2008]. In [Koutras andRantsoudis, 2015, Koutras andRantsoudis, 2017], we experimented with a notion of 'overwhelming majority', combined with the widely accepted intuition that (A ⇒ B) should mean that (A ∧ B) is more plausible than (A ∧ ¬B). We defined conditionals of this form to (essentially) mean that (A ∧ B) is true in 'almost all' (in the mathematical sense, i.e., in 'all but finitely many') points in the countable modal frame (ω, <) (the first infinite ordinal, strictly ordered under <), whose modal axiomatization (the normal modal logic K4DLZ) is known as the 'future' fragment of the temporal logic of discrete linear time [Goldblatt, 1987, Segerberg, 1970]. This majority conditional is modally defined and this readily provides a decision procedure, as a modal translation of conditional formulas can be checked for validity in (ω, <) using any of the proof procedures known for K4DLZ. We examined the properties of this conditional, in particular with respect to the (conditional incarnation of the) 'conservative core' of defeasible reasoning set by the KLM framework. The paradigm of 'overwhelming majority' in our work is consistently represented with cofinite subsets of ω. En route, we discuss variants: trying cofinal (rather than cofinite) subsets of ω, and/or varying the modal definition of the conditional connective. Then, we discuss the possibility of defining conditionals over cofinite subsets of ω in the neighborhood semantics for conditional logics; we prove that the conditionals defined can be very weak, even compared to the conditionals introduced in [Delgrande, 2006].

Our main goal in these papers was to identify a set of 'normality' principles that would possibly characterize a majority-based account of default conditionals, given that the 'cofinite vs. finite' intuition is undeniably a widely acceptable case in the 'big vs.

small' question, and to delineate the limits of such an approach. In addition, we decided to exploit the well-known (and well-behaved) machinery of modal logic which allowed us to obtain definitions of cofinite sets of possible worlds in (ω, <), resulting in logics with an NP-complete satisfiability problem. We have also experimented with logics defined on appropriately populated Scott-Montague frames obtaining relatively weak logics, something not entirely unexpected in this area (see [Delgrande, 2006] for weak conditionals constructed under a rule-based interpretation of defaults). A more fine-grained and elaborate approach came in [START_REF] Koutras | Default reasoning via topology and mathematical analysis: a preliminary report[END_REF] (typically, mostly) fly'. It has been noticed however that "the reading 'a bird that can be consistently assumed to fly does fly' is clearly epistemic in nature" [Delgrande, 2012, p. 95]. The reader should consult the recent paper [Delgrande, 2012] for a deep technical and philosophical discussion on the content, the nature and the role of default statements in Commonsense Reasoning and the pros and cons of using conditional logic to capture their content.

That the defeasible conditionals (or at least, some of them) clearly have an epistemic interpretation, has been noticed early enough, implicitly or explicitly. A 'normality statement' of the form 'every Tuesday afternoon, you can find Jimmy taking a beer in the corner pub' allows one to infer that on a 'regular' Tuesday s/he can meet Jimmy there and this default inference involves facts known ('it is a Tuesday'), facts observed and believed ('Jimmy frequents this place on Tuesday afternoon'), facts considered to be consistent with the belief base ('there is no reason to believe this is an 'irregular' Tuesday') and facts plausibly inferred ('most probably I will meet him there'). Although it is difficult to agree on the subtle details of the epistemic attitudes involved, it seems that there is an agreement on the fact that such a description is quite reasonable. Such cognitive statements are implicit in Reiter's normal defaults [Reiter, 1980] and the conditional entailment of H. Geffner and J. Pearl [START_REF] Geffner | Conditional entailment: Bridging two approaches to default reasoning[END_REF]: 'a rule a : b b may be seen as a soft constraint for believing b when a is known, while a conditional rule a ⇒ b can be viewed as a hard constraint to believe b in a limited context defined by a and possibly some background knowledge' [Eiter and Lukasiewicz, 2000, p. 220].

The study of the connection of defeasible (and perhaps other sorts of) conditionals with the area of Epistemic and Doxastic Logic has not been hitherto pursued in its full entirety. In general, the 'conditionals-via-modal-logic' technique is known and quite successful [Lewis, 1973, Chellas, 1975]; yet, the technical and philosophical step to the construction of conditionals via Epistemic Logic-or the integration of epistemic logic and conditional logic-has not been fully taken. The relation of Epistemic Logic to conditionals mainly revolves around the famous Ramsey test and this is also apparent in the earlier works of P. Lamarre & Y. Shoham [START_REF] Lamarre | Knowledge, certainty, belief, and conditionalisation (abbreviated version)[END_REF] or N. Friedman & J. Halpern [START_REF] Friedman | Modeling belief in dynamic systems, part I: foundations[END_REF] where an interesting notion of conditional belief is based on the semantics of default conditionals (see also [Aucher, 2014, p. 107]).

Modal approaches to defeasible conditionals [Lamarre, 1991, Boutilier, 1992, Boutilier, 1994, Delgrande, 2006] are mostly based on the model-theoretic intuition of 'preference' among possible worlds or propositions (overall, the 'preferential approach' to nonmonotonic logics and to logics of 'typicality' has been very influential, see [START_REF] Britz | Preferential reasoning for modal logics[END_REF] for a recent application). The conditional ϕ ⇒ ψ is true in a possible world if ψ is true in the most 'normal' or 'preferred' accessible ϕ-worlds; equivalently, given the context of ϕ, the proposition expressed by ϕ ∧ ψ is preferred over the one expressed by ϕ ∧ ¬ψ [Delgrande, 2006]. It is natural to consider that normality orderings are preorders (reflexive and transitive relations) and thus the modal approaches to defeasible conditionals usually employ the logic S4 (or its extension S4.3) within which the defeasible conditional is modally defined [Boutilier, 1992].

In [Koutras et al., 2017a,Koutras et al., 2019], we amplify the epistemic interpretation of defeasible conditionals and proceed to define them directly within Epistemic Logic. We work inside KBE, a recently introduced epistemic logic [Koutras et al., 2017b] accounting for knowledge, belief and estimation (as a form of weak, complete belief, interpreted as 'truth in most epistemic alternatives'). KBE comprises a S4.2 framework for knowledge and belief, following the fundamental investigations of W. Lenzen [Lenzen, 1978] who advocated it as the 'correct' logic of knowledge; note that R. Stalnaker arrived at a similar proposal via different assumptions [Stalnaker, 2006]. The non-normal modal operator for estimation is interpreted as a majority quantifier over the set of epistemic alternatives of a given possible world. The formal apparatus is that of a weak ultrafilter, which is an upwards-closed collection of sets, with pairwise non-disjoint members and such that exactly one out of a set and its complement occurs in the collection; the notion extends the weak filters introduced in [Schlechta, 1997] andlater, independently, in [Jauregui, 2008]. We define three nonmonotonic conditionals by capturing a size-oriented version of the fundamental intuition of normality conditionals: ϕ ⇒ ψ is set to mean that ϕ ∧ ψ is more normal compared to ϕ ∧ ¬ψ, as it holds in 'most' epistemically alternative worlds; this is achieved by exploiting the nature of KBE's 'estimation' operator as a majority quantifier. The logics emerging are rather weak compared to the 'conservative core' of default reasoning (the system P, [START_REF] Kraus | Nonmonotonic reasoning, preferential models and cumulative logics[END_REF]) but this is neither surprising nor discouraging: weak conditionals of this kind have been also introduced in [Delgrande, 2006, system C and system Λ] under a rule-based interpretation of defaults and it is wellknown that conditionals based on the plausibility structures of N. Friedman & J. Halpern do not generally satisfy all the KLM properties [Friedman and Halpern, 1997, p. 266].

Another, very 'natural' (but rather strong in epistemic assumptions) translation leads to a weak monotonic conditional, and two other epistemic definitions give rise to nonmonotonic conditional logics which do not satisfy the axiom ID (reflexivity), but they capture very interesting conditional principles and one of them comes close to the 'overwhelming majority' conditional defined in [START_REF] Koutras | In all but finitely many possible worlds: Model-theoretic investigations on 'overwhelming majority' default conditionals[END_REF]. Note that for all these definitions a recursive translation in the language of KBE provides direct access to the tableaux proof procedure for this logic [Koutras et al., 2017b], and thus a machinery for testing theoremhood is readily available. It should also be noted that analytic tableaux exist for KLM logics and the tableaux procedure is constructed via a modal encoding of nonmonotonic conditionals [START_REF] Giordano | Analytic tableaux calculi for KLM logics of nonmonotonic reasoning[END_REF].

There exist two main directions in employing Conditional Logic in Knowledge Representation. The first -and perhaps more influential one -asks for devising mechanisms which will reveal the contingent conclusions that can be plausibly extracted given a background conditional (default) theory. The second responds to the objective of introducing axiomatic ways to account for a precise notion of default conditional and devise theories that capture the basic properties of a defeasible conditional, in as much the same way it has been achieved for indicative or counterfactual conditionals; see J. Delgrande's handbook article [Delgrande, 1998] for further analysis. In these papers, we took the second direction. We focused on the 'epistemic connection' of defeasible conditionals and investigated the possibility of a direct syntactic definition within Epistemic Logic; the intension was to check the potential of such an approach, whose rewarding benefits are more than obvious.

We will come back to the realm of nonmonotonic reasoning in Chapter 6, where we briefly mention possible future connections between the results reported in this thesis and defeasible inferences.

CHAPTER 2 would check each active constraint at a time and apply an update action before repeating seems able to do so. Indeed, as we will witness in Section 2.5.2, the set {+D 1 , +D 2 } will be the only solution using such a dynamic procedure. Note also that a repair which conforms to the minimal change principle would suggest that {+D 2 } should be the only repair. While this is indeed the only minimal solution, it can be argued that it should not be the case that this employee was assigned to D 2 directly, without having worked on D 1 first.

A
Just as in [Caroprese andTruszczynski, 2011, Cruz-Filipe, 2014] we only consider ground constraints in the current chapter, i.e., we work with a propositional language.

Due to this, static constraints will be represented by boolean formulas and, as we have mentioned in Section 1.1, an active integrity constraint will be a couple r = C(r), R(r)

where C(r) is the static constraint and R(r) is the set of preferred update actions. In this chapter we examine active integrity constraints in the framework of dynamic logic and argue that they can be viewed as particular programs: the sequential composition of the test of ¬C(r) and the nondeterministic choice of an action in R(r). Repairing a database can then be done by means of a complex program that combines active integrity constraints. We use DL-PA, the simple yet powerful dialect of dynamic logic we introduced in Section 1.2.1. We recall that, instead of PDL's abstract atomic programs, the atomic programs of DL-PA are update actions: assignments of propositional variables to either true or false, written p ← and p ←⊥. Just as in PDL, these atomic programs can be combined by means of program operators: sequential and nondeterministic composition, finite iteration and test. The language of DL-PA has not only programs, but also formulas.

While DL-PA programs describe the evolution of the world, DL-PA formulas describe the state of the world. In particular, formulas of the form π ϕ express that ϕ is true after some possible execution of π, and [π]ϕ expresses that ϕ is true after every possible execution of π. The models of DL-PA are considerably simpler than PDL's Kripke models:

valuations of classical propositional logic are enough. The assignment p ← inserts p, while the assignment p ←⊥ deletes p. Apart from being simple yet quite expressive, its biggest computational advantage over PDL comes in the form of the elimination of the Kleene star: it is shown in [START_REF] Herzig | A dynamic logic of normative systems[END_REF], Balbiani et al., 2013] that every DL-PA formula can be reduced to an equivalent boolean formula (something that is not possible in PDL). This is an important attribute and a very useful tool, as it will allow us to construct repaired databases syntactically. The most significant advantage of using a dynamic logic framework though is the fact that we can easily study extensions (like the historybased repairs of Section 2.7) that are expressible in the language by simply extending the formulas in the appropriate ways.

The chapter is organized as follows. In Section 2.2 we provide a thorough background on static and active constraints, as well as the associated repairs for both (weak repairs, PMA repairs, founded and justified repairs). In Section 2.3 we provide an embedding of the associated repairs of static constraints (weak repairs and PMA repairs) into DL-PA. In Section 2.4 we do the same for the associated repairs of active constraints (founded and justified repairs). Section 2.5 comprises the main contribution of the chapter: we propose some new definitions of repairs in terms of while programs and compare them with the aforementioned founded and justified repairs in various aspects. Their computational complexity is investigated in Section 2.6. In Section 2.7 we push the envelope of the active constraint paradigm and examine databases with history as well as how the various repairs are integrated in their framework. Finally, Section 2.8 concludes with some examples of related reasoning problems and a brief discussion on future work.

This chapter extends [START_REF] Feuillade | A dynamic view of active integrity constraints[END_REF] by the analysis of justified repairs, a thorough discussion on the dynamic repairs introduced as well as how they compare with the available repair procedures from the literature, a complexity analysis and a look into databases with history.

Background

The basic definitions and properties of DL-PA have already been introduced in Section 1.2.1. We only note that:

(1) In the context of the present chapter a valuation is called a database.

(2) We sometimes use X as a metavariable for and ⊥ and write p ←X.

(3) For subsets P of P it will be convenient to write P ← to denote the set of update actions {p ← : p ∈ P }, and likewise for P ←⊥.

In the following subsections, we recall the definitions of the various repair procedures w.r.t. static and active integrity constraints.

Static Constraints and the Associated Repairs

In this subsection we consider the classical notion of database integrity that is defined in terms of static integrity constraints, or static constraints for short. In our propositional language they are nothing but boolean formulas. Two ways of repairing databases based on such constraints can be found in the literature [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF].

Both consist in first finding an appropriate set of update actions U and then building the update V U of V by U as defined in Section 1.2.1. We relate them to well-known operations in belief revision and update [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF], which allows us to reuse their embeddings into DL-PA [Herzig, 2014].

Weak Repairs and Drastic Updates

Let V be a database, U a set of update actions and C a set of static constraints, i.e., a set of boolean formulas. In the rest of the chapter we will only consider finite sets of static constraints. We say that U is relevant w.r. Proposition 2.1. Let V be a database and let C be a set of static constraints. Then:

V U : U is a weak repair of V achieving C = C
Note that a weak repair may contain assignments of variables that do not occur in C.

To witness, in the above example {p ← , q ← , r ← } is a weak repair of V achieving C. To remedy this we consider every weak repair U from now on to be such that if p ← or p ←⊥ occurs in U then p ∈ P C . This corresponds to a very basic update semantics that is sometimes called Winslett's standard semantics [Winslett, 1990, Herzig and[START_REF] Herzig | [END_REF].

Repairs Tout Court and their Relation to Winslett's PMA

We now present the definition of a repair which, as we already mentioned, uses the principle of minimal change to produce repair solutions that are considered more practical in contrast to the more general weak repairs.

Definition 2.2. Let V be a database and let C be a set of static constraints. A repair of V achieving C is a weak repair of V achieving C that is minimal w.r.t. set inclusion: there is no weak repair of V achieving C that is strictly contained in it.

The next example is a follow-up to Example 2.1.

Example 2.2. Let V = ∅ and C = {p∨q}. There are exactly two repairs of V achieving C, viz. {p ← } and {q ← }.

We are now going to relate repairs to Winslett's possible models approach PMA [Winslett, 1988, Winslett, 1990]. Remember that the update of a database V by a boolean formula A according to the PMA is the set of valuations V such that V |= A and such that the symmetric difference between V and V is minimal w.r.t. set inclusion. Formally, the symmetric difference is defined as D(V , V ) = {p : V (p) =V (p)} and the PMA update of V by A is the set:

V : V |= A and there is no V ∈ ||A|| such that D(V , V ) ⊂ D(V , V )
For example, the PMA update of ∅ by p∨q is {p}, {q} and the PMA update of ∅ by (p∧q)∨r is {p, q}, {r} .

Proposition 2.2. Let V be a database and let C be a set of static constraints. Then:

V U : U is a repair of V by C is the PMA update of V by C
The above result justifies the term PMA repair that we are going to employ henceforth (because the mere term 'repair' might lead to confusions).

Active Constraints and the Associated Repairs

Active integrity constraints were proposed more than ten years ago [START_REF] Flesca | Active integrity constraints[END_REF] and various ways of repairing a database V by such constraints were studied in the literature. Just as for static constraints, all definitions are based on the notion of a repair set:

an appropriate set of update actions U such that V U no longer violates the integrity constraints. V U is once again the result of updating V by U as defined in Section 1.2.1

and is called the repaired database.

In the present subsection we recall syntax and semantics of the two main routes that have been explored in the literature.

Active Integrity Constraints

An active integrity constraint (or active constraint for short) combines a static integrity constraint with a set of preferred repair actions.

Definition 2.3. An active constraint is a couple r = C(r), R(r) , where C(r) is a boolean formula and R(r) is a finite set of update actions that is consistent.

As before, C(r) is a static integrity constraint that is violated when C(r) is false. If this is the case and R(r) = ∅ then r is applicable and R(r) indicates how to get rid of the violation and restore integrity. The elements of R(r) are viewed as permitted update actions: when C(r) is violated then each of the actions in R(r) gets a 'license to update'. This is a rather imprecise description of the job the update actions in R(r) are expected to do and in the literature various semantics were proposed. One of the most prominent of them are founded repairs which make use of the foundedness condition in order to apply the correct update actions, while justified repairs build upon and refine this condition in order to tackle the so-called circularity of support issue that can be witnessed by founded repairs.

We say that an active constraint r = C(r), R(r) is standard if C(r) is a clause and each update action in R(r) makes one of the literals of C(r) true: if p ← ∈ R(r) then p has to be one of the literals of C(r) and if p ←⊥ ∈ R(r) then ¬p has to be one of the literals of C(r).

Remark 1. The definition in the literature differs in several respects from ours here. First, C(r) is usually not viewed as a static integrity constraint but as the negation of a static integrity constraint: r is violated when the first argument of r is true. Second, active constraints are noted C(r) → R(r), which makes them look like formulas. However, "→" is different from material implication as the right hand side of the implication is not a formula but a set of programs. So their semantics remains to be given: in the literature this is typically done by means of disjunctive logic programs under a non-monotonic semantics. Third, all active constraints have to be standard.

We denote finite sets of active constraints by η, η 1 , etc. The set of static integrity constraints associated with η is defined as

C(η) = {C(r) : r ∈ η}. Furthermore, the size of C(η), denoted by | C(η) |, is the sum of the lengths of each C(r) for all r ∈ η, i.e., | C(η) | = r∈η | C(r) |, where | C(r)
| is the length of the boolean formula C(r) as defined in propositional logic.

It remains to give a semantics to active constraints. In the rest of this subsection we discuss the two main existing directions, viz. founded and justified repairs. We later propose a new one in Section 2.5 using the programs of DL-PA.

Founded Weak Repairs and Founded Repairs

In the literature, founded repairs are considered to be a basic semantics of active constraints. They provide a basis for further refinements. The key notion they rely on is the foundedness condition.2

Definition 2.4. Let V be a database and let η be a set of active constraints. A consistent set of update actions U is founded if for every α ∈ U there is an r ∈ η such that:

(a) α ∈ R(r) (b) V U |= C(r) (c) V (U \ {α}) |= C(r)
Given this condition, the definitions of a founded weak repair and a founded repair immediately follow.

Definition 2.5. Let V be a database and let η be a set of active constraints. A set of update actions U is a founded weak repair of V by η if U is a weak repair of V achieving

C(η) and U is founded. Moreover, if U is also a PMA repair of V achieving C(η), then U
is a founded repair of V by η.

The following simple example showcases this definition.

Example 2.3. Let V = ∅ and η = p, {p ← } , p∨q, {q ← } . The set {p ← }
is the only founded weak repair of V by η. Indeed, the second update action in {p ← , q ← } cannot be founded on the second active constraint of η. It is also the only founded repair.

There are sets of active constraints for which there is no founded repair, although there is a founded weak repair [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], Example 2]. The next example, which is adapted from the example of the introductory Section 2.1, shows that there are sets of active constraints for which there is not even a founded weak repair.

Example 2.4. Let V = ∅ and η = p∨q, {p ← } , ¬p∨q, {q ← } . The set {q ← } is a PMA repair of V achieving C(η). However, there is no founded weak repair (and thus no founded repair either).

Last but not least, the next example illustrates circularity of support: each update action is individually founded because the others happen to be in the repair.

Example 2.5 ( [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], Example 3). Let V = ∅ and η = p∨q, {p ← } , ¬p∨q, {q ← } , p∨¬q, {p ← } . The set {p ← , q ← } is the only founded weak repair of V by η: p ← is founded on p∨¬q, {p ← } and q ← is founded on ¬p∨q, {q ← } . It is also a founded repair.

Such repairs were considered to be unintended in [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF] and the notion of justified repair was proposed to overcome the problem. We discuss this issue further in Section 2.5.3.

Justified Weak Repairs and Justified Repairs

Justified repairs use a stronger condition than foundedness in order to avoid the aforementioned circular dependencies. We start with the definition of a closed set of update actions.

Definition 2.6. Let η be a set of standard active constraints. For r ∈ η, all the literals in C(r) which have no preferred update actions in R(r) are called non-updatable. A set of update actions U is closed under an r ∈ η when the following holds: if the update actions in U falsify all the non-updatable literals in C(r), then U must contain an update action from R(r). Furthermore, U is closed under η if it is closed under every r ∈ η.

For example, {p ← , q ← } is closed under p∨¬q, {p ← } , ¬p∨q, {q ← } and p∨q, {p ← } , while it is neither closed under ¬p∨¬q, {p ←⊥} nor under ¬p∨r, {r ← } . The second step is to define the no-effect actions associated with an initial database V and an updated database V .

Definition 2.7. Let V and V be two databases. The update action p ← is a no-effect action of (V , V ) if p ∈ V ∩ V and the update action p ←⊥ is a no-effect action of

(V , V ) if p / ∈ V ∪ V .
The set ne(V , V ) denotes the set of all no-effect actions of (V , V ).

Clearly, for given V and U , we have that

V U = V (U \ U ) for every U ⊆ ne(V , V U ).
Returning to our initial aim now, the definitions of a justified weak repair and a justified repair are the following.

Definition 2.8. Let V be a database and let η be a set of standard active constraints. A consistent set of update actions U is a justified weak repair of V by η iff:

3 (a) U ∩ ne(V , V U ) = ∅ (no 'no-effect' actions) (b) U ∪ ne(V , V U ) is closed under η (c) there is no U ⊂ U ∪ ne(V , V U ) such that: (1) U contains ne(V , V U ) (2) U is closed under η Finally, if U is also a PMA repair of V achieving C(η), then U is a justified repair of V by η.
The next theorem shows the relationship between founded and justified repairs.

Theorem 2.1 ( [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], Corollaries 1 and 2). Let V be a database, U a consistent set of update actions and η a set of standard active constraints.

If U is a justified weak repair of V by η, then U is also a founded weak repair of V by η (and likewise, if it is a justified repair of V by η, then it is also a founded repair of V by η).

The next example shows that the converse does not hold. Furthermore, it illustrates that for justified repairs circularity of support is no longer an issue.

Example 2.6 ( [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], Example 5). Consider again V = ∅ and η = p∨q, {p ← } , ¬p∨q, {q ← } , p∨¬q, {p ← } . In contrast with Example 2.5 and its founded repair, there is no justified weak repair of V by η. As justified weak repairs are also founded weak repairs, we only have to check whether U = {p ← , q ← } is a justified weak repair of V by η. Supposing that P = {p, q}, we

have ne(V , V U ) = ne(∅, {p, q}) = ∅ and U ∪ ne(V , V U ) = U is not a minimal
set of update actions containing ne(V , V U ) and closed under η, as ∅ also has these properties.

However if we replace η with η = p∨q, {p ← , q ← } , ¬p∨q, {q ← } , p∨¬q, {p ← } then the set {p ← , q ← } is both a justified and a founded repair of V by η (and both are the only ones).

In the next two sections, we show that weak, PMA, founded and justified repairs can be captured in DL-PA.

Repairs and Weak Repairs in DL-PA

We now embed Winslett's standard semantics (and thereby weak repairs) and the PMA (and thereby repairs tout court) into DL-PA. This was already done in [Herzig, 2014],

but our embeddings are slightly more elegant and are presented in a more uniform and streamlined way. We start with some auxiliary definitions.

To each propositional variable p we associate a fresh propositional variable p ± . Each p ± will register whether or not the proposition p has been modified along the update.4

This is necessary to ensure that every variable is modified at most once during a repair.

We extend the definition to sets of variables P ⊆ P:

P ± = {p ± | p ∈ P }.
With the information stored in the fresh variables P ± , we can retrieve the initial valuation from a valuation V ⊆ P ∪ P ± through the set:

{p ∈ V : p ± / ∈ V } ∪ {p / ∈ V : p ± ∈ V }
First, we need a program that sets all the propositions in a given set P to ⊥: P ←⊥ is the sequence of assignments p ←⊥ for all p ∈ P (whose order does not matter, see Proposition 1.3). Second, the following two DL-PA programs (1) modify a single proposition and store this and (2) undo that modification: It is easy to see then that starting from a database V that contains none of the variables p ± , a weak repair of V achieving C can be obtained through the following DL-PA program:

toggle(p) = if ¬p ± then p ←¬p; p ± ← else fail = ¬p ± ?; p ←¬p; p ± ← undo(p) = if p ± then p ←¬p; p ± ←⊥
weakRepair(C) =   p∈P C toggle(p)   * ; C ?
Since each variable can be updated at most once and since the order of the updates does not matter, this can be rewritten without the Kleene star as a sequence:

toggle(p 1 ) ∪ skip ; . . . ; toggle(p k ) ∪ skip ; C ?
where p 1 , . . . , p k are the variables in P C . Furthermore, given that none of the variables p ± occur in the database, the program toggle(p) simplifies to just: p ←¬p; p ± ← .

Finally, we define the following DL-PA formula:

Minimal(C) = ¬   p∈P C undo(p)   + C
The program in this formula undoes a nonempty set of toggle(p) actions (and nondeterministically so, failing when there was no change at all). Thus, the formula Minimal(C)

says that there is no execution of that program leading to a database closer to the actual database that satisfies the constraints. Hence the actual database corresponds to a minimal change of the initial database. We sum up all the above in the following theorem.

Theorem 2.2. Let C be a set of static integrity constraints in the language of P and let V ⊆ P be a database (i.e., no p ± occurs in either of them). Let U be a consistent set of update actions that is relevant w.r.t. V .

• U is a weak repair of V achieving C iff:

V , V U ∈ ||weakRepair(C) ; P C ± ←⊥|| • U is a PMA repair of V achieving C iff: V , V U ∈ ||weakRepair(C) ; Minimal(C)? ; P C ± ←⊥||
Proof. For the first item, when

V ⊆ P observe that V , V ∈ ||weakRepair(C)|| iff
V ∈ || C|| and the following holds for all variables p ∈ P (i.e., excluding the p ± ):

(a) p ± ∈ V iff V (p) = V (p) (b) if p / ∈ P C then V (p) = V (p)
which means that only p's from C and the associated p ± were modified.

So V , V U ∈ ||weakRepair(C); P C ± ←⊥|| iff (V U ) ∈ || C|| and no p ± exists in U .
By Definition 2.1 then, this is equivalent to U being a weak repair of V achieving C.

For the second item, given some actual database V , define the initial database as:

V = {p ∈ P : p ∈ V and p ± / ∈ V } ∪ {p ∈ P : p / ∈ V and p ± ∈ V } Then V ∈ ||Minimal(C)|| iff there is no V ∈ || C|| such that D(V , V ) ⊂ D(V , V ). 5
Again then, starting from an initial database

V ⊆ P, V , V U ∈ ||weakRepair(C); Minimal(C)?; P C ± ←⊥|| iff (V U ) ∈ || C||, there is no V ∈ || C|| such that D(V , V ) ⊂ D(V , V U )
and no p ± exists in U , which according to Definition 2.8 is equivalent to U being a PMA repair of V achieving C.

Founded and Justified Repairs in DL-PA

We will now move on to the embedding of the notions of founded and justified repairs into DL-PA. For this, we will re-use the programs defined in the previous section for finding a weak repair and checking minimality, as well as the set of fresh variables P ± we had at our disposal in order to keep track of modifications. Moreover, we will need to define a program for checking the foundedness condition in order to generate the founded repairs as well as programs for adding the no-effect actions to a database and checking if a set of update actions is closed under a set of active constraints.

We start with the embedding of founded repairs into DL-PA, for which we will need the following formula:

Founded(η) = p∈P C(η)     p ± → r∈η p ←X∈R(r) p ←¬p ¬C(r)    
where X ranges over { , ⊥}. As we will see, the formula is true if and only if all current update actions (encoded in the current valuation by means of the fresh variables p ± ) are founded.

The embedding of justified repairs into DL-PA is a bit more complex. Firstly, we use the set nup(r) of all the non-updatable literals in r that we saw in Definition 2.6, i.e., all the literals in C(r) for which there is no preferred update action in R(r). By nup(r) + we denote the set of propositional variables of the form p in nup(r), i.e., nup(r) + = nup(r) ∩ P. Similarly, nup(r) -comprises the propositional variables of the form ¬p in nup(r), i.e., nup(r) -= {¬p | p ∈ nup(r) \ P}. Furthermore, we introduce two new sets of fresh propositional variables, P + and P -, defined similarly to P ± as follows:

P + = {p + | p ∈ P } and P -= {p -| p ∈ P }.
Intuitively, the proposition p + will keep track of the no-effect action of the form p ← , while the proposition p -will keep track of the no-effect action of the form p ←⊥. This is realized by the following two programs:

ne + (p) = p ∧ ¬p ± ? ; p + ← ne -(p) = ¬p ∧ ¬p ± ? ; p -←
Moreover, we will need a program that skips when neither p ← nor p ←⊥ is a no-effect action and fails otherwise (where 'ea' stands for 'effect action'):

ea(p) = p ± ?
Then we associate with the current database all the no-effect actions between the initial database and the current state through the following program:

ne(η) = ne + (p 1 ) ∪ ne -(p 1 ) ∪ ea(p 1 ) ; . . . ; ne + (p k ) ∪ ne -(p k ) ∪ ea(p k )
where p 1 , . . . , p k are the variables in P C(η) (so the no-effect actions that are added are only those that are relevant w.r.t. η). The next lemma will be helpful in the proof of Theorem 2.4 below.

Lemma 2.1. Let η be a set of standard active constraints in the language of P and let V 0 ⊆ P be a database (so no p ± , p + and p -occurs in either of them). Let V be some repaired database (containing variables p ± ) and let V = V ∩ P be the database V without the variables p ± . Furthermore, let U be a consistent set of update actions and let

U = {p + ← | p ← ∈ U } ∪ {p -← | p ←⊥ ∈ U }.
Then U contains all the no-effect actions between V 0 and V that are relevant w.r.t. η iff V , V U ∈ ne(η) .

Proof. For the left-to-right direction, V , V U ∈ ne(η) if all the extra variables in (V U ) \ V were added through the programs ne + (p) and ne -(p) for all p ∈ P C(η) For the right-to-left direction, let p + ∈ V U . Since V contains no p + variables, this means that p + ← ∈ U and consequently p ← ∈ U . Furthermore, since V , V U ∈ ne(η) , the only way for p + ∈ V U is through the program ne + (p) in ne(η). So this means that p ∧ ¬p ± ∈ V , which makes p ← a no-effect action between V 0 and V .

(note that V ⊆ V U ). But by definition, if p ← is a no-effect action of (V 0 , V ) then p ∈ V 0 ∩ V , which means that p ∧ ¬p ± ∈ V . Similarly, if p ←⊥ is a no-effect action of (V 0 , V ) then p / ∈ V 0 ∪ V , which means that ¬p ∧ ¬p ± ∈ V . But
Similarly for p -∈ V U . Finally, since the program ne(η) spans across all variables in P C(η) , the only way for both

p + / ∈ V U and p -/ ∈ V U is through the program ea(p).
This means then that p ± ∈ V and p is not a no-effect action between V 0 and V . Thus U contains all the no-effect actions between V 0 and V that are relevant w.r.t. η.

Next, we define A(r) and B(r) to be the following formulas:

A(r) = p∈nup(r) + (¬p ∧ p ± ) ∨ (¬p ∧ p -) ∧ p∈nup(r) - (p ∧ p ± ) ∨ (p ∧ p + ) B(r) = p ← ∈R(r) p ∨ p ←⊥∈R(r)
¬p

Using these then we define:

Closed(η) = r∈η A(r) → B(r) MinimallyClosed(η) =¬   p∈P C(η) undo(p)   + Closed(η)
The next lemma will be once again used in the proof of Theorem 2.4 below.

Lemma 2.2. Let η be a set of standard active constraints in the language of P and let V 0 ⊆ P be a database (so no p ± , p + and p -occurs in either of them). Let V 1 be some repaired database (containing variables p ± ) and let

V 1 = V 1 ∩ P be the database V 1
without the variables p ± . Furthermore, let

V 2 = V 1 ∪ {p + | p ← ∈ ne(V 0 , V 1 )} ∪ {p -| p ←⊥ ∈ ne(V 0 , V 1 )}
be the extension of V 1 containing all no-effect actions between V 0 and V 1 encoded through the variables p + and p -. Finally, let U comprise the update actions that re-

paired V 0 to V 1 , plus all no-effect actions between V 0 and V 1 . Then U is closed under η iff V 2 ∈ Closed(η) .
Proof. For the left-to-right direction, it is easy to see that if V 2 |= A(r) for some r ∈ η then V 2 falsifies all non-updatable literals in r. But by construction the variables in these literals either come from the repairing of V 0 to V 1 (through p ± ), or from adding the noeffect actions to V 1 (through p + and p -). This means that they come from update actions in U , which by hypothesis is closed under η. Thus U must contain an update action from

R(r) and V 2 |= B(r). Since r ∈ η was arbitrary, V 2 ∈ Closed(η) .
For the right-to-left direction, let the update actions in U falsify all non-updatable literals in C(r) for some r ∈ η. By construction again, this means that V 2 |= A(r).

But by hypothesis V 2 ∈ Closed(η) , so V 2 |= B(r) as well. If also V 0 |= B(r), then either the constraint r ∈ η was already satisfied from the beginning and the update action

p ←X ∈ R(r) such that V 0 |= B(r)
is a no-effect action, or it got satisfied by another update action in U . In all cases U contains an update action from R(r), which means U is closed under r. Since r ∈ η was arbitrary, U is closed under η.

So given a set of standard active constraints η, the first formula is true exactly when all current update actions (again, encoded in the current valuation through the set P ± ) plus all the no-effect actions (encoded in the current valuation through the sets P + and P -) are closed under η, while the second formula is true if and only if the set comprising of all current update actions is the minimal set of update actions that (together with the no-effect actions) has this property. Finally, we define the following abbreviations:

Justified(η)? = ne(η) ; Closed(η)? ; MinimallyClosed(η)?

ClearAll = P C ± ←⊥ ; P C + ←⊥ ; P C -←⊥
The following two theorems now give a complete characterisation of founded and justified repairs in terms of DL-PA programs.

Theorem 2.3. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database (i.e., no p ± occurs in either of them). Let U be a consistent set of update actions that is relevant w.r.t. V .

• U is a founded weak repair of V by η iff:

V , V U ∈ weakRepair(C(η)) ; Founded(η)? ; P C ± ←⊥ • U is a founded repair of V by η iff: V , V U ∈ weakRepair(C(η)) ; Founded(η)? ; Minimal(C(η))? ; P C ± ←⊥
Proof. Let V 0 be the initial database and suppose V is some repaired database (containing variables p ± ). Define the set of update actions:

U V ,η = {p ← : p ± ∈ V and p ∈ V } ∪ {p ←⊥ : p ± ∈ V and p / ∈ V } Let us prove that V 0 , V ∈ ||weakRepair(C(η)); Founded(η)?|| iff U V ,η is a founded
weak repair of V 0 by η. The latter means that for every α ∈ U V ,η the three conditions (a)

α ∈ R(r), (b) V 0 U V ,η |= C(r) and (c) V 0 (U V ,η \ {α}) |= C(r) of Definition 2.4 are satisfied.
For the left-to-right direction consider some

p ← ∈ U V ,η . Then p ± ∈ V . First of all, V 0 , V ∈ ||weakRepair(C(η))|| so U V ,η is a weak repair of V 0 by η. Condition (b) is
satisfied from the definition weakRepair(C(η)) and Theorem 2.2. Condition (a) is satisfied by the existence of a candidate constraint in the definition of Founded(η); remark that we are guaranteed that the constraint contains indeed p ← , as opposed to p ←⊥, because undoing the change on p changes C(r) to false (so X has to be ).

Condition (c) is satisfied because V 0 (U \{p ← }) |= C(r) is equivalent to V 0 U |= ¬ p ←⊥ C(r). Similarly for some p ←⊥ ∈ U V ,η . So U V ,η
is a weak repair and satisfies the three conditions, making it a founded weak repair of V 0 by η.

For the right-to-left direction, since U V ,η is also a weak repair of V 0 by η, Theorem 2.2 ensures that V 0 , V ∈ ||weakRepair(C(η))|| (remember that we chose the repaired database V to contain variables p ± ). To prove that V ∈ ||Founded(η)||, consider some p ± ∈ V . By definition, it entails p ←X ∈ U V ,η for some X ∈ { , ⊥}.

Condition (a) ensures that there is a constraint r ∈ η with p ←X ∈ R(r).

Condition (c) implies V |= ¬ p ←¬X C(r). So V , V ∈ ||Founded(η)?|| and thus V 0 , V ∈ ||weakRepair(C(η)); Founded(η)?||.
The rest of the proof (regarding minimality and non-existence of any p ± in U ) is similar to that of Theorem 2.2.

Theorem 2.4. Let η be a set of standard active constraints in the language of P and let V ⊆ P be a database (so no p ± , p + and p -occurs in either of them). Let U be a consistent set of update actions that is relevant w.r.t. V .

• U is a justified weak repair of V by η iff:

V , V U ∈ weakRepair(C(η)) ; Justified(η)? ; ClearAll • U is a justified repair of V by η iff: V , V U ∈ weakRepair(C(η)) ; Justified(η)? ; Minimal(C(η))? ; ClearAll
Proof. First of all, notice that we can reduce the set of no-effect actions to those only concerning the set of active integrity constraints η, since the rest have no impact on the repairing procedure and produce the same results. Without loss of generality, we can assume that the set ne(V , V U ) only contains those no-effect actions that are relevant w.r.t. η, for all V and U . Similarly to the previous proof, let V 0 be the initial database, V 1 some repaired database (containing variables p ± ) and define the set of update actions:

U = {p ← : p ± ∈ V 1 and p ∈ V 1 } ∪ {p ←⊥ : p ± ∈ V 1 and p / ∈ V 1 }
Furthermore, let V 2 extend V 1 with variables p + and p -which encode the no-effect actions between V 0 and V 0 U :

V 2 = V 1 ∪ {p + | p ← ∈ ne(V 0 , V 0 U )} ∪ {p -| p ←⊥ ∈ ne(V 0 , V 0 U )}
We have to prove that V 0 , V 2 ∈ ||weakRepair(C(η)); Justified(η)?|| iff U is a justified weak repair of V 0 by η. According to Definition 2.8, the latter is equivalent to the fact

that (a) U ∩ ne(V 0 , V 0 U ) = ∅, (b) U ∪ ne(V 0 , V 0 U ) is closed under η and (c) U ∪ ne(V 0 , V 0 U ) is a minimal set containing ne(V 0 , V 0 U ) which is closed under η.
Note that by construction, V 1 is the repaired database V 0 U together with the variables

p ± .
For the left-to-right direction, the construction of V 2 through the use of the programs weakRepair(C(η)), ne(η), Closed(η)? and MinimallyClosed(η)? gives:

(1)

V 2 , V 2 ∈ Closed(η)? and thus V 2 ∈ Closed(η) (2) V 2 , V 2 ∈ MinimallyClosed(η)? and thus V 2 ∈ MinimallyClosed(η)
Property (a) is derived from the fact that U is relevant w.r.t. V 0 . Property (b) is immediate by (1) and Lemma 2.2. So the set U ∪ne(V 0 , V 0 U ) obviously contains the set ne(V 0 , V 0 U ) and is also closed under η. For property (c), suppose there exists a repair U such that U ⊂ U ∪ ne(V 0 , V 0 U ) and which also contains the set ne(V 0 , V 0 U ) and is closed under η, and let U = U \ ne(V 0 , V 0 U ). Define also V to be V 0 U , together with the variables p ± that keep track of the changes between V 0 and V 0 U plus the variables p + and p -that encode the no-effect actions in ne(V 0 , V 0 U ). Then V , V ∈ ||Closed(η)?|| and since U ⊂ U we have that V 2 / ∈ MinimallyClosed(η) , which is contrary to property (2).

For the right-to-left direction, since U is also a weak repair of V 0 by η, Theorem

2.2 ensures that V 0 , V 1 ∈ ||weakRepair(C(η))|| (remember that we chose the repaired database V 1 to contain variables p ± ). Then V 1 , V 2 ∈ ||ne(η)
U ∪ ne(V 0 , V 0 U ) is a minimal set containing ne(V 0 , V 0 U ) which is closed under η, then V 2 ∈ ||MinimallyClosed(η)|| as well. So V 2 , V 2 ∈ ||Closed(η)?|| and V 2 , V 2 ∈ ||MinimallyClosed(η)?|| and thus V 0 , V 2 ∈ ||weakRepair(C(η)); Justified(η)?||.
Once again, the rest of the proof (regarding minimality and non-existence of any p ± , p + and p -in U ) is similar to that of Theorem 2.2.

A New Definition of Repair in DL-PA

We now propose some new definitions that take advantage of the resources of DL-PA.

More precisely, we make use of while loops in order to iterate the application of active constraints. We start by discussing how databases can be repaired by applying active constraints in sequence. This will lead us to the definition of dynamic repair. We show that it is incomparable with both founded and justified repairs and discuss its properties and some variants.

Repairing a Database: a Dynamic View

Suppose there is only one active constraint r that is standard. Then it is clear how to proceed: either V |= C(r) and there is nothing to do, or V |= C(r) and we have to apply r. In the second case, each α i ∈ R(r) provides a PMA repair of V achieving C(r). 6 What about the case where R(r) is empty? Well, then V cannot be repaired and we are stuck.

So far so good. The situation may get way more intricate when the set of active constraints η contains two or more elements that can interact. Firstly, the example of the introductory Section 2.1 and Example 2.4 illustrated an instance of active constraints which intuitively should have a repair (and it does, in the case of PMA repairs) but for which there is no founded or justified weak repair. We would like to find a definition of a repair which depends only on the preferred update actions and always provides a repaired database, as long as there are update actions from each C(r) to choose from. Moreover, even for standard active constraints it might not be enough to apply an update action

α i ∈ r∈η R(r)
only once: some of the active constraints might have to be applied several times in order to obtain integrity. The following active constraints that are inspired by an (n+1)-bit counter highlight this.

Suppose for n ≥ 0 we represent binary numbers up to 2 n+1 -1 by means of n+1

propositional variables: ¬p n ∧ • • • ∧¬p 0 represents the integer zero and p n ∧ • • • ∧p 0 repre-6 For our more general active constraints where there is no syntactical link between C(r) and R(r) we have to compute all possible minimal subsets U ⊆ R(r) such that V U |= C(r). All of them will be PMA repairs.

sents 2 n+1 -1. For each bit we also need an auxiliary variable p i . Let:

r 1 = p 0 ∨x 1 ∨ • • • ∨x n , {p 0 ← } r 2 k = p k ∨¬p k-1 ∨ • • • ∨¬p 0 ∨x k , {x k ← } , for 1 ≤ k ≤ n r 3 k i = ¬p i ∨¬x k , {p i ←⊥} , for 1 ≤ k ≤ n and 0 ≤ i ≤ k -1 r 3 k k = p k ∨¬x k , {p k ← } , for 1 ≤ k ≤ n r 4 k = ¬p k ∨p k-1 ∨ • • • ∨p 0 ∨¬x k , {x k ←⊥} , for 1 ≤ k ≤ n
The idea is that when ¬p k ∧p k-1 ∧ • • • ∧p 0 is true, i.e., when the number 011. . .1 has to be incremented to 100. . .0, then x k is made true by r 2 k and remains so until 100. . .0 has been attained. This involves flipping the k digits in the conjunction ¬p k ∧p k-1 ∧ • • • ∧p 0 : with active constraints this is done one-by-one by r 3 k i and r 3 k k . Then x k is set to false again by r 4 k . Let η n be the set of all the above rules, for a given n, i.e., η n is the set:

r 1 }∪{r 2 1 , . . . , r 2n }∪{r 3 1 0 , r 3 1 1 }∪{r 3 2 0 , r 3 2 1 , r 3 2 2 }∪. . .∪{r 3n 0 , . . . , r 3n n }∪{r 4 1 , . . . , r 4n }
Successive repairing steps then implement an (n+1)-bit counter counting from the initial database ∅ to the database {p n , . . . , p 0 }.

The computation takes a number of steps that is exponential in n, while the number of update actions is 1 2 (n 2 +7n)+1, demonstrating that sometimes atomic repairs must be performed an exponential number of times: for example r 1 needs to be applied 2 n times in order to repair V 0 = ∅ by η n . Let us illustrate by the 3-bit counter how the repairs are done.

Example 2.7. Let's take n = 2 and try to obtain the integer 111 starting from 000. In Figure 2.1 we can see the steps needed through which we will reach the set of update actions U = {p 0 ← , p 1 ← , p 2 ← } that will update the database ∅ in order for it to satisfy the active integrity constraints in η 2 . The first column represents the current database (starting from ∅), the second column shows the constraint that was applied in order to reach it and in the third we see the current integer in the counter. Last but not least, the last column shows when an x k is kept true in order for the procedure to reach the integer 10 from 01 and the integer 100 from 011 when needed.

¬p 2 ∧ ¬p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ ¬x 2 000 - ¬p 2 ∧ ¬p 1 ∧ p 0 ∧ ¬x 1 ∧ ¬x 2 r 1 001 - ¬p 2 ∧ ¬p 1 ∧ p 0 ∧ x 1 ∧ ¬x 2 r 2 1 001 ¬p 2 ∧ ¬p 1 ∧ ¬p 0 ∧ x 1 ∧ ¬x 2 r 3 1 0 000 ¬p 2 ∧ p 1 ∧ ¬p 0 ∧ x 1 ∧ ¬x 2 r 3 1 1 010 ¬p 2 ∧ p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ ¬x 2 r 4 1 010 - ¬p 2 ∧ p 1 ∧ p 0 ∧ ¬x 1 ∧ ¬x 2 r 1 011 - ¬p 2 ∧ p 1 ∧ p 0 ∧ ¬x 1 ∧ x 2 r 2 2 011 ¬p 2 ∧ p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ x 2 r 3 2 0 010 ¬p 2 ∧ ¬p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ x 2 r 3 2 1 000 p 2 ∧ ¬p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ x 2 r 3 2 2 100 p 2 ∧ ¬p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ ¬x 2 r 4 2 100 - p 2 ∧ ¬p 1 ∧ p 0 ∧ ¬x 1 ∧ ¬x 2 r 1 101 - p 2 ∧ ¬p 1 ∧ p 0 ∧ x 1 ∧ ¬x 2 r 2 1 101 p 2 ∧ ¬p 1 ∧ ¬p 0 ∧ x 1 ∧ ¬x 2 r 3 1 0 100 p 2 ∧ p 1 ∧ ¬p 0 ∧ x 1 ∧ ¬x 2 r 3 1 1 110 p 2 ∧ p 1 ∧ ¬p 0 ∧ ¬x 1 ∧ ¬x 2 r 4 1 110 - p 2 ∧ p 1 ∧ p 0 ∧ ¬x 1 ∧ ¬x 2 r 1 111 - Figure 2.1: Incrementing 000 to 111 through η 2
We can see how some constraints need to be applied many times in order to succeed in repairing the original database. This calls for a dynamic way through which a database is updated in order for it to be repaired: a procedure that modifies the database according to the integrity constraints step by step, until it reaches a satisfactory form (i.e., satisfies the integrity constraints). Founded and justified repairs cannot do the job in this and other scenarios of that kind, as an active constraint can only be used once: indeed, in the example of the (n+1)-bit counter, no repair can be obtained by means of founded and justified repairs. That's why we introduce dynamic repairs.

Dynamic Weak Repairs and Dynamic Repairs

We associate with every active constraint r the DL-PA programs:

π r = ¬C(r) ? ; α∈R(r) α π ± r = ¬C(r) ? ; p ←X∈R(r) p ←X; p ± ← Remember that α∈R(r)
α equals fail when R(r) is empty. This matches the intuitive reading that we have given to active constraints in Section 2.2.2: the repair program π r checks whether the static integrity constraint associated with r is violated, and if so nondeterministically applies one of the update actions from R(r). The program π ± r moreover stores that p has been changed. These intuitions are also supported by the following proposition, which tells us that applicability of an active constraint r (the fact that C(r) is violated) is matched by the DL-PA notion of executability of the program π r .

Proposition 2.3. Let r be an active constraint and let V be a database. Then applicability of r at V is equivalent to both V |= π r and V |= π ± r .

Proof. It suffices to observe that when π is a nondeterministic composition of update actions then the equivalence ¬C(r) ↔ ¬C(r)?; π is DL-PA valid for every C(r).

Based on these, the definitions of a dynamic weak repair and a dynamic repair are the following.

Definition 2.9. Let V be a database and let η be a set of active constraints. A dynamic weak repair of V by η is a consistent set of update actions U such that U is relevant w.r.t.

V and:

V , V U ∈ while ¬ C(η) do r∈η π r Moreover, if U is also a PMA repair of V achieving C(η), then U is a dynamic repair of V by η.
In the following example we see that dynamic repairs can sometimes coincide with founded repairs.

Example 2.8 (Example 2.5, ctd.). Consider again V = ∅ and η = p∨q, {p ← } , ¬p∨q, {q ← } , p∨¬q, {p ← } . There is a single dynamic weak repair (and also dynamic repair) of V by η, viz. {p ← , q ← }. Remember by Example 2.6 that there is no justified repair.

As we have already witnessed with the (n+1)-bit counter though, dynamic weak repairs are not necessarily founded. The next example is simpler.

Example 2.9 (Example 2.3, ctd.). Consider again V = ∅ and η = p, {p ← } , p∨q, {q ← } , whose only founded weak repair was {p ← }. There are two dynamic weak repairs of V by η, namely {p ← } and {p ← , q ← }. Only the former is a dynamic repair.

Remember also that at the beginning of Section 2.5.1 we argued against founded and justified repairs using Example 2.4 (itself an adaptation of the example discussed in the introductory Section 2.1), for which we would like to have a way to repair V by η. The next examples shows that dynamic weak repairs solve this problem. Let us also note that just like founded and justified repairs, dynamic weak repairs do not necessarily coincide with dynamic repairs.

Example 2.10 (Example 2.4, ctd.). Consider again V = ∅ and η = p∨q, {p ← } , ¬p∨q, {q ← } . The only dynamic weak repair of V by η is the set of update actions {p ← , q ← }. But {q ← } is the PMA repair of V achieving C(η), so there is no dynamic repair.

Finally, in a similar manner as in the previous sections, the next theorem characterises dynamic repairs in terms of DL-PA programs.

Theorem 2.5. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database (i.e., no p ± occurs in either of them). Let U be a consistent set of update actions that is relevant w.r.t. V . U is a dynamic repair of V by η iff:

V , V U ∈ while ¬ C(η) do r∈η π ± r ; Minimal C(η) ? ; P C ± ←⊥
Proof. The proof is quite trivial and based on the definitions. Given a database V ⊆ P and a set of active integrity constraints η, a dynamic repair of V by η is both a dynamic weak repair of V by η and a PMA repair of V achieving C(η). In DL-PA terms then, this is given by the sequential composition of the programs while ¬ C(η) do r∈η π ± r and Minimal(C(η))?, with the DL-PA program π ± r keeping track of which propositions have been modified along the update so that they can be checked again in the latter. Finally, as before the program P C ± ←⊥ ensures that no p ± exists in U .

Some Interesting Properties

In this subsection we present some interesting properties of this dynamic procedure that distinguishes it from the other main repairs which have been studied and prevailed in the literature, viz. weak repairs, PMA repairs, founded and justified repairs. Our goal is to provide a concrete argument that repairs produced in this way are an interesting kind of repairs, possessing the advantages of the others while not comprising some of their disadvantages.

The main problem with founded repairs is the so called circularity of support which has been already mentioned at the end of Section 2.2.2. This undesirable property is what ultimately led to the definition of justified repairs, which are way more complex and difficult to understand, at least at first sight. Dynamic repairs on the other hand provide a solution to this problem without straying too far from the initial definition, making it far less intricate. In contrast with founded repairs which need the foundedness property to give priority to the "preferred" repairs, dynamic repairs simply select an update action from the set that they have access to (the set of preferred ones) without checking for any other condition. This leads to no circular support between any set of preferred actions and can also be seen in Example 2.8 where {p ← , q ← } remains a dynamic repair of V by η even if the constraint ' p∨¬q, {p ← } ' is absent (something that cannot be said for founded repairs, as this constraint is required for the foundedness of 'p'). Furthermore, although justified repairs solve this problem, they often do not exist, as can be seen by Example 2.6. Through dynamic repairs we can provide a solution to cases like this, avoiding the circularity of support found in founded repairs, while still being able to provide a repaired database. So not only are dynamic repairs more intuitive, but they also comprise the best of both situations.

Despite this however, one could still argue that they are too "strict", sometimes requiring that every integrity constraint in C(η) have a way to be repaired (an update action in R(r) should exist for all r ∈ η in order to make C(r) true). If R(r) = ∅ for some r ∈ η, then the whole dynamic repairing procedure could collapse and a dynamic weak repair never occur. The next example illustrates exactly this.

Example 2.11. Let V = {q} and η = p∨q, {p ← } , p, ∅ . The set {p ← } is a PMA repair of V achieving C(η). However, there are no dynamic weak repairs (and thus no dynamic repairs either).

As we can see, the problem arises when an integrity constraint has no preferred update actions and cannot be satisfied by the application of some other constraint when repairing the database. One could differentiate this behavior into three classes of repairs, based on the level of "strictness" of the preference that is involved in the active constraints. The more strict repairs are those conforming to the idea that every integrity constraint C(r) should be repaired only through an update action in R(r), the less strict allow any update actions in r∈η R(r) to be used for any integrity constraint C(r), while the middle ground is to keep a balance between the two. As we can see, the passing from the more strict class to the others changes the meaning of the update actions in R(r) from permitted repair actions to preferred ones, a distinction that is not always made clear in the literature. As

Example 2.11 shows, dynamic repairs and dynamic weak repairs possess some of this "strict" nature: an update action will only arise while updating a database if it helps to repair some constraint. This forbids repairs in cases where all clauses apart from those having no preferred actions are already satisfied. In contrast, in such cases solutions with founded weak repairs can occur, as shown in the next example.

Example 2.12 ( [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], Example 2). Let V = ∅ and η = p∨¬q ∨¬r, {p ← } , ¬p ∨ q ∨ ¬r, {q ← } , ¬p ∨ ¬q ∨ r, {r ← } , p, ∅ . The set {p ← , q ← , r ← } is the only founded weak repair of V by η. Furthermore, the set {p ← } is a PMA repair of V achieving C(η). There are no dynamic weak repairs (and thus no dynamic repairs either).

So this leads to the following question: should we require a repair to exist in such cases or not? Are we willing to agree with the fact that such databases do not and should not have a repair, or is repairing the database in order to satisfy the integrity constraints in C(η) of the highest priority?

If the answer to the last question is positive then dynamic repairs could be less interesting. We can however tweak the definition slightly and define global-dynamic weak repairs to be a kind of dynamic repairs with the same intuitive behavior as before but belonging to the least strict of the aforementioned classes of repairs. More precisely, the reason that dynamic repairs cannot repair a constraint using update actions found in other clauses is the local nature of the do part in the while loop. Before trying to repair the whole set of active integrity constraints in η, a dynamic repair locally checks if every clause (integrity constraint) is satisfied. If we drop this requirement and allow the dynamic procedure to globally choose update actions found in other clauses, then we will have a solution in Examples 2.11, 2.12 and more generally the cases we have discussed.

Definition 2.10. Let V be a database and let η be a set of active constraints. A globaldynamic weak repair of V by η is a consistent set of update actions U such that U is relevant w.r.t. V and:

V , V U ∈ while ¬ C(η) do r∈η α∈R(r) α
In the same vein as before, if U is also a PMA repair of V achieving C(η), then U is a global-dynamic repair of V by η.

It is easy to see now that this tweaked definition provides us with the desired repaired database in Examples 2.11 and 2.12. Specifically, the set {p ← } is a global-dynamic repair of V by η in both examples. Furthermore, a dynamic weak repair is always a global-dynamic weak repair, as it can be created by the same procedure using one step less, namely by not checking the condition "¬C(r)?" in the do part of the program. This makes dynamic weak repairs a subset of global-dynamic weak repairs (and also dynamic repairs a subset of global-dynamic repairs).

It is our intention to use the global-dynamic repairs mainly as a tool of comparison between the different classes of repairs and less as a practical repairing technique that would replace the others. As we will see, the most important attribute of global-dynamic repairs is that they are exactly the global-dynamic weak repairs that are minimal w.r.t. set inclusion (i.e., if U is a global-dynamic repair of V then there is no global-dynamic weak repair U of V such that U ⊂ U ). The recipe when defining repairs till now is to first give the definition of their weak versions and then state that they also have to be PMA repairs. This is of course different from saying that these repairs are the weak repairs that are minimal w.r.t. set inclusion, as in this case they would always exist if at least one of their weak counterparts existed. But it is not always the case that they may coincide with PMA repairs and usually may not exist altogether. This can be witnessed in Example 2.12 for founded repairs and in Example 2.10 for dynamic repairs.

However, when minimality w.r.t. set inclusion and coincidence with PMA repairs is the same, we have a much more powerful and reliable tool in our hands that avoids the main disadvantage of other repairs, namely that they may not exist (even if their weak versions do). This is shown in Theorem 2.6. Before this, a small lemma characterises this global-dynamic nature.

Lemma 2.3. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database. Let U 1 be a global-dynamic weak repair of V by η and U 2 be a weak repair of V achieving C(η) such that U 2 ⊂ U 1 . Then U 2 is also a global-dynamic weak repair of V by η.

Proof. By hypothesis, U 1 and U 2 are both consistent sets of update actions that are relevant w.r.t. V such that V U 1 |= C(η) and V U 2 |= C(η) with U 2 ⊂ U 1 . This means that V can be updated with less update actions than U 1 in order to satisfy the integrity constraints in η. But U 1 was constructed by iteration on checking the satisfaction of C(η) and applying update actions from r∈η R(r). Then U 2 can be constructed in exactly the same way, since it doesn't comprise any update actions outside of U 1 , with the difference of taking less update actions into account: namely, by restricting the nondeterministic choice to updates from U 2 and leaving the update actions in U 1 \ U 2 out of consideration. This will also lead to a repaired database. So U 2 is a global-dynamic weak repair of V by η as well.

Theorem 2.6. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database. Let U be a consistent set of update actions that is relevant w.r.t. V .

U is a global-dynamic repair of V by η iff U is a global-dynamic weak repair of V by η that is minimal w.r.t. set inclusion.

Proof. Let the set GDR consist of all the global-dynamic repairs of V by η and let M GDW R consist of all the global-dynamic weak repairs of V by η that are minimal w.r.t. set inclusion. For convenience we also define in the same way R as the set of all PMA repairs and W R as the set of all weak repairs of V achieving C(η). Finally, let GDW R be the set of all global-dynamic weak repairs of V by η. First of all, observe that

GDR = GDW R ∩R (1) and GDW R ⊆ W R (2). Let us show that GDR = M GDW R. • GDR ⊆ M GDW R: let U 1 ∈ GDR. By (1) then, U 1 ∈ GDW R and U 1 ∈ R. Let U 2 ∈ GDW R such that U 2 ⊂ U 1 . By (2) we also have that U 2 ∈ W R. This means that U 1 ∈ R and U 2 ∈ W R with U 2 ⊂ U 1 .
But this cannot be the case, as a PMA repair is a minimal weak repair w.r.t. set inclusion. So there is no

U 2 ∈ GDW R such that U 2 ⊂ U 1 , where U 1 ∈ GDW R. Thus U 1 ∈ M GDW R.
Note that this also applies to founded, justified and dynamic repairs. The difference is in the other direction.

• M GDW R ⊆ GDR: let U 1 ∈ M GDW R. By definition then, U 1 ∈ GDW R and there is no U ∈ GDW R such that U ⊂ U 1 (3). Let U 2 ∈ W R such that U 2 ⊂ U 1 .
By Lemma 2.3 it is also the case then that U 2 ∈ GDW R. But this cannot be the case by (3). So there is no

U 2 ∈ W R such that U 2 ⊂ U 1 . Since by (2) U 1 ∈ W R
as well, this means that U 1 ∈ R. Thus U 1 ∈ GDW R ∩ R and using (1) we get

U 1 ∈ GDR.
So there is enough evidence to support the idea of using global-dynamic repairs as our repairs of choice when we want to update a database taking into account active integrity constraints in the cases where other repairs don't work. They are the closest thing to a PMA repair as shown by the next Proposition, with the only limitation of being nonexistent if the set of update actions r∈η R(r) is empty or if an integrity constraint can't be repaired even through update actions existing in other clauses (in both cases a solution to this problem shouldn't exist intuitively).

Proposition 2.4. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database. Let U be a consistent set of update actions that is relevant w.r.t. V .

U is a global-dynamic repair of V by η iff U is a PMA repair of V achieving C(η) and

U ⊆ r∈η R(r).
Proof. The left-to-right direction is trivial by the definition of global-dynamic repairs, whereas the right-to-left direction follows immediately by Theorem 2.6.

But ultimately the choice between dynamic and global-dynamic repairs is traced back

to what the answer should be regarding the repairing or not of a database in all of these cases. The former use a more restrictive procedure that makes it more local, while the latter do not. A global-dynamic weak repair of V by η using the alternative definition with toggle(p) is the set of update actions {p ← , q ← , r ← }, which is obviously absurd.

As already mentioned, this does not happen with dynamic weak repairs and dynamic repairs. It is another aspect of their "strict" and local nature, as they check if a clause needs repairing before toggling any propositional variable, thus making any update action chosen to be exactly the intended one from the set of preferred ones.

Complexity of Dynamic Repairs

In this section we provide tight complexity bounds for the problems of existence of a dynamic weak repair and a dynamic repair. It is known that deciding the existence of a repair is NP-complete for weak repairs, PMA repairs and founded weak repairs, while it is Σ 2 Pcomplete for founded repairs, justified weak repairs and justified repairs [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF]. As we will see, the same problem proves to be more difficult for dynamic weak repairs and dynamic repairs: deciding their existence is PSPACE-complete.

For the lower bound (hardness) we provide a reduction from the problem of checking whether a fully quantified boolean formula is true, whereas for the upper bound (membership) a reduction to the model checking problem of DL-PA will suffice. The result follows from the fact that checking whether a fully quantified boolean formula is true and DL-PA model checking are both PSPACE-complete problems [Stockmeyer andMeyer, 1973, Balbiani et al., 2014].

Lower Complexity Bound

In order to show that the existence of dynamic weak repairs and dynamic repairs is PSPACE-hard we will provide a reduction from the following problem: given a fully quantified boolean formula G, decide whether G is true. We suppose w.l.o.g. that G is in prenex normal form, with the variables in the prefix being all different and the matrix containing only the boolean connectives ¬ and ∧. Let subf(G) be the set comprising all the subformulas of G and let subf v (G) be the set comprising all the variables in G.

Furthermore, let subf ¬ (G), subf ∧ (G), subf ∃ (G) and subf ∀ (G) be the sets comprising all subformulas of G that have the form ¬A, A ∧ B, ∃x.A and ∀x.A, respectively. It is easy

to see that subf(G) = subf v (G) ∪ subf ¬ (G) ∪ subf ∧ (G) ∪ subf ∃ (G) ∪ subf ∀ (G). Next,
we define the set P G of propositional variables to be composed of:

• all x, x? and x! such that x ∈ subf v (G)

• A+?, A-?, A+!, A-! and A± for each A ∈ subf(G) Intuitively, the elements of P G play the following roles: x stores the truth value of x in G, x? indicates that a value for x must be chosen and x! indicates that the value for x has been chosen. Similarly, A+? indicates that we check if A is true and A+! indicates that A has been proved to be true. The same goes for A-? and A-!, for checking and proving that A is false. Last but not least, A± is used to record the intermediate state whenever we need to verify that A is true for both x and ¬x (viz. when we have already checked the case where x is true and still have to check the case where x is false).

The idea now is to start from the initial formula G and to compute whether it is true by asking whether there is a dynamic procedure that repairs the database {G+?} under a set of active constraints. We will define this set by first assigning a set of active constraints to each A ∈ subf(G), indicating the required steps for checking whether or not A can be proved true or false, and taking their union. For each A, the goal is to reach a state satisfying ¬A+? ∧ A+! if we want to prove that A is true and ¬A-? ∧ A-! if we want to prove that A is false. Indeed, each A ∈ subf(G) is associated with a set of active constraints which repair any database satisfying A+?∧¬A+! (respectively A-?∧¬A-!) to one satisfying ¬A+? ∧ A+! (respectively ¬A-? ∧ A-!). So, starting from the database {G+?} which satisfies G+? ∧ ¬G+!, if there is a successful dynamic repair procedure using these sets of active constraints then ¬G+? ∧ G+! will be reached and the initial formula G will be proved to be true. On the other hand, if there is no dynamic weak repair of {G+?} by these active constraints then G will be false.

In the following we define the sets of active integrity constraints for each A ∈ subf(G) that encode the truth conditions that are used in the evaluation of G. The literals underlined highlight the differences between the static constraints while the rightmost column explains the action taken. A small lemma after each definition proves why the respective case works, where (1) IndHyp(A, V ) + and (2) IndHyp(A, V ) -denote the induction hypotheses for A ∈ subf(G) and V ⊆ subf v (G), i.e.:

(1) := the set {A+? ←⊥, A+! ← } is a dynamic weak repair of

{A+?} iff V |= A (2) := the set {A-? ←⊥, A-! ← } is a dynamic weak repair of {A-?} iff V |= A • When A = ∃x.B we set: a 1 : ¬A+? ∨ A+! ∨ B+? ∨ B+! ∨ x? ∨ x! ∨ x
}. If V |= A then either V \ {x} |= B or V ∪ {x} |= B (1). Starting from
V ∪ {A+?} then, the active constraints a 1 to a 4 will make sure that the truth value of

x is set, i.e., x is in the database or ¬x is in the database, via the auxiliary variables x?

and x!. The active constraint a 5 then will ask if B is satisfied given the truth value of

x that is already set in the database. This will be checked by the active constraints that are assigned to B. By (1) then, since B is indeed satisfied for at least one of the truth values of x, choosing the correct one will result in the induction hypothesis removing the variable B+? from the database and adding the variable B+! to the database. Thus, the constraint a 6 will be violated and it is recorded that A is proved to be satisfied via the variable A+!. The active constraints a 7 to a 10 then remove all the auxiliary variables in case A needs to be checked again. 7 Given these we have that for at least one value of x the procedure is ending and a dynamic weak repair of V ∪ {A+?} by η exists. On the other hand, if a dynamic weak repair of V ∪ {A+?} by η exists then B has been proved to be satisfied for at least one truth value of x. This is done in the transition from a 5 to a 6 where, by adding B+? to the database, the active constraints assigned to B repair the database into one satisfying ¬B+? ∧ B+!. By induction hypothesis then, this means that either V \ {x} |= B or V ∪ {x} |= B (according to which of a 2 or a 3 took place last) which means that V |= A.

• When A = ∀x.B we set: Lemma 2.6. Let A ∈ subf ¬ (G) and V ⊆ subf v (G). Furthermore, consider that the induction hypothesis holds for B, where A = ¬B, i.e., both of IndHyp(B, V ) + and IndHyp(B, V ) -hold. Then: V ∪ {A+?}, the active constraint c 1 will ask for B to be false. This will be checked by the active constraints that are assigned to B. By (1) then, since B is indeed false in V , the (second) induction hypothesis will remove the variable B-? from the database and will add the variable B-! in the database. Thus, the constraint c 2 will be violated and it is recorded that A is proved to be satisfied via the variable A+!. The active constraint c 3 then removes the variable B-! in case A needs to be checked again. Finally, c 4 removes the variable A+?, thus ending the check for A. Given these observations, we have that the procedure is ending and a dynamic weak repair of V ∪ {A+?} by η exists. On the other hand, if a dynamic weak repair of V ∪ {A+?} by η exists then B has been proved to be false in V , i.e., V |= B, in the transition from c 1 to c 2 and the (second) induction hypothesis. Thus, V |= A.

b 1 : ¬A+? ∨ A+! ∨ A± ∨ B+? ∨ B+! ∨ x , {x ← } make sure x is true b 2 : ¬A+? ∨ A+! ∨ A± ∨ B+? ∨ B+! ∨ ¬x
• V |= A iff there is a dynamic weak repair of V ∪ {A+?} by {c 1 , c 2 , c 3 , c 4 } • V |= A iff
For the second case, the argument is similar (using the first induction hypothesis).

• When A = B ∧ C we set:

d 8 : ¬A-? ∨ A-! ∨ B-? ∨ C-? ∨ ¬B-! ∨ C-! , {A-? ← } B being false, A is proved false d 9 : ¬A-? ∨ A-! ∨ B-? ∨ C-? ∨ B-! ∨ ¬C-! , {A-? ← } C being false, A is proved false d 10 : ¬A-? ∨ ¬A-! ∨ B-? ∨ C-? ∨ ¬B-! ∨ C-! , {B-! ←⊥} remove the result for B d 11 : ¬A-? ∨ ¬A-! ∨ B-? ∨ C-? ∨ B-! ∨ ¬C-! , {C-! ←⊥} remove the result for C d 12 : ¬A-? ∨ ¬A-! ∨ B-? ∨ C-? ∨ B-! ∨ C-! , {A-? ←⊥} end the request for A Lemma 2.7. Let A ∈ subf ∧ (G) and V ⊆ subf v (G)
. Furthermore, consider that the induction hypothesis holds for B and C, where A = B ∧C, i.e., both of IndHyp(B, V ) + and IndHyp(C, V ) + hold whereas at least one of IndHyp(B, V ) -or IndHyp(C, V ) -holds.

Then: Proof. It can be checked that the procedure is similar to the one of Lemma 2.6, with the only points of interest being that in the first case we have to check through d 1 and d 2 that both B and C are satisfied by V before recording that A has been proved to be satisfied by V via the variable A+!. In the second case, since only one of B or C is needed to be proved false in V for A to be false in V , we distinguish these cases through the constraints d 8 and d 9 .

• V |= A iff
• When A = x we set: Proof. For the first case, consider the database V and the set of active constraints η =

e 1 : ¬A+? ∨ A+! ∨ ¬A , {A+! ← } A is proved true
{e 1 , e 2 }. Since A ∈ subf v (G) and V ⊆ subf v (G), V |= A means that A ∈ V . Starting
from V ∪ {A+?} then, the active constraint e 1 will confirm that A is in the database, whereas through e 2 the check for A will stop. Given these, we have that the procedure is ending and a dynamic weak repair of V ∪ {A+?} by η exists. On the other hand, if a dynamic weak repair of V ∪ {A+?} by η exists then e 1 was violated and consequently

A ∈ V , which means that V |= A.
Similarly for the second case, where V |= A means that A / ∈ V and e 3 is violated by V ∪ {A-?}.

Finally, consider g = G+? ∨ ¬G+!, {G+! ←⊥} which is used in the final step to ensure minimality of the repair procedure, i.e., in order to ensure that only the update action G+? ←⊥ survives at the end. We then define the set of active constraints η G to be the following:

A∈subf ∃ (G) {a 1 , . . . , a 10 } ∪ A∈subf ∀ (G) {b 1 , . . . , b 10 } ∪ A∈subf ¬ (G) {c 1 , . . . , c 8 } ∪ A∈subf ∧ (G) {d 1 , . . . , d 12 } ∪ A∈subf v (G)
{e 1 , . . . , e 4 } ∪ g

Then we have the following lemma, proposition and theorem.

Lemma 2.9. If there is a dynamic weak repair of {G+?} by η G then there is also a dynamic repair of {G+?} by η G .

Proof. By the construction of η G and the active constraint g, the set {G+? ←⊥} will always be the only dynamic weak repair of {G+?} by η G and, since ∅ is not a weak repair of {G+?} by η G , it is also a PMA repair. So if a dynamic weak repair of {G+?} by η G exists, it will be the set {G+? ←⊥} which is also a dynamic repair of {G+?} by η G .

Proposition 2.5. Let G be a fully quantified boolean formula in prenex normal form, with the variables in the prefix being all different and the matrix containing only the boolean connectives ¬ and ∧. Then:

• G is true iff there is a dynamic weak repair of {G+?} by η G

• G is true iff there is a dynamic repair of {G+?} by η G Proof. The first result is immediate by the construction of η G and Lemmas 2.4, 2.5, 2.6, 2.7 and 2.8. The second result follows from the first one and Lemma 2.9.

Theorem 2.7. The problems of existence of a dynamic weak repair and a dynamic repair are both PSPACE-hard.

Proof. It is known that checking whether a fully quantified boolean formula is true is a PSPACE-complete problem. The result follows from Proposition 2.5 and the fact that, given a formula G, the cardinality of the set η G is linear in the length of G.

Upper Complexity Bound

Next, in order to show that deciding the existence of dynamic weak repairs and dynamic repairs is in PSPACE we just need to reduce the problem into the model checking problem of DL-PA, since the latter is known to be PSPACE-complete [START_REF] Balbiani | DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE[END_REF]. The reduction is easy and is based on the following proposition.

Proposition 2.6. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database.

• A dynamic weak repair of V by η exists iff V |= π η , where π η is the program:

while ¬ C(η) do r∈η π r • A dynamic repair of V by η exists iff V |= π η , where π η is the program: while ¬ C(η) do r∈η π ± r ; Minimal(C(η))? ; P C ± ←⊥
Proof. In both cases, for the left to right direction consider that a dynamic weak repair (respectively, dynamic repair) of V by η exists. By Definition 2.9 and Theorem 2.5, this means that there exists a set of update actions U such that U is relevant w.r.t. V and

V , V U ∈ ||π η ||. Since V U |= , the result follows.
Again in both cases, for the right to left direction let V |= π η . This means that there exists a V such that V , V ∈ ||π η ||. It is easy to see that, if we set U = {p ← :

p ∈ V and p / ∈ V } ∪ {p ←⊥ : p ∈ V and p / ∈ V } then V = V U and U is relevant w.r.t. V .
So, in other words, there exists a U such that U is relevant w.r.t. V and V , V U ∈ ||π η ||. By Definition 2.9 and Theorem 2.5 then, this means that there exists a dynamic weak repair (respectively, dynamic repair) of V by η.

The theorem for membership then follows immediately.

Theorem 2.8. The problems of existence of a dynamic weak repair and a dynamic repair are both in PSPACE.

Proof. It is known that model checking in DL-PA is a PSPACE-complete problem. The result follows from Proposition 2.6 and the fact that, given a set of active integrity constraints η, the length of the program π η is linear in the size of the set C(η).

Using Theorems 2.7 and 2.8 then, we have the following corollary.

Corollary 2.1. The problems of existence of a dynamic weak repair and a dynamic repair are both PSPACE-complete.

History-Based Repairs

In this section we would like to discuss history-based repairs, an extension of the repairs seen so far taking into account databases with history. What we mean by history is the consistent set of transactions that took place from the last time the database satisfied the integrity constraints up until its current form. So let's say that apart from the initial database, we are also provided with a consistent set of update actions: these are what we refer to as history, the extra information of the route taken from an earlier point in time (more specifically, the last time the integrity constraints were satisfied) until the current state of affairs.

So given this extra information, how should we make use of it? A starting point would be to make sure that the update actions which took place in order to reach the current database will not appear again in the future. Imagine, for instance, that we are provided with the database V , a set of active integrity constraints η and an update action that took place in order to reach it, p ←⊥. If there exist two repairs of V by η, namely U 1 = {p ← } and U 2 = {q ← }, then we would like to disregard U 1 as it would repair

V by adding p and V would return to an "earlier state" (from which it was updated by removing p) thus violating the 'priority of the new information' principle that was widely considered in the update literature [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF]. Furthermore, we

should consider what happens in the case where, although repairs exist, there is no repair that updates the database without returning it to an "earlier state". Should we make use of them and disregard the given history or not? Intuitively, the repair actions of active integrity constraints are of the highest priority when repairing a database, whereas the aforementioned history is based on a set of update actions which was used to repair a previous database into the current one, but can be undone if needed. We can see this in the previous example as well, where if U 1 was the only repair of V by η then it should be applied regardless of p ←⊥ being used to reach V .

But perhaps a more concrete example is the following, based on the "an employee cannot be in 2 departments" constraint: let P = {d 1 , d 2 }, where d 1 and d 2 denote departments 1 and 2 respectively, and the integrity constraint r = ¬d 1 ∨¬d 2 , {d 1 ←⊥, d 2 ←⊥} which says that no employee should work in both departments at the same time; if this is the case, then they should be removed from either one, without any specific preference.

Assume now that H = {d 1 , d 2 }, {d 1 ← } is our history-based database, where {d 1 , d 2 } is our actual database V (saying that there is someone working on both departments) and the set {d 1 ← } represents the history, i.e., that the last department which they joined was d 1 . In this case, we would prefer the repairing of V by {d 2 ←⊥}, instead of {d 1 ←⊥}, considering the latest action of putting the specific employee recently in department 1 to be of higher priority. This is done by repairing V by r H = ¬d 1 ∨¬d 2 , {d 2 ←⊥} instead of r and actually disregarding the "preferred" update action d 1 ←⊥ in R(r) which conflicts with the provided history.

With that in mind, we call H = V , U a history-based database when V ⊆ P is a database and U ⊆ U a consistent set of update actions such that there is V ⊆ P with V U = V . We also define as U -1 the set comprising the opposite update actions in U :

U -1 = {p ←⊥ : p ← ∈ U } ∪ {p ← : p ←⊥ ∈ U }.
According to what has been said so far, we would like U to be a repair of a historybased database H = V , U by a set of active integrity constraints η, only if U ∩U -1 = ∅.

In order for this to happen we have to repair V by η H instead of η, where η H has:

r H = C(r), R(r) \ U -1 , for r ∈ η
In this way we disregard update actions which have the risk of returning our current database to a previous state and give priority to the new ones. As already mentioned, by choosing to ignore update actions based on the history U that we have, we may risk reducing a set R(r) to be empty for some r ∈ η, thus leading to no repairs occurring. In this case, choosing to not take U into consideration is the only option and we return to the repairing of V by η, instead of H by η. The following example highlights everything that's been said so far.

Example 2.13.

Let H = {d 1 , d 2 }, {d 1 ← } and η 1 = ¬d 1 ∨¬d 2 , {d 1 ←⊥, d 2 ←⊥} .
Both U 1 = {d 1 ←⊥} and U 2 = {d 2 ←⊥} are founded, justified, dynamic and globaldynamic repairs of V = {d 1 , d 2 } by η 1 . Only the second is a founded, justified, dynamic and global-dynamic repair of H by η 1 . Similarly, consider η 2 = ¬d 1 ∨¬d 2 , {d 1 ←⊥} .

Then U 1 = {d 1 ←⊥} is a founded, justified, dynamic and global-dynamic repair of V = {d 1 , d 2 } by η 2 . There are no repairs of H by η 2 , however, making us reduce H to just V and use U 1 once again.

Finally, let us define:

weakRepairH(C(η), U ) =   p∈A toggle(p)   * ; C(η) ? π ± r,U = ¬C(r) ? ; p ←X∈B p ←X; p ± ← and π ± r,U = p ←X∈B p ←X; p ± ←
where A = P C(η)\U -1 (the set of the variables that occur in C(η) and not in U -1 ) and

B = R(r) \ U -1 .
The next theorem characterises founded, justified, dynamic and global-dynamic history-based repairs in terms of DL-PA programs.

Theorem 2.9. Let η be a set of active integrity constraints in the language of P and let V ⊆ P be a database (so no p ± , p + and p -occurs in either of them). Let U and U be consistent sets of update actions such that U is relevant w.r.t. V .

• U is a founded repair of H = V , U by η iff:

V , V U ∈ weakRepairH(C(η), U ); Founded(η)? ; Minimal(C(η))? ; P C ± ←⊥

• U is a justified repair of H = V , U by η iff η is a set of standard active constraints and:

V , V U ∈ weakRepairH(C(η), U ); Justified(η)?; Minimal(C(η))?; ClearAll • U is a dynamic repair of H = V , U by η iff: V , V U ∈ while ¬ C(η) do r∈η π ± r,U ; Minimal C(η) ? ; P C ± ←⊥ • U is a global-dynamic repair of H = V , U by η iff: V , V U ∈ while ¬ C(η) do r∈η π ± r,U ; Minimal C(η) ? ; P C ± ←⊥
Proof. Note that the construction of all history-based repairs in DL-PA terms are identical to their counterparts in the previous sections, with the difference being in the choice of p's and update actions p ←X in the nondeterministic composition place of the programs.

By removing the set U -1 from each nondeterministic choice imposed by the programs

weakRepairH(C(η), U ), π ± r,U and π ± r,U
we get exactly the active integrity constraints r H (instead of r) needed in order to repair a history-based database by the corresponding set of active integrity constraints η H .

Conclusion

We have shown how several definitions of database repair via active integrity constraints can be expressed in DL-PA, including new proposals in terms of their iterated application. More specifically, we have introduced a new, dynamic way of handling database repair under a set of active integrity constraints and have shown some interesting properties (including advantages over other repairs, complexity) and alternatives (history-based repairs), all through the use of the quite simple but expressive Dynamic Logic of Propositional Assignments DL-PA. This allows us to claim that DL-PA is a nice integrated framework for database updates: it not only provides operators p ← of insertion and p ←⊥ of deletion and more generally sets U of such assignments that can be applied to a database V ; it also provides a means to reason about the repair of the resulting V U when some element of the set of integrity constraints is violated.

In the following, the program repair denotes one of the repair programs of Theorems 2.2, 2.3, 2.4, 2.5, 2.9, as well as Definitions 2.9 and 2.10. We can witness the aforementioned treatment of DL-PA as a means of reasoning between repairs in the following two instances:

• V is a possible repair of the update of the database V by the insertion or deletion of p if and only if the couple V , V belongs to the interpretation of the DL-PA programs p ← ; repair or p ←⊥; repair respectively.

• The set of candidate repaired databases is the interpretation of the DL-PA formula repair c ϕ V , where ϕ V is a conjunction of literals describing V syntactically.

But beyond identifying possible repaired databases, what is even more interesting is that our programs repair also allow to solve decision problems. Some notable examples follow:

• We may check whether it is possible at all to repair V by model checking in DL-PA whether V |= repair .

• We can check whether there is a unique repair of V by model checking whether the set of databases V such that V , V ∈ ||repair|| is a singleton. This amounts to model check for each of the variables p occurring in the constraints whether

V |= [repair]p ∨ [repair]¬p.
• We might as well wish to check possibility or unicity of the repairs independently of a specific database V . For instance, we can check whether η can repair any database by checking whether the formula repair is DL-PA valid.

• A further interesting reasoning task is to check whether two sets of active constraints η 1 and η 2 are equivalent under a given semantics by checking whether

||repair η 1 || = ||repair η 2 ||.
All of the above demonstrate the usefulness of DL-PA as a logic dealing with database repair. The related decision problems also provide a hint of the variety of applications it provides. Furthermore, our way of handling active integrity constraints of the form r = C(r), R(r) allowed us to generalise the condition C(r) from clauses to arbitrary formulas (that could actually even be DL-PA formulas). This opens up two perspectives. First, our definition also covers revision programs [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF]; we leave it to future work to establish the exact relationship. Second, we could further generalise the action R(r) from a set of update actions to arbitrary DL-PA programs. Dynamic repairs would then still make sense, while it is not clear how founded and justified repairs would have to be defined.

Last but not least, although we have argued that there are real world problems, such as the one in the introductory Section 2.1, where dynamic repairs are preferable over founded or justified repairs, we did see that this comes at a cost: the computational complexity of dynamic repairs is higher. We leave it to future work to explore possible avenues of improving this dynamic behavior, especially in terms of computational resources. A possible extension to a first-order setting is also a good avenue for future research, seeing that the nature of the procedure is independent of the propositional setting that we worked on and that it could easily be adapted on higher level formalisms. We immediately take the first steps and venture into the setting of Description Logics which lie between propositional and first-order logic.

CHAPTER 3

Repairing ABoxes via Active TBoxes: a Syntactic Approach

Introduction

As we have seen so far, the integrity constraints of the database literature are usually considered to be universal conditions or rules that must hold in any situation. When a database fails to satisfy such constraints it has to be repaired in order to restore integrity.

On a similar note, TBoxes in Description Logic are usually created by a long and careful procedure, rendering them of the highest priority for the ABoxes to abide by. In case of inconsistencies between an ABox and a TBox, the ABox is usually the one that should be updated to conform with the rules of the TBox [START_REF] Lembo | Inconsistency-tolerant semantics for description logics[END_REF], Bienvenu et al., 2014, Bienvenu et al., 2016].

In this chapter, we integrate the idea behind active integrity constraints to the TBoxes of Description Logic and extend the TBox axioms with preferred update actions. The or a : ∃R.A. It is mainly for this reason that we start our investigations with a syntactic approach, i.e., making syntactic modifications to ABox assertions until consistency with the TBox is achieved.

As we mentioned in Section 1.2.3, in this chapter we will make use of the basic description logic ALC. Furthermore, throughout the chapter we impose the following conventions:

• we suppose that all ABoxes are consistent

• we suppose that all TBoxes are consistent

• a TBox contains only concept inclusions and concept definitions

The chapter will be presented as follows. In Section 3.2 we discuss the main issues of extending TBoxes with update actions and the main differences with AICs on databases.

Section 3.2.1 is where the ideas discussed so far start to materialize with the first formal definition of 'active' TBoxes as extensions of the usual TBoxes. We then continue by taking a syntactic approach in Section 3.3, exploring ways in which we can reach a desired ABox that is repaired according to the preferences of these active TBoxes. We conclude in Section 3.4 with a discussion on the limitations of this syntactic way of repairing ABoxes, thus motivating further the semantic approaches that will follow in subsequent chapters.

Integrating Active Constraints to the TBox

We have already witnessed and discussed the importance and effectiveness of AICs on databases and how giving a designer tools to express preferences can lead to more informed ways of maintaining databases. We have also argued that such tools should be very useful for ontology engineers as well. Let's start by giving a simple example of a TBox in Figure 3.1, expressing the different definitions of marital status. In this TBox it is clearly stated that someone cannot be identified as bachelor and married at the same time. Now an ABox containing the concept Bachelor Married among its assertions is clearly inconsistent with respect to this TBox and has to be repaired. Dropping any of the two would solve this, however one could argue that a person declared as both bachelor and married should only be identified as married everywhere. Whereas one can achieve married status from being a bachelor, a married person cannot 'go back' to being bachelor but can only become divorced or widowed instead. Thus, dropping the concept Bachelor whenever the concept Bachelor Married appears in an ABox should be the preferred update action. In the same vein, since by the last inclusion of Figure 3.1 everybody has to have a marital status, the preferred update action would be to add the concept Bachelor to an individual violating this axiom, as in any other case the person would have to declare that s/he got married, divorced or widowed. Finally, as we can see it is clearly stated that someone cannot be identified as divorced and widowed at the same time. However, as a distinction between divorced and widowed cannot be made without further information, the axiom Divorced Widowed ⊥ should not give any preference between the concepts Divorced and Widowed. So, as witnessed by this example, there exist logical reasons for extending TBoxes and equipping them with extra information on preferences as well as investigating ways to make use of them.

A first difficulty comes in the form of the concept constructors that are employed by most DL languages and, more specifically, value restriction and full existential quantification. While AICs on propositional databases have a specific structure that makes the addition of update actions easy and straightforward (we have already investigated this structure in Chapter 2), it is not as straightforward to find the logical form of AICs in the case of DLs. the inconsistencies that may arise from complex concepts inside the axioms will not have a way to be repaired. It is for this reason that the active axioms that we will define in this and the next chapter will ultimately prove to be quite limited on the repairing routes that they will be able to provide.

Another differentiation between the TBox axioms and the constraints on databases is

the open world semantics that the ABoxes of DL Knowledge Bases employ in contrast to the closed world semantics of classical databases. Whereas in the latter one assumes to have complete knowledge of the facts expressed in a database, the description of a situation through an ABox is always incomplete, i.e., the absence of a statement does not imply its negation. We can also witness this distinction from the models of the DL Knowledge Bases and the fact that consistent ABoxes have multiple models which may describe differently the various parts of the domain not expressed by the ABox. This means that a repaired ABox with respect to a TBox is one that is consistent with the TBox: there exists an interpretation which is a model of both. Whereas for databases a repaired database is one which entails all the constraints, in the case of DL Knowledge Bases there may be other interpretations which do not satisfy the KB. So instead of model checking if a repaired database is the model of (i.e., satisfies) the integrity constraints, we now move on to consistency checking (or satisfiability checking) of a repaired KB.

Moreover, the aforementioned differentiation due to the open world nature of DLs gives rise to a duality in the case of removing concepts. While the update action add(A)

A T

(1)

A T

(2) This is akin to the distinction between revision and contraction from the belief change literature [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF]. As we mentioned before, achieving consistency with a TBox T in both cases amounts to finding an interpretation satisfying both A and T , i.e., A ∩ T = ∅. Figure 3.2 shows the difference between removing and forgetting concepts in order to achieve consistency inside a KB. In the current chapter we do not differentiate between the two and remove(A) can be interpreted both ways. In the following chapters though we adopt the former meaning as it behaves better semantically and the logics created this way come closer to the logic DL-PA we investigated in Chapter 2 (and whose atomic programs A ←⊥ are clearly interpreted in the former way).

The Active TBoxes

Similarly to how the active integrity constraints extend static constraints by adding update actions to each constraint, we define 'active' TBoxes to contain preferred update actions of the form add(A) and remove(A) for atomic concepts A. We start by defining what exactly is a static constraint in this setting.

Definition 3.1. A conjunctive constraint is any inclusion of the form

C 1 • • • C n ⊥.
A static constraint is any inclusion that is either a conjunctive constraint or equivalent to a conjunctive constraint.

For example, in the TBox of Figure 3.1, all three of the inclusions:

Bachelor Married ⊥, Divorced Widowed ⊥ Person Married Divorced Bachelor Widowed are static constraints since the first two are conjunctive constraints whereas the third is equivalent to the conjunctive constraint:

Person ¬Married ¬Divorced ¬Bachelor ¬Widowed ⊥

In fact, any inclusion axiom of this chapter is a static constraint. We continue with the definition of an active constraint.

Definition 3.2. Let ρ be a static constraint. If ρ is not a conjunctive constraint, let ρ be the conjunctive constraint that is equivalent to ρ. An active constraint η is a couple ρ → S, where S is a set of add(A) and remove(A) actions such that:

• if add(A) ∈ S then ¬A is a literal on the conjunction of ρ (or ρ ).

• if remove(A) ∈ S then A is a literal on the conjunction of ρ (or ρ ).

For instance, for the static constraint A ∃r.C B all the possible active constraints extending it are the following:

η 1 : A ∃r.C B → ∅ η 2 : A ∃r.C B → {add(B)} η 3 : A ∃r.C B → {remove(A)} η 4 : A ∃r.C B → {add(B), remove(A)}
We use the expression body(η) to denote the static constraint ρ and the expression head(η)

to denote the set of update actions add(A) and remove(A) for atomic concepts A.

We can already witness by the above example how specific concept constructors provide no counterparts for preferred update actions if we simply adapt the idea behind AICs to DLs and only allow additions or deletions of atomic concepts. As we can see, η 2 and η 3 give a preference between one of the two atomic concepts and η 4 gives no preference to any of them. In case however one doesn't want to change the status of these atomic concepts then the only other solution is to not change anything through η 1 , as there is no repairing path through the concept ∃r.C. So in the current state of active TBoxes, we have to keep in mind this limitation (that will be overcome in Chapter 5).

We formalize all the above by the relation ρ η, where ρ is a static constraint and η is an active constraint extending it as described in Definition 3.2. The next step is to generalise this construction to TBoxes. We extend the relation and define active TBoxes as follows.

Definition 3.3. Let T be a TBox. aT is an active TBox extending T , viz. T aT , iff for each static constraint ρ in T there is an active constraint η in aT such that ρ η and, vice versa, for each active constraint η in aT there is a static constraint ρ in T such that ρ η.

In Figure 3 In what follows, we present a first, syntactic approach for the difficult task of repairing an ABox, inconsistent with respect to an active TBox, taking into account preferred update actions, especially when the inconsistencies appear inside the scope of a quantifier.

A Syntactic Way of ABox Repairing

While updating a simple ABox (i.e., an ABox whose assertions consist only of concept literals) is quite straightforward, the update of an ABox which has complex concepts may not be easy (or even impossible) [START_REF] Flouris | Updating dls using the AGM theory: A preliminary study[END_REF], Flouris et al., 2009, Liu et al., 2011]. this goal, especially when the update actions are defined only on the atomic level. In this section we investigate how we could transform an initial ABox, inconsistent with respect to the active TBox, to a repaired one conforming to the active constraints of the TBox.

We mainly focus on the syntactic procedure that leads to a repaired ABox and what this resulting ABox could look like.

We start by defining a relation between two ABoxes, so that the second ABox is the outcome of applying a small change to the first ABox. Let S A be the set that consists of all concept symbols in the ABox A. For A ∈ S A we define the following:

• A = {A B | B ∈ S A } • A = {A B | B ∈ S A } • A ¬ = {¬A}
Furthermore, let: Definition 3.5. Let A and A be ABoxes and n > 0. Then A ∼ n A iff there are ABoxes A 1 , . . . , A n+1 such that:

• Γ A:A = A ∪ A ∪ A ¬ • Γ A = A∈S A Γ A:A Intuitively, Γ A
1. A = A 1 , A n+1 = A and A i ∼ 1 A i+1 , ∀i ∈ {1, . . . , n}.
2. A 1 , . . . , A n+1 are semantically different from one another, i.e., for any two A i and A j there exists an interpretation I such that I |= A i and I |= A j .

3. there is no n < n with these two properties.

When A ∼ n A we say that at least n steps are needed in order to reach the ABox A from the ABox A. Note that while we may have

A 2 = A 1 [A 1 | C 1 ] and A 3 = A 2 [A 2 | C 2 ]
and therefore

A 1 ∼ 1 A 2 ∼ 1 A 3 , we do not have A 1 ∼ 3 A 3 because of the last constraint.
Finally, let us define the relation A ∼ A to mean that A can be reached from A by an arbitrary number of steps.

Definition 3.6. Let A and A be ABoxes. Then A ∼ A iff there exists n > 0 such that

A ∼ n A .
By construction, ∼ is symmetric but it is neither reflexive (A cannot be semantically different from A) nor transitive (A ∼ A and A ∼ A but A ∼ A). So we have a way to change an ABox syntactically to another one with the use of the set Γ A by applying a finite number of times one-step changes to concept symbols on each subsequent ABox.

Furthermore, by construction the two ABoxes are always semantically different from each other and there is always a shortest path of n > 0 steps between them.

We can now utilize this construction in our effort of repairing an ABox with respect to an active TBox. Let A and aT be an ABox and an active TBox respectively such that

A is inconsistent with respect to aT and let R A n = {A | A ∼ n A } be the set of ABoxes that can be reached from A by at least n steps. So for each n > 0 we have that the

sets R A 1 , R A 2 , R A 3 , .
. . are pairwise disjoint and their union is the set R A = {A | A ∼ A } of ABoxes that can be reached from A by an arbitrary number of steps. The next propositions give some important properties on the cardinality of these sets.

Proposition 3.1. Let A and aT be an ABox and an active TBox respectively. Then for each n > 0 the set R A n is finite.

Proof. We start by noticing that since the ABox is always finite, the set S A containing its concept symbols is also finite. As a result, for each A ∈ S A the sets A , A and A ¬ are also finite, since they are made up of disjunctions, conjunctions and negations between symbols of S A . Then the set Γ A:A which is the union of the finite sets A , A and A ¬ is also finite, for all A ∈ S A . It follows that the set Γ A of concepts that can be reached with one step from S A is finite, since it comprises a finite union of finite sets.

The proof continues by induction. Let us look initially at the set R A 1 . It comprises the ABoxes that are semantically different and can be reached with one step from A. So by the definition,

A ∈ R A 1 iff A = A [A | C] or A = A [A | C] for some A ∈ S A
, where C ∈ Γ A:A . But as the A ∈ S A are finite and for each A the set Γ A:A is also finite, there is a finite number of ABoxes such that

A = A [A | C] or A = A [A | C]. As a result the set R A
1 is also finite. Next, we make the induction hypothesis, i.e., we consider that the set R A n is finite for an arbitrary n > 0. It suffices to show that the set R A n+1 is also finite. Let us take an ABox A ∈ R A n and create the set R A 1 of ABoxes that are semantically different and can be reached with one step from A . We already know that this set is finite.

But by hypothesis, the set of ABoxes A ∈ R A

n is also finite and thus the union

A ∈R A n R A 1 is finite as well. It's easy to see that R A n+1 ⊆ A ∈R A n R A
1 since for each ABox A which is at least n + 1 steps away from A there is an ABox A which is at least n steps away from A such that A ∼ n A and A ∼ 1 A . Thus the set R A n+1 is also finite and the induction is complete.

Proposition 3.2. Let A and aT be an ABox and an active TBox respectively. Then the set

R A is finite. Proof. It suffices to show that R A = m n=1 R A
n for some m > 0. Since we have a finite number of concept symbols, there is only a finite number of semantically different concepts that can be expressed by these symbols using the three boolean constructors. Furthermore, using these concepts in combination with the role symbols of A there is a finite number of semantically different concepts that can reach a specific role depth. But since for all concepts the role depth never changes between the ABox A and the ABoxes A ∈ R A , and also the set of individuals occurring in A is finite and doesn't increase, there will be a set of ABoxes R A n for which each subsequent ABox constructed by the relation ∼ 1 will have a semantically equivalent ABox belonging in a set R A m for m < n. In other words, there is an m > 0 such that R A n = ∅ for all n > m and

R A = m n=1 R A n .
Next we define a syntactic modification to be the update action needed in order to reach an ABox A from an ABox A in one step using the set Γ A .

Definition 3.7. Let A and A be two ABoxes such that A ∼ 1 A . The syntactic modification from A to A is the singleton set:

U A A =      {A → C} if A = A [A | C] {C → A} if A = A [A | C]
where C ∈ Γ A:A .

Using this definition we can now define an update sequence to be the sequence of syntactic modifications needed in order to reach an ABox A from an ABox A in n steps using the set Γ A .

Definition 3.8. Let A and A be two ABoxes such that A ∼ n A . The update sequence from A to A is the sequence:

S A A = U A 2 A 1 , U A 3 A 2 , . . . , U An A n-1 , U A n+1 An
where A 1 , . . . , A n+1 are the semantically different ABoxes of Definition 3.5.

Finally, if an ABox A can be syntactically modified to the semantically different

ABox A in at least n steps (i.e., if A ∼ n A ) through the update sequence S A A , we write

A S A A = A .
Notice that up until now we have not made use of the 'active' part of the TBox and only investigated the different ways to construct new ABoxes. The next step is to indicate what it means for an ABox to be repaired with respect to the active TBox. We will make use of concepts that are counterparts of those that we already presented in Chapter 2 about active integrity constraints to show the relation between the two settings. We start by the definitions of weak repair and PMA repair.

Definition 3.9. Let A and T be an ABox and a TBox respectively such that A is inconsistent with respect to T .

A weak repair of A achieving T is an update sequence S A

A such that A S A A is consistent with respect to T . 2. A PMA repair of A achieving T is a weak repair of A achieving T that is minimal with respect to the number of steps needed, i.e., there is no weak repair of A achieving T in fewer steps.

Next we define the notion of foundedness on the level of syntactic modifications and on the level of update sequences.

Definition 3.10. Let A and aT be an ABox and an active TBox respectively such that A is inconsistent with respect to aT . A syntactic modification U A A is founded if there is an active constraint η on aT such that: 1. A is not consistent with respect to body(η).

2.

A is consistent with respect to body(η).

U A

A either adds or removes a concept according to the update actions in head(η).

Furthermore, an update sequence S A

A is founded if for every U ∈ S A A there is an active constraint η on aT such that U is founded.

Finally, using the above definitions, we define founded weak repairs and founded repairs as follows.

Definition 3.11. Let A and aT be an ABox and an active TBox respectively such that A is inconsistent with respect to aT .

An update sequence S A

A is a founded weak repair of A by aT if S A A is a weak repair of A achieving static(aT ) and S A A is founded.

An update sequence S A

A is a founded repair of A by aT if S A A is a PMA repair of A achieving static(aT ) and S A A is founded.

Summing up, let A be an ABox and aT an active TBox such that A is inconsistent with respect to aT . A repaired ABox with respect to aT is any ABox A ∈ R A such that S A A is a founded weak repair of A by aT . A minimally repaired ABox with respect to aT is any ABox A ∈ R A such that S A A is a founded repair of A by aT . Since by Proposition 3.2 there is a finite number of ABoxes that we can construct step by step from the initial ABox using the set Γ A , the sets of repaired and minimally repaired ABoxes with respect to aT are also finite. This means that we can start from the set of ABoxes R A 1 and continue searching all the sets R A n for n > 0 until we find a minimally repaired ABox with respect to aT .

We now return to the original example of The ABoxes A and A also showcase in practice the difference between removing and forgetting concepts that we discussed in Section 3.2. Since we defined minimality to be relative to the number of syntactic modifications needed and not interpretation-wise, both

A and A are considered to be minimally repaired.

Discussion and Conclusion

In this chapter we explored and discussed the ways in which active constraints, which originate from the database community, could be integrated into the TBoxes of Description Logic. Based on these 'active' TBoxes, we then investigated a syntactic approach of transforming an ABox (inconsistent with an active TBox) step-by-step by syntactic modifications to a repaired one, conforming to the preferred update actions found in the active constraints of the extended TBox.

As we discussed, applying the idea behind AICs to the DL setting via the extension of TBox axioms with preferred update actions is not as straightforward as it is for databases. The main limitations of this chapter that we will try to tackle moving forward are (1) the fact that a syntactic repairing method cannot address inferred inconsistencies and (2) the fact that the preferred update actions of the active TBoxes deal only with atomic concepts. An example of the first case is when a concept is defined in the TBox and does not explicitly appear inside the ABox but is inferred, as is showcased in the following example.

Example 3.1. Consider the following active TBoxes:

aT 1 = {B ≡ E F, A B ⊥ → {remove(B)}} aT 2 = {B E F → {remove(B)}, E F B → {remove(E)}, A B ⊥ → {remove(B)}} aT 3 = {B ≡ E F, A E F ⊥ → {remove(E)}, A B ⊥ → {remove(B)}} and the ABoxes A 1 = {α : A E F } and A 2 = {α : A B E F }.
Using aT 1 we would not be able to provide a founded repair for any of the two ABoxes. For A 1 the source of inconsistency (the concept B) is inferred by the first definition but cannot be removed as is. Similarly for A 2 . The only way to overcome this issue is by defining more precise active TBoxes. We can witness this with aT 2 , which provides a founded repair for A 2 , and even more with aT 3 , which provides a founded repair for both ABoxes.

criteria. The dynamic logic framework also allows us to lift the approach of [START_REF] Feuillade | A dynamic view of active integrity constraints[END_REF] from propositional databases to DLs.

We consider that TBoxes are sets 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. A simple example from [START_REF] Liu | Foundations of instance level updates in expressive description logics[END_REF] is the following: consider the ABox A = {John : ∃hasChild.Happy, Mary :

Happy The chapter is structured as follows. Section 4.2 presents syntax and semantics of formulas and programs. In Section 4.3 we prove decidability of the logic through reduction axioms eliminating programs from formulas in a similar fashion to DL-PA. In Section 4.4

we transpose the notions of weak repairs and PMA repairs to the DL setting and use the programs of our language to constructively represent them. Section 4.5 is the main contribution of the chapter where we apply the idea behind active integrity constraints to Description Logic TBoxes and explore founded and dynamic repairs in a similar manner as in the database literature. We conclude in Section 4.6.

Syntax and Semantics

The update of an ABox is represented with the help of PDL programs. Their behavior is identical with the programs of PDL, with formulas of the form π ϕ 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.

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:

ϕ ::= A | {a} | ⊥ | ϕ → ϕ | ∃r.ϕ | Uϕ | π ϕ | π c ϕ π ::= +A(a) | -A(a) | π; π | π ∪ π | π * | ϕ?
where A ∈ Con, a ∈ Ind, and r ∈ R. Similarly, Ind(π) denotes the set of all individuals occurring in π.

Interpretations and their Updates

• ∆ I = ∆ I • a I = a I • A I = A I ∪ {a I | +A(a) ∈ U } \ {a I | -A(a) ∈ U } • r I = r I
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).

Semantics

The semantics of a formula is w.r.t. an interpretation I: it is a set of individuals of ∆ I . The semantics of a program is a relation on interpretations. The extension of • I to complex formulas is defined inductively as follows:

{a} I = {a I } ⊥ I = ∅ ϕ → ψ I = ∆ I \ ϕ I ∪ ψ I ∃r.ϕ I = {δ ∈ ∆ I | there is δ ∈ ∆ I such that (δ, δ ) ∈ r I and δ ∈ ϕ I } Uϕ I =      ∆ I if ϕ I = ∆ I ∅ otherwise π ϕ I = (I,I )∈ π ϕ I π c ϕ I = (I ,I)∈ π ϕ I
while the semantics of programs is: Note that the test program is interpreted globally. 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.

(I, I ) ∈ || + A(
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 describe it. What is of interest to us is that the set A U equals the set of interpretations satisfying π U c A, where π U is the program that applies the update actions of U . In this way, as we will soon see, we will be able to obtain a unique syntactic representation of the set A U through the formula π U c A of our logic.

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 [START_REF] Ditmarsch | Dynamic Epistemic Logic[END_REF]. We start with the reduction axioms for complex programs.

Proposition 4.1. The following equivalences are valid:

π 1 ; π 2 ϕ ↔ π 1 π 2 ϕ π 1 ∪ π 2 ϕ ↔ π 1 ϕ ∨ π 2 ϕ π * ϕ ↔ π ≤2 n ϕ ψ? ϕ ↔ ϕ ∧ Uψ
where n = card(Con(π)) × card(Ind(π)).

Proof. For an equivalence ϕ ↔ ψ to be valid, it suffices to show that ϕ I = ψ I for any interpretation I. For an arbitrary interpretation I then we have:

• π 1 ; π 2 ϕ I = (I,I )∈ π 1 ;π 2 ϕ I = (I,I )∈ π 1 (I ,I )∈ π 2 ϕ I = (I,I )∈ π 1 π 2 ϕ I = π 1 π 2 ϕ I • π 1 ∪ π 2 ϕ I = (I,I )∈ π 1 ∪π 2 ϕ I = (I,I )∈ π 1 ∪ π 2 ϕ I = (I,I )∈ π 1 ϕ I ∪ (I,I )∈ π 2 ϕ I = π 1 ϕ I ∪ π 2 ϕ I = π 1 ϕ ∨ π 2 ϕ I •
In dynALCO, programs can only modify the assertions (i.e., the status of atomic concepts on individuals) that occur in them. This means that for any program π with

Con(π) = {A 1 , . . . , A n }: if (I, I ) ∈ ||π * || then A I = A I for A = A i , i ∈ {1, . . . , n}
Furthermore, by the semantics of update actions:

if (I, I ) ∈ ||π * || then A I \ A I ⊆ Ind(π) and A I \ A I ⊆ Ind(π) for all A ∈ Con(π)
More formally, let us define π(I) = {I | (I, I ) ∈ ||π||}. Then we have that:

π * (I) = {I | A I \ A I ⊆ Ind(π) and A I \ A I ⊆ Ind(π) for all A ∈ Con(π)}
It follows that for a given interpretation I there are at most 2 card(Con(π))×card(Ind(π)) dif- ϕ I = ∅ and ϕ ∧ Uψ

I = ϕ I ∩ Uψ I = ϕ I ∩ ∅ = ∅
Observe that, contrarily to PDL and just as in DL-PA, the Kleene star can be eliminated. The next proposition shows how to reduce atomic programs.

Proposition 4.2. The following equivalences are valid: Proposition 4.3. The following equivalences are valid:

+A(a) B ↔      {a} ∨ B if A = B B otherwise -A(a) B ↔      ¬{a} ∧ B if A = B B otherwise ±A(a) {b} ↔ {b} ±A(a) ⊥ ↔ ⊥ ±A(a) (ϕ → ψ) ↔ ±A(a) ϕ → ±A(a)
+A(a) c ϕ ↔ (a : A) ∧ ϕ ∨ -A(a) ϕ -A(a) c ϕ ↔ (a : ¬A) ∧ ϕ ∨ +A(a) ϕ π 1 ; π 2 c ϕ ↔ π 2 c π 1 c ϕ π 1 ∪ π 2 c ϕ ↔ π 1 c ϕ ∨ π 2 c ϕ π * c ϕ ↔ π ≤2 n c ϕ ψ? c ϕ ↔ ψ? ϕ
where n = card(Con(π)) × card(Ind(π)).

Proof. For an arbitrary interpretation I we have:

• If a I / ∈ A I : +A(
I = ϕ I 1 ∪ ϕ I 2 • -A(a) c ϕ I = (a : ¬A) ∧ ϕ ∨ +A(a) ϕ I
similarly to the previous procedure but reversing the arguments.

• π 1 ; π 2 c ϕ I = (I ,I)∈ π 1 ;π 2 ϕ I = (I ,I )∈ π 1 (I ,I)∈ π 2 ϕ I = (I ,I)∈ π 2 (I ,I )∈ π 1 ϕ I = (I ,I)∈ π 2 π 1 c ϕ I = π 2 c π 1 c ϕ I • π 1 ∪ π 2 c ϕ I = (I ,I)∈ π 1 ∪π 2 ϕ I = (I ,I)∈ π 1 ∪ π 2 ϕ I = (I ,I)∈ π 1 ϕ I ∪ (I ,I)∈ π 2 ϕ I = π 1 c ϕ I ∪ π 2 c ϕ I = π 1 c ϕ ∨ π 2 c ϕ I • From the proof of Proposition 4.1 we have that (I, I ) ∈ ||π * || iff (I, I ) ∈ ||π ≤2 n ||,
where n = card(Con(π)) × card(Ind(π)). Therefore:

π * c ϕ I = (I ,I)∈ π * ϕ I = (I ,I)∈ π ≤2 n ϕ I = π ≤2 n c ϕ I where n = card(Con(π)) × card(Ind(π)) • ψ? c ϕ I = (I ,I)∈ ψ? ϕ I = (I,I )∈ ψ? ϕ I = ψ? ϕ I since (I 1 , I 2 ) ∈ ψ? iff (I 2 , I 1 ) ∈ ψ?
Using now Propositions 4.1, 4.2 and 4.3 we obtain the following theorem.

Theorem 4.1. Every formula of dynALCO is equivalent to a static formula.

Proof. Let ϕ be any arbitrary dynALCO-formula. As we mentioned at the beginning of this section, we start by using Proposition 4.1 together with the last four equivalences of Proposition 4.3 iteratively until all complex programs inside ϕ are eliminated and ϕ ends up comprising only atomic programs. We then use the last four equivalences of Proposi- Last but not least, decidability of global satisfiability in dynALCO follows from the fact that any static formula can be mapped to an ALCO(U)-concept and vice versa and that concept satisfiability in ALCO(U) is decidable [START_REF] Horrocks | The even more irresistible SROIQ[END_REF]. This correspondence between static dynALCO-formulas and ALCO(U)-concepts is realized through the following one-to-one and onto mapping τ (note that we use the connectives ¬ and ∨ in the place of ⊥ and → since the former are easier to present):

• τ (A) = A • τ ({a}) = {a} • τ (¬ϕ) = ¬τ (ϕ) • τ (ϕ ∨ ψ) = τ (ϕ) τ (ψ) • τ (∃r.ϕ) = ∃r.τ (ϕ) • τ (Uϕ) = ∀r U .τ (ϕ)
where A ∈ Con, a ∈ Ind, and r ∈ R (recall also that r U is the universal role). Thus, (global) satisfiability checking of the static fragment of our logic can be reduced to the satisfiability problem of ALCO(U).

Lemma 4.1. Let ϕ be a static dynALCO-formula which is mapped to the ALCO(U)concept C, i.e., τ (ϕ) = C. Then ϕ is (globally) satisfiable iff the concept ∀r U .C is satisfiable.

Proof. First of all, by induction on ϕ it is easy to prove that τ (ϕ) I = ϕ I for any interpretation I. Since the first four cases are quite trivial we only give the details for the last two.

• Let ϕ = ∃r.ψ and suppose the induction hypothesis holds for ψ, i.e., τ (ψ)

I = ψ I .
Then:

τ (ϕ) I = τ (∃r.ψ) I = ∃r.τ (ψ) I = {δ ∈ ∆ I | there is δ ∈ ∆ I such that (δ, δ ) ∈ r I and δ ∈ τ (ψ) I } = {δ ∈ ∆ I | there is δ ∈ ∆ I such that (δ, δ ) ∈ r I and δ ∈ ψ I } = ∃r.ψ I = ϕ I
• Let ϕ = Uψ and suppose the induction hypothesis holds for ψ, i.e., τ (ψ)

I = ψ I .
Then:

τ (ϕ) I = τ (Uψ) I = ∀r U .τ (ψ) I = {δ ∈ ∆ I | for all δ ∈ ∆ I , if (δ, δ ) ∈ r I U then δ ∈ τ (ψ) I } = {δ ∈ ∆ I | for all δ ∈ ∆ I , δ ∈ ψ I } = {δ ∈ ∆ I | ψ I = ∆ I } =      ∆ I if ψ I = ∆ I ∅ otherwise = Uψ I = ϕ I
Now let ϕ be globally satisfiable. This means that there exists a model of ϕ, i.e., there is an interpretation I such that ϕ I = ∆ I and subsequently

C I = ∆ I since ϕ I = τ (ϕ) I = C I .
Similarly to before, we have that (∀r U .C)

I = {δ ∈ ∆ I | C I = ∆ I }. But C I = ∆ I
and thus (∀r U .C) I = ∆ I . This gives (∀r U .C) I = ∅, i.e., the concept ∀r U .C is satisfiable.

On the other direction, if the concept ∀r U .C is satisfiable then there exists an interpretation I such that (∀r U .C) I = ∅. This means that there exists a δ ∈ (∀r U .C) I and since

(∀r U .C) I = {δ ∈ ∆ I | C I = ∆ I } then C I = ∆ I . From C I = τ (ϕ) I = ϕ I it follows
that ϕ I = ∆ I as well, i.e., ϕ be globally satisfiable.

Using Lemma 4.1 now we obtain the following theorem.

Theorem 4.2. Global satisfiability in the logic dynALCO is decidable.

Proof. Deciding whether a dynALCO-formula ϕ is (globally) satisfiable is realized by

(1) finding a static formula ψ that is equivalent to ϕ through Theorem 4.

Weak Repairs and Repairs

From now on we consider a fixed satisfiable TBox T together with a fixed finite set Con of atomic concepts and Ind of individual names. Furthermore, we consider for the rest of the chapter that all ABoxes we work with are consistent. We proceed to define the notions of weak repair and repair of an ABox A with respect to T , i.e., a modification of the ABox such that A is consistent with the concept inclusion axioms of T . We recall that an ABox

A is inconsistent with respect to T iff there is no interpretation satisfying both A and T , and that in dynALCO this amounts to unsatisfiability of the formula T ∧ A. We start with the definition of a weak repair.

Definition 4.2. Let T ∧A be unsatisfiable. A weak repair of A is a consistent set of update actions U such that T ∧ (A U ) is satisfiable.

We continue with the definition of a repair, which is based on the principle of minimal change and Winslett's possible models approach [Winslett, 1988, Winslett, 1990, Herzig and Rifi, 1999].

Definition 4.3. Let T ∧ A be unsatisfiable. A (PMA) repair U of A is a weak repair of A
that is minimal with respect to set inclusion, i.e., such that T ∧ (A U ) is unsatisfiable for all U ⊂ U .

We showcase the above definitions in the following simple example. 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 weak repair using less update actions. It is easy to see that this can be achieved through the program:

gotoAltInt(A) = A∈Con a∈Ind + A(a) ∪ -A(a) * ; A ?
Summing up, we use the above to create the formula: 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.

Minimal(A) = ¬ gotoAltInt(A) ;
Last but not least, let mkFalse ± abbreviate the program which falsifies all the asser-tions of the form A + (a) and A -(a) for all A ∈ Con and a ∈ Ind. The program mkFalse ± 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.

Theorem 4.3. Let A be inconsistent with respect to T 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 weak repair of A iff there exists an I such that:

(I, I U ) ∈ A ? ; weakRepair

• U is a repair of A iff there exists an I such that: For the second item, we can see how the construction of repair(A) via the programs toggle ± (A(a)), gotoAltInt(A), redo(A(a)) and undo(A(a)) makes sure that there is no alternative model of A that achieves consistency with T using less update actions. The procedure is based on the respective one for the propositional case of Chapter 2, with the difference being that now it doesn't suffice to just undo some update actions and check if the ensuing interpretation is a model of T . Indeed, due to the open world semantics of ABoxes there is no unique model of A (as was the case with databases) and we may begin from a 'problematic' model of A which needs extra update actions to tackle inconsistencies between (possibly irrelevant) individuals of the model and axioms of the TBox.

(I, I U ) ∈ A ∧ A∈Con a∈Ind ¬(a : A + ) ∧ ¬(a : A -) ? ; repair(A) ; mkFalse ± Proof.
In such a case, the update actions chosen from the toggle ± (A(a)) program may indeed be minimal with respect to the specific interpretation and just retracting them may lead to interpretations that are not models of T , thus incorrectly identifying them as a minimal set of update actions repairing A. To be sure we did not choose such an inappropriate interpretation, we need to visit all possible models of A and check for each one that it cannot achieve consistency with less update actions by means of the redo(A(a)) and undo(A(a))

programs. All of these are realized with the use of the new concepts of the form A + and A -, similarly to those of Chapter 2, ending with the mkFalse ± program which removes them from U .

Active Inclusion Axioms in ALC TBoxes

In this section we once again import the idea behind active integrity constraints into DL, but this time we also 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. The following are reformulations of Definitions 3.1, 3.2 and 3.3.

Definition 4.4. A concept inclusion of the form C 1 • • • C n ⊥ is called a static concept inclusion.
Note that in ALC, any concept inclusion axiom is equivalent to a static concept inclusion.

Definition 4.5. Let r = C 1 • • • C n ⊥ be a static concept inclusion. An active concept inclusion is of the form r, V where V is a set of indexical update actions such that:

• if +A ∈ V then there exists C i = ¬A. • if -A ∈ V then there exists C i = A.
An active TBox, denoted by aT , is a set of active concept inclusions.

For an active concept inclusion η = r, V we let static(η) = r and active(η) = V .

Note that active(η) can be empty. For an active TBox aT we let static(aT ) = {static(η) :

η ∈ aT } and active(aT ) = η ∈aT active(η). We say that aT extends T iff T is equivalent to static(aT ).

Going back to the example of Section 4.1, we observe that the active TBox aT conforms to the above definitions. Note also that static(aT ) is equivalent to T . We also recall that we have fixed a satisfiable TBox T together with a finite set Con of atomic concepts and Ind of individuals. From now on, we also consider a fixed active TBox aT that extends T . 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 .

Similarly to Chapter 2, the former are based on [START_REF] Caroprese | Active integrity constraints for database consistency maintenance[END_REF]Truszczynski, 2011] while the latter are based on [START_REF] Feuillade | A dynamic view of active integrity constraints[END_REF].

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.6. 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. is unsatisfiable for all U ⊂ U , then U is a founded repair of A.

The following simple example showcases this definition. In order to find a founded weak repair we have to ensure that the foundedness condition of Definition 4.6 holds after the update actions of the toggle ± (A(a)) program of the previous section. To do this, we define the following formula:

Founded = A∈Con a∈Ind a : A + ∨ a : A -→ η∈aT ±A∈active(η) + A(a) ∪ -A(a) ¬static(η)
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 Then the following theorem completes the picture.

Theorem 4.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 founded weak repair of A iff there exists an I such that:

(I, I U ) ∈ A∧

Dynamic Weak Repairs and Dynamic Repairs

We now investigate dynamic repairs which we have met before in Chapter 2 and 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 ± π a η are defined as follows:

π a η = ¬ a : static(η) ? ; ±A∈active(η)
±A(a)

+ π a η = +A∈active(η) + A(a) ; +A + (a) -π a η = -A∈active(η) -A(a) ; +A -(a) ± π a η = ¬ a : static(η) ? ; + π a η ∪ -π a η
Intuitively, the program π a η will check for each active concept inclusion η and individual 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 dynamic repairs.

Definition 4.8. 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∈Ind η∈aT π a η If T ∧ (A U ) is unsatisfiable for all U ⊂ U , then U is a dynamic repair of A.
It is worth noting that, just as in the propositional case, dynamic weak repairs are not necessarily founded. The next example showcases this. We now use 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:

dynamicRep(A) = while ¬T do a∈Ind η∈aT ± π a η ; Minimal(A) ?
we have the following theorem.

Theorem 4.5. 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:

(I, I U ) ∈ A ∧ A∈Con a∈Ind ¬(a : A + ) ∧ ¬(a : A -) ? ; dynamicRep(A) ; mkFalse ± Proof.
Once again the proof is trivial and based on the definitions, since the only additional thing we do is keep track of the update actions that take place in the course of the while program in order to check for minimality with the familiar procedure of the previous theorems. As always, we end the procedure by removing the stored concepts.

Going back to Example 4.4 this time we can witness how, taking I to be a model of {John : Born ¬Alive ¬Dead}, only the set {+Alive(John)} satisfies the condition of Theorem 4.5 whereas the set {+Alive(John), +Dead(John)} does not for any I.

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 which, when applied to an ABox, produces a repaired ABox The foundedWeakRepair program is defined in terms of a simple 'generate and test' schema. We just observe here that one might however further exploit dynALCO by replacing foundedWeakRepair by a program that is the dynALCO counterpart of some algorithm computing founded weak repairs.

A slightly different route, more in line with Description Logic, would be to define a repair to be any repaired ABox A and, given an ABox A, evaluate if A is indeed a repair of A by checking if the formula A ∧ repair A is satisfiable, where repair is any of the repair programs defined in the previous sections and used in Theorems 4.3, 4.4 and 4.5. Of course we then would have to guess such a repair A , 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 a repair of A by checking whether the formula repair c A is satisfiable, where A is the initial ABox. Indeed, any interpretation that satisfies the formula repair c A will be a model of at least one repaired ABox.

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 4.5, the TBox T = {∃hasFather.Female ⊥} can be only extended to from [START_REF] Liu | Foundations of instance level updates in expressive description logics[END_REF] applies here as well). Consequently, there may exist repairs that we cannot express in order to check if they result from the preferences specified by an active TBox. For this reason the ABoxes we will be working with will also incorporate nominals. Similarly to the previous chapter, both the TBox and the ABox are represented in our language by single formulas.

We continue with the presentation style of the previous chapters and give a glimpse of what we are able to achieve in this one. More specifically, we are able to construct exactly the active TBoxes of Section 1.1 and have their intended meaning as discussed.

We recall that the starting TBox T was the following:

{Father Male Parent, OnlyChild ∀hasSibling.⊥}

The active TBoxes aT 1 = {η 1 , η 2 , η 3 } and aT 2 = {η 4 , η 5 } then which we want to extend

T have the following form: with the preferred update actions on the left part of each active axiom having the respective meaning. This structure for active axioms also enables us to transform them directly into atomic programs. Moreover, contrarily to the first semantic approach that we investigated in the previous chapter, the preferred update actions this time can be applied on any subset of the domain rather than to specific individuals. More precisely, each of them is applied to the subset of the domain containing all individuals which violate its respective axiom.

η 1 : +Male if ¬ (Father Male Parent)
The chapter is structured as follows. In Section 5.2 we present syntax and semantics of the formulas and programs. In Section 5.3 we show decidability of the logic with the same procedure of reducing it to the fragment which contains no programs. In Section 5.4

we define the notion of standard repairs which are not based on preferred update actions but merely on repairing assertions based on the axioms that they violate. Section 5.5

comprises the definition of this chapter's active TBoxes and Section 5.6 explores dynamic repairs in the current setting. Finally, we conclude in Section 5.7 with a discussion around the presented approach.

Syntax and Semantics

We recall that a knowledge base KB = (T , A) consists of a TBox T and an ABox A. The ABox is constructed from a finite set of concept assertions a : C and role assertions r(a, b)

where C is a complex concept of the DL language, r is a role and a, b are individuals.

Similarly, the TBox is constructed from a finite set of axioms whose form again depends on the DL at hand. In this chapter we use the language of the description logic ALCI for As for the dynamic logic framework, it has PDL-style formulas of the form π ϕ expressing that ϕ is true after some possible execution of the program π. The main differences with PDL are the absence of the Kleene star and the atomic level of the programs:

whereas PDL has abstract atomic programs, the atomic programs of our language have the form 'λ if ϕ' where λ is a program applied on the individuals that satisfy the formula ϕ.

Moreover, the programs of our language can be once again eliminated and every formula is reducible to a static formula, i.e., a formula without programs. Last but not least, the models of our logic are identical with the models of Chapter 4, i.e., interpretations of the underlying Description Logic.

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 A more complex example is ∀r 1 .-r 2 .(B ∧ ∃r 3 .A) which when applied to an individual a is the program that removes all relations r 2 (b, c) for each b such that r 1 (a, b) where c satisfies B ∃r 3 .A. Last but not least, the reader may have noticed that there is an asymmetry between the local programs concerning (1) addition of atomic concepts but not roles and (2) application of local programs through universal quantification but not through existential quantification. This is due to some technical limitations that the latter cases would have as well as the existence of scenarios where either the addition of roles or the addition of concepts to only one individual through a role prove to be unintuitive.

We will discuss more on this distinction later in the concluding section.

In the third level are the programs that are used on all individuals. For this reason we Finally, we denote by Ind(A), Con(A) and Role(A) the sets of all individuals, atomic concepts and roles, respectively, that occur in the ABox A.

Semantics

We recall that an interpretation is a couple I = (∆ I , • I ) where ∆ I is the domain and • I is the interpretation function that maps each atomic concept A to a subset of the domain, each role r to a binary relation on the domain and each individual a to an element of the domain, i.e., A I ⊆ ∆ I , r I ⊆ ∆ I × ∆ I and a I ∈ ∆ I . The extension of • I to inverse roles and complex formulas is defined inductively as follows: Lastly, let ϕ be a formula. We say that ϕ is (globally) satisfiable iff there exists an interpretation I such that ϕ I = ∆ I . We say that ϕ is valid iff ϕ I = ∆ I for every interpretation I. Paralleling the previous chapter, we call the logic that is built using this syntax and semantics dynALCIO since it is an extension of the logic ALCIO with dynamic logic elements.

r c I = {(b, a) ∈ ∆ I × ∆ I | (a, b) ∈ r I } {a} I = {a I } ⊥ I = ∅ ϕ → ψ I = ∆ I \ ϕ I ∪ ψ I
A I =      A I ∪ ϕ I if ± A is + A A I \ ϕ I if ± A is -A (I, I ) ∈ -r.ϕ 1 if ϕ 2 iff ∆ I = ∆ I , a I = a I , A I = A I , R I = R I for R = r and: r I = r I \ {(a, b) | a ∈ ϕ I 2 , b ∈ ϕ I 1 } (I, I ) ∈ -r c .ϕ 1 if ϕ 2 iff (I, I ) ∈ -r.ϕ 2 if ϕ 1 (I, I ) ∈ ∀r.λ if ϕ iff (I, I ) ∈ λ if

Reduction and Mathematical Properties

This time we convert the formulas of dynALCIO that contain programs to equivalent static formulas which contain no programs. Exactly as in Section 4.3, we achieve this reduction by first reducing complex programs to atomic programs and second by eliminating an atomic program which is inside a formula by finding an equivalent formula without it. We start with the reduction axioms for complex programs.

Proposition 5.1. The following equivalences are valid:

π 1 ; π 2 ϕ ↔ π 1 π 2 ϕ π 1 ∪ π 2 ϕ ↔ π 1 ϕ ∨ π 2 ϕ ψ? ϕ ↔ ϕ ∧ Uψ
Proof. The proof for all three equivalences is identical to the respective cases on the proof of Proposition 4.1.

The next three proportions show how to reduce the atomic programs.

Proposition 5.2. The following equivalences are valid:

∀r.λ if ϕ ψ ↔ λ if ∃r c .ϕ ψ ∀r c .λ if ϕ ψ ↔ λ if ∃r.ϕ ψ
where r ∈ R.

Proof. For an arbitrary interpretation I we have:

λ if ϕ {a} ↔ {a} λ if ϕ ⊥ ↔ ⊥ λ if ϕ (ψ 1 → ψ 2 ) ↔ λ if ϕ ψ 1 → λ if ϕ ψ 2 λ if ϕ ∃r.ψ ↔              ¬ϕ ∧ ∃r. λ if ϕ ψ ∨ ϕ ∧ ∃r.(¬ϕ ∧ λ if ϕ ψ) if λ=-r.ϕ -r.ϕ if ϕ ∃r.ψ if λ=-r c .ϕ ∃r. λ if ϕ ψ otherwise λ if ϕ ∃r c .ψ ↔              ¬ϕ ∧∃r c . λ if ϕ ψ ∨ ϕ ∧∃r c .(¬ϕ∧ λ if ϕ ψ) if λ=-r.ϕ -r.ϕ if ϕ ∃r c .ψ if λ=-r c .ϕ ∃r c . λ if ϕ ψ otherwise λ if ϕ Uψ ↔ U λ if ϕ ψ
where a ∈ Ind, r ∈ R and λ has one of the following forms: +A, -A, -r.ϕ, -r c .ϕ.

Proof. The first three equivalences as well as the last one are proved similarly to the respective cases of Proposition 4.2. Regarding the remaining two, suppose I is an arbitrary interpretation. Then we have that:

• -r.ϕ if ϕ ∃r.ψ • Similarly for λ if ϕ ∃r c .ψ

Proposition 5.4. The following equivalences are valid:

+A if ϕ B ↔      A ∨ ϕ if A = B B otherwise -A if ϕ B ↔      A ∧ ¬ϕ if A = B B otherwise -r.ϕ 1 if ϕ 2 A ↔ A -r c .ϕ 1 if ϕ 2 A ↔ A
where A, B ∈ Con and r ∈ R.

Proof. The first two equivalences are once again similar to those of Proposition 4.2. For the other two, let I be an arbitrary interpretation. We have: which is clearly the expected outcome.

• -r.ϕ 1 if ϕ 2 A I = (I,I )∈ -r.ϕ 1 if ϕ 2 A I = A I
From Propositions 5.1, 5.2, 5.3 and 5.4 we then obtain the following theorem.

Theorem 5.1. Every formula of dynALCIO is equivalent to a static formula.

Proof. The procedure is the same as in Theorem 4.1: given a dynALCIO-formula ϕ, iterative applications of the equivalences in Proposition 5.1 will result in a formula without complex programs that is equivalent to ϕ. With the equivalences of Proposition 5.2 then all local programs of the form ∀r.λ and ∀r c .λ are eliminated from within the atomic programs. Next, using Proposition 5.3 the atomic programs can be pushed through the boolean connectives, the universal and existential quantifiers, as well as the universal operator. Finally, all of the atomic programs are eliminated by applying iteratively the equivalences of Proposition 5.4 together with the first equivalence of Proposition 5.3.

Since all equivalences are valid we obtain a static formula that is equivalent to ϕ.

Through Theorem 5.1 we can now reduce every formula of the logic which we work with to the static fragment of the logic which contains no programs. Decidability of global satisfiability in dynALCIO then follows using the same argument of the previous chapter: any static formula can be mapped to an ALCIO(U)-concept and vice versa and concept satisfiability in ALCIO(U) is decidable [START_REF] Horrocks | The even more irresistible SROIQ[END_REF]. The mapping τ that achieves the correspondence between static dynALCIO-formulas and ALCIO(U)concepts extends the previous mapping in the obvious way (where we once again use the connectives ¬ and ∨ in the place of ⊥ and →), i.e.:

• τ (A) = A • τ ({a}) = {a} • τ (¬ϕ) = ¬τ (ϕ) • τ (ϕ ∨ ψ) = τ (ϕ) τ (ψ) • τ (∃r.ϕ) = ∃r.τ (ϕ) • τ (∃r c .ϕ) = ∃r c .τ (ϕ) • τ (Uϕ) = ∀r U .τ (ϕ)
where A ∈ Con, a ∈ Ind, and r ∈ R (with r U the universal role). Then (global) satisfiability checking of the static fragment of dynALCIO is similarly reduced to the satisfiability problem of ALCIO(U) and we obtain the following theorem.

Theorem 5.2. Global satisfiability in the logic dynALCIO is decidable.

Both the proof of Theorem 5.2 as well as the lemma that it is based on are identical to the respective of Section 4.3 and are omitted.

Associating Local Programs with TBox Axioms

We can now make use of the language of dynALCIO and, as a first step, show how to build a (non-dynamic) repairing procedure that checks whether an assertion or ABox can be obtained as a result of repairing an initial ABox that is inconsistent with a TBox through a bounded number of steps. Through this problem we showcase the flexibility of the programs that can be built using our dynamic logic framework. We recall that an ABox A is inconsistent with a TBox T iff there is no model of (T , A), i.e., iff the formula T ∧ A is (globally) unsatisfiable in our logic. Furthermore, we consider for the rest of the chapter that all TBoxes we work with are consistent and all ABoxes we work with are consistent: we focus then on cases where their conjunction is inconsistent due to the interaction between them. We start by defining the set of update actions that each TBox axiom can be paired with.

Definition 5.1. Let ρ be any concept inclusion axiom. The set pr(ρ) of programs associated with ρ is defined inductively as follows:

pr(A) = {+A, -A} pr(¬C) = pr(C) pr(C 1 C 2 ) = pr(C 1 ) ∪ pr(C 2 ) pr(∀r.C) = {-r.¬C} ∪ {∀r.λ | λ ∈ pr(C)} pr(∀r c .C) = {-r c .¬C} ∪ {∀r c .λ | λ ∈ pr(C)} pr(C D) = pr(C) ∪ pr(D)
The set pr(ρ) is defined to contain all local programs that can be constructed from each ρ ∈ T based on the intuitions given in Section 5.2. For example, consider the concept inclusion ρ = A ∀r.¬B. According to Definition 5.1, the set pr(ρ) comprises the following programs: +A, -A, -r.B, ∀r.+B, ∀r.-B. Clearly, not all of them can provide a repairing solution. For example, consider the assertion a : A ∃r.B which is not consistent with ρ. The programs +A and ∀r.+B when applied to a do not provide a repaired assertion because the sources of the inconsistency are not tackled by these programs, while the programs -A, -r.B and ∀r.-B do so. So the set pr(ρ), although finite, contains arbitrary local programs constructed from ρ many of which may not be suitable when repairing an assertion or ABox that is inconsistent with ρ. This does not pose a threat though as that ineffective subset of pr(ρ) can be ignored during the repairing procedure or, in the worst case, raise the number of computations needed without modifying the result.

Standard Repairs

Given the set pr(ρ) we can now define the program that tries to repair an ABox that is inconsistent with a TBox T by updating the individuals which violate some ρ ∈ T with random update actions based on the concepts and roles of each ρ ∈ T . Since this program does not depend on any active axioms (that we will introduce in the next section)

and since there is no preference between the update actions chosen, we call it a standard repair program.

Definition 5.2. Let T be a TBox and n ∈ N. The standard repair program up to n of T is the following program:

π n T = ρ∈T λ∈pr(ρ) λ if ¬ρ ≤n ; T ?
It is easy to see what this program does: it applies at most n times update actions from the axioms of T that are violated until T is ultimately satisfied. So now we are in a position to take advantage of the atomic programs of our logic to build decision procedures that can check whether specific ABoxes are repairs or not. More specifically, if T is a TBox and A is an ABox that is inconsistent with T , we can decide if an assertion or ABox A is the outcome of repairing A (by using at most n computations). This is possible by checking if the formula A∧ π n T A is satisfiable in our logic and is articulated in the next proposition. The reader may wonder whether we could just check satisfiability of the formula T ∧ A in order to see if A is a repair of A. As we show in Example 5.2 below, through the satisfiability of the formula A ∧ π n T A we can also check if A is a repair of A that results from updating the individuals according to the axioms they violate, so A is not any random ABox. Furthermore, we know that we can achieve this with at most n computations.

We continue with the definition of relevance between two ABoxes. Definition 5.3. Let A and A be two ABoxes. We say that A is relevant to A iff:

• Ind(A ) ⊆ Ind(A) • Con(A ) ⊆ Con(A) • Role(A ) ⊆ Role(A) • if r(a, b) ∈ A then r(a, b) ∈ A
The role of relevance is to make sure that a repair of an ABox does not contain irrelevant concept and role assertions. For instance, when repairing the ABox A = {a : ¬A} which is inconsistent with the TBox T = { A}, the ABox A = {r(a, b), b : B} should not be a repair of A, although the formula A ∧ π 1 T A is satisfiable, because both of its assertions have nothing to do with A.

Next is the main definition of this section, viz. that of a standard repair.

Definition 5.4. Let T be a TBox and let A be an ABox. An ABox A is a standard repair of A with respect to T iff A is relevant to A and the formula A ∧ π n T A is satisfiable for some n ∈ N.

So, in other words, a standard repair of A with respect to T is an ABox that can be built from updating assertions of A so that they conform with the axioms of T and that doesn't contain any irrelevant (with respect to A) concept and role assertions or new individuals. Note that since the program π n T can apply quite arbitrary update actions from the set pr(ρ) for each ρ ∈ T , standard repairs can diverge more from the initial ABox than desired. A simple example that highlights this follows. T A 1 is satisfiable using the atomic program:

-hasSpouse.Man if ¬ (Man ∀hasSpouse.¬Man) and thus, according to Proposition 5.5 and Definition 5.4, A 1 is consistent with T and is also a standard repair of A with respect to T . If we just checked satisfiability of the formula T ∧ A 2 though, where:

A 2 = {John:¬Person, Peter:¬Person, hasSpouse(John, Peter), hasSpouse(Peter, John)} then we would have that A 2 is also a repair of A with respect to T , although the way to obtain A 2 from A is irrelevant with the axioms of T that were violated by A and seems rather undesirable. Last but not least, according to Definition 5.4 a standard repair of A with respect to T is also the ABox A 3 = {John : ¬Man, Peter : ¬Man} using the atomic programs:

∀hasSpouse.-Man if ¬ (Man ∀hasSpouse.¬Man) -hasSpouse.¬Man if ¬ (¬Man ∀hasSpouse.Man) which, although consistent with T and a standard repair of A with respect to T , is also a debatable repair.

So, although we can check whether a possible repair of the initial ABox can be achieved using a bounded number of computations, this procedure can also provide other, quite undesirable ABoxes through the application of too many update actions to the initial ABox. We can separate then the standard repairs into two classes: those that are achieved through a minimal number of computations and those that are not. The next definition singles out the classes of standard repairs based on the minimum number of computations required.

Definition 5.5. Let T be a TBox and let A be an ABox that is inconsistent with T . The set of all standard repairs of A with respect to T is denoted by StandRep(T , A). The subset of StandRep(T , A) comprising the standard repairs that can be achieved with a minimum of n computations is denoted by StandRep n (T , A).

Given Definition 5.5, the way to check if an ABox belongs to the set StandRep n (T , A) for some n ∈ N is given next.

Proposition 5.6. Let T be a TBox and let A be an ABox that is inconsistent with T . For an ABox A then, A ∈ StandRep n (T , A) iff:

• A is relevant to A • the formula A ∧ π n T A is satisfiable • the formula A ∧ π n-1 T A is unsatisfiable Proof. For the left to right direction, if A ∈ StandRep n (T , A) then A is a standard
repair of A and thus A is relevant to A as well as the formula A∧ π n T A is satisfiable for some n ∈ N. The fact that A can be achieved with a minimum of n computations means that A ∧ π m T A is satisfiable for all m ≥ n. Furthermore, satisfiability of A ∧ π n-1 T A would obviously mean that A can also be achieved with n -1 computations and A / ∈

StandRep n (T , A). Thus A ∧ π n-1 T A is unsatisfiable.
For the right to left direction, the first two items give that A is a standard repair of A that can be achieved within n steps. By the third item, for all m < n -1 the formulas A ∧ π m T A are also unsatisfiable since a repair that can be achieved with at most m steps can also be achieved with more than m (imagine the rest of the steps being the ' ?' programs in the definition of 'γ ≤n '). This means that A needs at least n steps and

A ∈ StandRep n (T , A).
As mentioned in this proof, if the formula A ∧ π n T A is satisfiable then the formula A ∧ π m T A is also satisfiable for any m > n. Furthermore, there exists a minimal k ∈ N such that the formula A ∧ π k T A is satisfiable and this k is the minimum number of steps needed to obtain A from A. Based on this we have the following proposition.

Proposition 5.7. For every TBox T and ABox A, either StandRep(T , A) = ∅ or there exists an n ∈ N such that: Non-existence of a repair can be the case when there is an inconsistency that cannot be repaired because the sets pr(ρ) do not provide any adequate update actions based on Definition 5.1. Consider e.g. the TBox T = { ∃r. } and the ABox A = {a : ∀r.⊥}.

• StandRep n (T , A) = ∅ • StandRep m (T , A) = ∅ for all m < n
Then StandRep(T , A) = ∅. We will come back to this later in the concluding discussion.

For every T and A with StandRep(T , A) = ∅ we denote the set StandRep n (T , A)

satisfying Proposition 5.7 by MinStandRep(T , A). This is the set that comprises the standard repairs which require the least amount of computations. We thus obtain the definition of minimal standard repairs.

Definition 5.6. Let T be a TBox and let A be an ABox that is inconsistent with T . An ABox A is a minimal standard repair of A with respect to T iff A ∈ MinStandRep(T , A).

Going back to Example 5.2 then we can witness that A 1 ∈ StandRep 1 (T , A) whereas

A 3 ∈ StandRep 2 (T , A), and since MinStandRep(T , A) = StandRep 1 (T , A) we con- clude that A 1 is a minimal standard repair whereas A 3 is not. Furthermore, A 2 / ∈ StandRep(T , A).
Therefore, there is a way to avoid debatable repairs like A 3 by searching only for minimal standard repairs. The way to obtain the minimum number of computations required for each repairing procedure is given in the following proposition.

Proposition 5.8. Let T be a TBox and let A be an ABox that is inconsistent with T . We In the next section we are going to provide a framework and tools for more informed ways of repairing ABoxes. As with earlier chapters, this will be achieved by endowing TBox axioms with preferred update actions through which they should be repaired in case of inconsistency. As we discussed in Section 5.1, the distinguishing feature of the present approach is the global nature of the update actions and their greater expressiveness.

have that MinStandRep(T , A) = StandRep k (T , A) iff: • the formula A ∧ π k T is satisfiable • the formula A ∧ π k-1 T is unsatisfiable

Active Inclusion Axioms in ALCI TBoxes

In this section we use the structure of the programs in our quest to enrich the axioms of the TBoxes with update actions. We then examine the various results we can obtain when we start from an ABox that is inconsistent with a TBox and modify it via these preferred update actions such that it is ultimately consistent with the concept inclusion axioms of the TBox. The first thing to do is to define the static and active concept inclusions.

Definition 5.7. Any concept inclusion axiom ρ is called a static concept inclusion. An active concept inclusion is of the form 'λ if ¬ρ' where λ ∈ pr(ρ). An active TBox, denoted by aT , is a set of active concept inclusions.

For η ='λ if ¬ρ' we let static(η) = ρ. For an active TBox aT we let static(aT ) = {static(η) : η ∈ aT }. We say that aT extends T iff T = static(aT ). The next definition extends the notion of inconsistency.

Definition 5.8. Let aT be an active TBox. We say that an ABox A is consistent with aT iff

A is consistent with static(aT ). Similarly, A is inconsistent with aT iff A is inconsistent with static(aT ).

We can see now that the active TBoxes of Section 5.1 can be expressed in this framework and, more specifically, that static(aT 1 ) = static(aT 2 ) = T .

Active TBoxes are a way for an ontology engineer to specify preferred update actions to tackle inconsistencies. Our goal now is to provide appropriate tools that check whether an assertion (or a whole ABox) is indeed the outcome of applying these preferred update actions a bounded number of times. More specifically, given an active TBox aT and an ABox A that is inconsistent with aT , we would like to define a program π n aT that uses the active inclusion axioms of aT to determine whether or not the formula A ∧ π n aT A is satisfiable for an assertion or ABox A . We thus introduce in the following section the notion of dynamic repair programs, which choose among the update actions in aT in order to provide repair solutions given an upper bound on the number of steps. Their construction resembles the dynamic repairs we have seen in Chapters 2 and 4.

Dynamic Repairs

We now investigate dynamic repair programs which make use of the setting of Dynamic Logic in order to provide a dynamic perspective on the repair procedure; more specifically, by making use of the restricted while programs of dynALCIO we are able to iterate the process of applying the preferred update actions and apply each one at a time until all the inconsistencies are eliminated after a bounded number of computations. We begin with the basic definition. So, in a similar manner as before, we can now utilize the atomic programs of our logic to build decision procedures that check if an assertion or ABox A is indeed the outcome of applying the preferred update actions of an active TBox after a bounded number of steps. We can witness this in the following corollary.

Corollary 5.1. Let aT be an active TBox, let A be an ABox, let A be either an assertion or an ABox and let n ∈ N. If the formula A ∧ π n aT A is satisfiable then A is consistent with aT .

Proof. Consider A ∧ π n

aT A is satisfiable. By Proposition 5.9 the formula A ∧ π n T A is also satisfiable, where T = static(aT ). Proposition 5.5 then gives that T ∧ A is consistent or, equivalently, that A is consistent with T . By Definition 5.8 then A is also consistent with aT .

Once again, satisfiability of the formula A ∧ π n aT A provides much more than just consistency checking: it also makes sure that the assertion or ABox A conforms to the active axioms of aT as well as ensures we can achieve this with at most n repair steps.

The definition of a dynamic repair immediately follows.

Definition 5.10. Let aT be an active TBox and let A be an ABox. An ABox A is a dynamic repair of A with respect to aT iff A is relevant to A and the formula A∧ π n aT A is satisfiable for some n ∈ N. Going back to the example of Section 5.1 again (see also the example on Section 1.1), we can check now that: with respect to aT 1 and aT 2 , respectively, by checking that both of the formulas A ∧ π 2 aT 1 A 1 and A ∧ π 2 aT 2 A 2 are satisfiable. Furthermore, using the reduction axioms of Section 5.3 we have that: Last but not least, for an active TBox aT let us restrict static(aT ) to the subsets of each pr(ρ) that comprise the local programs of each active axiom η ∈ aT . For an ABox A then it is easy to see that A is a dynamic repair of A with respect to aT iff A is a standard repair of A with respect to static(aT ). We end the section with a corollary based on this observation that shows the relationship between standard and dynamic repairs.

Corollary 5.2. Let T be a TBox, let aT = {λ if ¬ρ | ρ ∈ T and λ ∈ pr(ρ)} and let A be an ABox. An ABox A is a dynamic repair of A with respect to aT iff A is a standard repair of A with respect to T . Furthermore, MinDynRep(aT , A) = MinStandRep(T , A) and thus A is a minimal dynamic repair of A with respect to aT iff A is a minimal standard repair of A with respect to T .

Proof. The left to right direction is immediate since it is easy to check by Definition 5.10 and Proposition 5.9 that every dynamic repair of A with respect to aT is also a standard repair of A with respect to static(aT ). For the other direction, we recall (from the proof of Proposition 5.9) that π n

Discussion and Conclusion

In this chapter we have proposed a richer framework for defining extensions of TBoxes with active axioms, specifying preferred repairing routes in case their static part is violated by an ABox. We tackled the problem of checking whether there exists a repair of an ABox that is inconsistent with a TBox in a bounded number of computations through dynamic logic programs. Furthermore, given a possible repair of an ABox, we have shown how to check whether or not it can be obtained from the active axioms of the TBox under a bounded number of steps and, in case it is indeed a repair, whether or not it can do so with the least amount of steps possible.

The reader may have noticed that we make no effort to repair an axiom of the form Even in our framework, there exist cases where one should be careful with concepts like the previous example. More specifically, when a concept appears inside an axiom and, in case of inconsistency of the axiom with an ABox, repairing this concept amounts to 'something should exist' then an alternative repairing route might be better pursued by the active axioms. For instance, the axiom 'ρ = Grandparent ∃hasChild.Parent' should only be extended as follows:

-Grandparent if ¬ (Grandparent ∃hasChild.Parent)

since the inconsistency that comes from the concept '∃hasChild.Parent' is not trivial: the assertion John : Grandparent ¬∃hasChild. is inconsistent with this axiom but cannot be repaired by adding properties to John's children (since he doesn't have any). Therefore, in order to assure that a repairing procedure will not fail, an ontology engineer should not 'risk' putting the update action '∀hasChild.+Parent' which is the only other meaningful program from the set pr(ρ) apart from '-Grandparent'. Although for another individual (that has children) it could provide a drastic repair (drastic in the sense that all children would be parents, although at least one is needed), it will always fail for John since the formula:

John : Grandparent ∧ ¬∃hasChild. ∧ π n aT is unsatisfiable for all n ∈ N when the update action '∀hasChild.+Parent' is the only choice.

Our approach in this chapter and the logic we use don't allow to check whether a possible (standard or dynamic) repair exists in general, since StandRep(T , A) = ∅ iff the formula A ∧ π n T is satisfiable for some n ∈ N (and respectively DynRep(aT , A) = ∅ iff the formula A ∧ π n aT is satisfiable for some n ∈ N). We thus have a positive answer in case a (standard or dynamic) repair exists but we are not able to decide in case there isn't. The compromise we make though gives us some extra information, i.e., we can check if a repair exists within a specific number of computations and, in case there is, what is the minimal number of computations through which we can achieve this. This makes sense in real world applications where a big deviation from the original ABox may not be desirable. This means that, in practice, if a transaction has turned an ABox that is consistent with aT into one that is inconsistent with aT then the dynamic repair should only involve few active axioms. It follows that the maximal allowed number of update actions can reasonably be expected to be rather low. Now, in order to be in a position to check if a repair exists in the general case, the logic dynALCIO has to be extended with the 'Kleene star' operator of PDL, similarly to the logic dynALCO of Chapter 4. Then we would be able to abbreviate an arbitrary finite number of applications of 'λ if ¬ρ' with a single program π aT , thus deciding the existence of a dynamic repair by checking if the formula A ∧ π aT is satisfiable or not. However, the addition of this program makes the reduction to the static fragment unachievable and the logic dynALCIO extended with the 'Kleene star' operator is not guaranteed to be decidable anymore. This is showcased in the following example, where (.) * is the Kleene star operator.

Example 5.3. Let I be an interpretation such that: The reason this didn't happen for dynALCO is the combination of the local nature of its update actions with the less expressive power of its atomic programs. But as we argued before, deciding the existence of a standard or dynamic repair in general may not be very interesting, since the repair might be too divergent from the original ABox and difficult to pinpoint. So with the approach we took in this chapter, an ontology engineer can set a benchmark by specifying the maximum number of operations within which a repair should be achieved and, in case this is not possible, it may be an indication that the active axioms defined in the active TBox may be suboptimal in producing a desirable repair.

• ∆ I =
Summing up, we have taken a more elaborate semantic approach to the investigation of repairing ABoxes with regard to active TBoxes, the latter being an extension of regular TBoxes with update actions inspired by the active integrity constraints of the database literature. This time we have exploited a dynamic logic framework admitting global semantics for atomic programs on which various decision procedures are introduced and compared. Having successfully overcome both limitations that we set out to do at the end of Chapter 3, we end the thesis by combining the aforementioned semantic proposal to evaluating repaired ABoxes with the syntactic proposal to constructing them.

CHAPTER 6

Conclusion

Throughout the course of this thesis we investigated methods for maintaining the integrity and consistency of knowledge bases, both in the propositional and in the DL setting, with a specific goal in mind: extend propositional databases and description logic TBoxes with preferred update actions and take them carefully into account when searching for repairing solutions. Whereas the landscape in the propositional case was already explored and understood, the extension to higher level languages like Description Logics proved to be non-trivial and challenging. Relying mainly on Dynamic Logic we acquired tools for both representing known procedures in our setting as well as constructing new, dynamic ones.

Speaking of Dynamic Logic, and as we already mentioned at the end of Section 1.2.3, a correspondence between DLs and (variants of) PDL has been achieved early on [Schild, 1991]. Let us note at this point that we do not attempt something similar here.

In practice, we merely extend ALCO and ALCIO with simple atomic (and complex) programs that ultimately reduce to static ALCO(U) and ALCIO(U) concepts. Thus, our logics are as expressive as plain ALCO(U) and ALCIO(U), respectively, and do not admit regular expressions over roles like role union, role composition, reflexive-transitive closure of roles and role identity. This makes DLs admitting regular expressions over roles like ALCO reg and ALCIO reg strictly more expressive than dynALCO and dynALCIO, since the universal role can be expressed in the former by the union and the reflexivetransitive closure of roles.

Our approaches also come close to the work presented in [START_REF] Ahmetaj | Managing change in graph-structured data using description logics[END_REF] where dynamic problems on graph-structured data are reduced to static DL reasoning.

The Dynamic Logic framework presented here though is different and allows us to not be restricted into finite interpretations, among other things. Furthermore, we introduce and work mainly with active TBoxes, which differentiates us from other approaches to tackle (possibly dynamic) problems in DLs using regular TBoxes.

Last but not least, let us note that our perspective in this thesis differs from [START_REF] Motik | Bridging the gap between OWL and relational databases[END_REF], Tao et al., 2010], since we do not split the TBox up into integrity constraints and other, non-integrity axioms. The direction we pursue is clearly different from their attempts to encode integrity constraints into TBoxes, which differentiate the KB from the set of integrity constraints, treating the latter with a closed-worlds assumption and using different dedicated semantics. Nevertheless, it looks like a promising future direction to import their way of handling integrity constraints inside TBoxes and see how such an approach would compare with our own in this thesis.

We now conclude our investigations with an attempt at connecting the two different directions we took for repairing ABoxes: constructing them syntactically and assessing them semantically. We recall from Chapter 3 that, starting from an ABox A, the set S A consists of all concept symbols occurring in A. Furthermore, the set R A comprises the ABoxes that can be reached from A by an arbitrary number of syntactic modifications and it is always finite. These syntactic modifications however take place only for atomic concepts and not for nominals or roles. Since in Chapter 5 we are working on ALCIO and nominals can exist in ABoxes, we now extend the set S A into the set S * A which also includes the nominals of the ABox A and also define the sets A * , A * , A * ¬ , Γ * A:A and Γ * A accordingly. We can then also extend all the definitions of Section 3. Taking these new syntactic modifications into account, we can see how all ABoxes in the new set R A follow Definition 5.3 and are relevant to A since no new individuals, concepts or roles are introduced and role assertions can be only removed. This means that searching for repairs in the set R A is safe and, given an active TBox aT , satisfiability of the formula A ∧ π n aT A for some n ∈ N and A ∈ R A is enough to identify A as a dynamic repair of A with respect to aT . So now the number n ∈ N can have a dual purpose: both an upper bound that specifies the maximum number of (semantic) updates within which a repair should be found as well as an upper bound on the number of syntactic modifications that the initial ABox should be the subject of. In other words, for an upper bound k ∈ N, we only check if the formula A ∧ π k aT A is satisfiable where:

A ∈ k n=1 R A n (1)
If no dynamic repair is found in this way then we stop. Of course, since all of the sets R A n as well as the set R A are finite, we could search if A ∧ π k aT A is satisfiable for all A ∈ R A . The purpose of limiting the A s such that (1) holds is to once again showcase methods for not straying too far away from the initial ABox. and A 2 ∈ R A 2 by means of S A 2 A = {¬Man → Man}, {¬Male → Male} . Note also that A 2 ∈ DynRep 2 (aT , A) and thus A 2 is not a minimal dynamic repair although it is a dynamic repair achieved with the least number of syntactic modifications. Finally, it is easy to check that the update sequence S A 3 A = {¬Man → Man} is a PMA repair of A according to Chapter 3, but A 3 / ∈ DynRep(aT , A) according to Chapter 5.

So one can choose to look for dynamic repairs in R A by interpreting minimality either way s/he wants, pursuing one of the following:

• After fixing the number k, go though all ABoxes A in R A 1 , R A 2 , . . . and check whether A ∧ π k aT A is satisfiable. The first ABox for which this is the case will be a dynamic repair achieved with the least number of syntactic modifications. We reiterate that we can either exhaust R A or stop at R A k .

• After pinpointing the number k for which DynRep k (aT , A)=MinDynRep(aT , A)

with the procedure of Chapter 5, check for any A ∈ R A whether A ∧ π k aT A is satisfiable. The first ABox for which this is the case will be a minimal dynamic repair.

It is clear though that immediate applications of the above procedures in real world scenarios may be computationally impractical. Thus, next research steps should consist of finding 'reasonable' complexity bounds for working with active TBoxes. In connection to Section 1.4, an attempt to combine our results with other areas of research could be to look at possible applications of the proposed repairing methods on nonmonotonic scenarios such as Defeasible Description Logics [Britz andVarzinczak, 2016, Britz andVarzinczak, 2017]. In particular, the preferential approach for nonmonotonic reasoning that has been established in the propositional setting has already been extended to DLs [Casini andStraccia, 2010, Giordano et al., 2015] and applying the results reported in this thesis to such a defeasible setting seems like an interesting future endeavor.

Summing up, by venturing into the landscape of active TBoxes we exhibited that preferences when repairing Description Logic KBs can constitute very interesting and important research directions, much like AICs on databases that came before them. Although a first-and quite theoretical-step in this direction, we believe that the basic idea behind active TBoxes is proving to be fruitful.

  Mots clefs: Contraintes d'Intégrité Active, Logique Dynamique, Logique de Description, Gestion de l'Inconsistance, Réparation de Bases de Données CHAPTER 1 Introduction Contents 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Background and State of the Art . . . . . . . . . . . . . . . . 4 1.3 Contributions and Outline of the Thesis . . . . . . . . . . . . 15 1.4 Other Contributions . . . . . . . . . . . . . . . . . . . . . . . 17

η 1 :

 1 Father Male Parent, {+Male, +Parent} η 2 : OnlyChild ∀hasSibling.⊥, {-OnlyChild} η 3 : Father Male Parent, {-Father} η 4 : OnlyChild ∀hasSibling.⊥, {-hasSibling. }

Figure 1 . 1 :

 11 Figure 1.1: Interpretation of formulas and programs.

C

  D and r s or C ≡ D and r ≡ s, where C, D are concept descriptions and r, s are role descriptions of the DL language. Axioms of the first kind are called concept and role inclusions whereas axioms of the second kind are called concept and role equalities.Furthermore, equalities whose left-hand side is an atomic concept or role name are called definitions. For any two atomic concept names A and B, if B appears on the right-hand side of the definition of A then we say that A directly sees B. We also say that A sees B to describe the transitive closure of the relation directly sees. If the TBox contains an atomic concept name that sees itself then the TBox contains a cycle. If it doesn't contain any such atomic concept name then the TBox is acyclic. In the course of this thesis we will mainly use TBoxes which contain concept inclusion axioms and they can be either cyclic or acyclic. Finally, the ABoxes are constructed from a finite set of assertional axioms of two types: the concept assertions a : C and the role assertions r(a, b) where a, b are individuals, C is a concept description and r is a role description which again depend on the DL language at hand. In Chapter 3 we use the language of the description logic ALC for both TBoxes and ABoxes. In Chapter 4 we stay on ALC for TBoxes, but we use its extension ALCO with nominals for ABoxes. In Chapter 5 the language of the slightly more expressive description logic ALCI is used for TBoxes and its extension ALCIO is used for ABoxes. Moving on, an interpretation I satisfies a concept inclusion C D if C I ⊆ D I and, respectively, a role inclusion r s if r I ⊆ s I . Similarly for concept and role equalities: I satisfies C ≡ D if C I = D I and I satisfies r ≡ s if r I = s I . An interpretation I satisfies a concept assertion a : C if a I ∈ C I and I satisfies a role assertion r(a, b) if (a I , b I ) ∈ r I . An interpretation that satisfies all terminological axioms of a TBox T is called a model of T . Similarly, an interpretation that satisfies all assertional axioms of an ABox A is called a model of A. Last but not least, an interpretation is a model of a KB = (T , A) if it is both a model of T and a model of A. If there is a model of a KB we say that the KB is consistent, or equivalently, that A is consistent with respect to T . We end the presentation on the fundamental notions of DLs by introducing the most important reasoning tasks for TBoxes and ABoxes. The subsumption problem is the problem of whether a concept is more (or less) general than another, i.e., given the concept descriptions C and D, whether C I ⊆ D I for all interpretations I. If the problem is relative to a TBox T then the question transforms into whether C I ⊆ D I for all models I of T . When this is the case then we write C T D or T |= C D. The satisfiability problem for a concept description C is the problem of whether there exists an interpretation I such that C I = ∅. When this is the case then we say that I is a model of C. Once again, if the problem is relative to a TBox T then the question transforms into whether C I = ∅ for a model I of T . Another reasoning task is the instance checking problem, which is the problem of whether an assertion follows from a specific ABox A, i.e., given the concept description C, the role description r and the individuals a, b, whether a I ∈ C I and (a I , b I ) ∈ r I for all models I of A. When this is the case then we write A |= a : C and A |= r(a, b), respectively. It is worth mentioning that most reasoning tasks in DLs are reducible to one another.

  else fail = p ± ?; p ←¬p; p ± ←⊥ As announced above, p ± keeps track of the modifications of p: we are going to ensure that it is true only once p has been modified during the current update. The program toggle(p) flips the truth value of p if this value has not been modified yet and records the modification by setting p ± to ; if p has already been made true then toggle(p) fails. The program undo(p) undoes this.

  these are exactly the test programs in ne + (p) and ne -(p).

Remark 2 .

 2 abbreviates:

  , {B+? ← } ask for B to be true, x being true b 3 : ¬A+? ∨ A+! ∨ A± ∨ B+? ∨ ¬B+! ∨ ¬x , {A± ← } record the intermediate state b 4 : ¬A+? ∨ A+! ∨ ¬A± ∨ B+? ∨ ¬B+! ∨ ¬x , {B+! ←⊥} x being true, erase the result for B b 5 : ¬A+? ∨ A+! ∨ ¬A± ∨ B+? ∨ B+! ∨ ¬x , {x ←⊥} now make x false b 6 : ¬A+? ∨ A+! ∨ ¬A± ∨ B+? ∨ B+! ∨ x , {B+? ← } ask for B to be true, x being false b 7 : ¬A+? ∨ A+! ∨ ¬A± ∨ B+? ∨ ¬B+! ∨ x , {A+! ← } A is now proved true b 8 : ¬A+? ∨ ¬A+! ∨ ¬A± ∨ B+? ∨ ¬B+! ∨ x , {B+! ←⊥} remove the result for B b 9 : ¬A+? ∨ ¬A+! ∨ ¬A± ∨ B+? ∨ B+! ∨ x , {A± ←⊥} remove the intermediate state b 10 : ¬A+? ∨ ¬A+! ∨ A± ∨ B+? ∨ B+! ∨ x , {A+? ←⊥} end the request for A Lemma 2.5. Let A ∈ subf ∀ (G) and V ⊆ subf v (G). Furthermore, consider that the induction hypothesis holds for B, where A = ∀x.B, i.e., both of IndHyp(B, V \ {x}) +and IndHyp(B, V ∪ {x}) + hold. Then:V |= A iffthere is a dynamic weak repair of V ∪ {A+?} by {b 1 , . . . , b 10 } Proof. Consider A = ∀x.B, the database V and the set of active constraints η = {b 1 , . . . , b 10 }. If V |= A then V \ {x} |= B and V ∪ {x} |= B (1). Starting from V ∪ {A+?} then, as a first step we make sure that x is true through b 1 . We then check, in a similar manner as before, that B is indeed satisfied for both truth values of x. This is done through the active constraints b 2 to b 6 . The only difference here is that we have to record an intermediate state via the variable A± when switching from x being true to x being false. The reason is that, if this intermediate state is not recorded through b 3 , a database which doesn't include the variable x will violate both b 1 and b 6 and may jump to the latter constraint, thus not checking if B is satisfied when x is true. The rest is the same: the auxiliary variables are removed from the database before ending the check in b 10 . By (1) then, since B is indeed satisfied for both truth values of x, and b 3 as well as b 7 are both violated, using the induction hypothesis we have that the procedure is ending and a dynamic weak repair of V ∪ {A+?} by η exists. On the other hand, if a dynamic weak repair of V ∪ {A+?} by η exists then, similarly with before, B has been proved to be satisfied for both truth values of x: for x in the transition from b 2 to b 3 and for ¬x and in the transition from b 6 to b 7 . By induction hypothesis then, this means that V \ {x} |= B and V ∪ {x} |= B and thus V |= A. • When A = ¬B we set: c 1 : ¬A+? ∨ A+! ∨ B-? ∨ B-! , {B-? ← } ask for B to be false c 2 : ¬A+? ∨ A+! ∨ B-? ∨ ¬B-! , {A+! ← } A is now proved true c 3 : ¬A+? ∨ ¬A+! ∨ B-? ∨ ¬B-! , {B-! ←⊥} remove the result for B c 4 : ¬A+? ∨ ¬A+! ∨ B-? ∨ B-! , {A+? ←⊥} end the request for A c 5 : ¬A-? ∨ A-! ∨ B+? ∨ B+! , {B+? ← } ask for B to be true c 6 : ¬A-? ∨ A-! ∨ B+? ∨ ¬B+! , {A-! ← } A is now proved false c 7 : ¬A-? ∨ ¬A-! ∨ B+? ∨ ¬B+! , {B+! ←⊥} remove the result for B c 8 : ¬A-? ∨ ¬A-! ∨ B+? ∨ B+! , {A-? ←⊥} end the request for A

  there is a dynamic weak repair of V ∪ {A-?} by {c 5 , c 6 , c 7 , c 8 } Proof. For the first case, consider A = ¬B, the database V and the set of active con-straints η = {c 1 , c 2 , c 3 , c 4 }. Clearly, if V |= A then V |= B (1). So starting from

d 1 :

 1 ¬A+? ∨ A+! ∨ B+? ∨ C+? ∨ B+! ∨ C+! , {B+? ← } ask for B to be trued 2 : ¬A+? ∨ A+! ∨ B+? ∨ C+? ∨ ¬B+! ∨ C+! , {C+? ← }ask for C to be trued 3 : ¬A+? ∨ A+! ∨ B+? ∨ C+? ∨ ¬B+! ∨ ¬C+! , {A+! ← } A is now proved trued 4 : ¬A+? ∨ ¬A+! ∨ B+? ∨ C+? ∨ ¬B+! ∨ ¬C+! , {B+! ←⊥} remove the result for B d 5 : ¬A+? ∨ ¬A+! ∨ B+? ∨ C+? ∨ B+! ∨ ¬C+! , {C+! ←⊥} remove the result for C d 6 : ¬A+? ∨ ¬A+! ∨ B+? ∨ C+? ∨ B+! ∨ C+! , {A+? ←⊥} end the request for A d 7 : ¬A-? ∨ A-! ∨ B-? ∨ C-? ∨ B-! ∨ C-! , {B-? ← , C-? ← } ask for B or C to be false

  there is a dynamic weak repair of V ∪ {A+?} by {d 1 , . . . , d 6 }• V |= A iff there is a dynamic weak repair of V ∪ {A-?} by {d 7 , . . . , d 12 }

e 2 :

 2 ¬A+? ∨ ¬A+! ∨ ¬A , {A+? ←⊥} end the request for A e 3 : ¬A-? ∨ A-! ∨ A , {A-! ← } A is proved false e 4 : ¬A-? ∨ ¬A-! ∨ A , {A-? ←⊥} end the request for A Lemma 2.8. Let A ∈ subf v (G) and V ⊆ subf v (G). Then: • V |= A iff there is a dynamic weak repair of V ∪ {A+?} by {e 1 , e 2 } • V |= A iff there is a dynamic weak repair of V ∪ {A-?} by {e 3 , e 4 }

  . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 3.2 Integrating Active Constraints to the TBox . . . . . . . . . . 71 3.3 A Syntactic Way of ABox Repairing . . . . . . . . . . . . . . 76 3.4 Discussion and Conclusion . . . . . . . . . . . . . . . . . . . 83

  resulting extended TBoxes are called active TBoxes in accordance with the nomenclature of active constraints. This extension of TBox axioms is achieved by means of the operations add(A) and remove(A), where A is an atomic concept. The intuition behind add(A) and remove(A) is similar to the one we have seen for AICs, i.e., whenever an inclusion axiom of the form C D ⊥ appears inside the TBox, for literals 1 C and D, then the TBox should also indicate the preferred way that this should be repaired when the axiom is violated in an ABox. While the problem is easier when an assertion of the form a : A B has to be updated to either the assertion a : A ¬B or the assertion a : A, difficulties start to arise when such a conjunction appears inside the scope of a quantifier, e.g. when having to update the assertion a : ∃R.(A B) to the either a : ∃R.(A ¬B)

Figure 3 . 2 :

 32 Figure 3.2: Removing (1) vs. forgetting (2)

  Figure 3.3: Example of an active TBox, based on the TBox of Figure 3.1

  Consider for instance the active constraint η = A B ⊥ → {remove(B)} and an ABox which includes only the assertions a : ∀ r. (A B) and r(a, b) for two individuals a and b. We would like to repair this ABox with respect to η into the ABox having either a : ∀ r. (A ¬B) or a : ∀ r. A as an assertion for the individual a 2 . From a semantic point of view, however, it is not clear what set of update actions would achieve

  denotes the set of concepts that can be reached with one step from S A using the three boolean constructors. Next, we write A [A | C] to denote the replacement in A of some instances of the atomic concept A with the concept C. Then we define the following relation. Definition 3.4. Let A and A be ABoxes. Then A ∼ 1 A iff: 1. there is an atomic concept A ∈ S A and a concept C ∈ Γ A:A such that A = A [A | C] or A = A [A | C]. 2. A and A are semantically different from one another, i.e., there exists an interpretation I such that I |= A and I |= A . The relation ∼ 1 is clearly symmetric and irreflexive. The next step is to generalise this definition to an n-step relation between two ABoxes.

  Figures 3.1 and 3.3 and examine an ABox (which is inconsistent with respect to this TBox) and two of its possible repairs. Let aT be the active TBox of Figure 3.3 and consider the following ALC-ABox: A = {John : Person Married Bachelor ∃ hasChild. (Divorced Widowed), Mary : Person ¬Married ¬Divorced ¬Bachelor ¬Widowed} A minimally repaired ABox with respect to aT is the following: A = {John : Person Married ∃ hasChild. Divorced, Mary : Person ¬Married ¬Divorced Bachelor ¬Widowed} A founded repair of A by aT then is the update sequence S A A = (U 1 , U 2 , U 3 ) where U 1 = {Married Bachelor → Married}, U 2 = {Divorced Widowed → Divorced} and U 3 = {¬Bachelor → Bachelor}. Notice also that if we replace U 1 by U 1 = {Bachelor → ¬Bachelor} and U 2 by U 2 = {Widowed → ¬Widowed} in S A A , the new update sequence S A A = (U 1 , U 2 , U 3 ) is also a founded repair of A by aT , where A S A A is the ABox: A = {John : Person Married ¬Bachelor ∃ hasChild. (Divorced ¬Widowed), Mary : Person ¬Married ¬Divorced Bachelor ¬Widowed}

  Clever} which we want to update by making Mary unhappy. The resulting ABox then would have the form A = {John : ∃hasChild.(Happy {Mary}), Mary : ¬Happy Clever}. 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 based on the intuitions described in Section 1.1 and the example therein. First, consider the following TBox T : {Sibling Brother Sister, ∀hasSibling.⊥ OnlyChild} An active TBox extending T then will be aT = {η 1 , η 2 } where: η 1 : Sibling ¬Brother ¬Sister ⊥, {-Sibling} η 2 : ∀hasSibling.⊥ ¬OnlyChild ⊥, {+OnlyChild}As we already explained, through these enhanced concept inclusions we aim to be able to propose the update actions that we prefer when repairing an ABox that is inconsistent with T . More specifically, the active axioms of aT should dictate that an individual who is neither a brother nor a sister of someone should drop its sibling status, whereas an individual who has no siblings should change its status and be an only child. The direction that we pursue in this chapter is a local one, with preferred update actions like those showcased above being applied only to the level of the individuals, i.e., they have the form +OnlyChild(a) and -Sibling(b) for specific individuals a and b. This local approach to update actions comes close to the approach we have witnessed in Chapter 2 and thus the logic we propose bears many similarities with DL-PA.

Finally,

  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}).

  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., A I ⊆ ∆ I , r I ⊆ ∆ I × ∆ I and a I ∈ ∆ 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 4.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 I such that:

  a)|| iff I = I {+A(a)} (I, I ) ∈ || -A(a)|| iff I = I {-A(a)} (I, I ) ∈ ||π 1 ; π 2 || iff there exists I such that (I, I ) ∈ ||π 1 || and (I , I ) ∈ ||π 2 || (I, I ) ∈ ||π 1 ∪ π 2 || iff (I, I ) ∈ ||π 1 || ∪ ||π 2 || (I, I ) ∈ ||ϕ?|| iff I = I and ϕ I = ∆ I (I, I ) ∈ ||π * || iff (I, I ) ∈ k∈N 0 ||π|| k

  ferent interpretations I such that I ∈ π * (I) or, equivalently, such that (I, I ) ∈ ||π * ||. This means that (I, I ) ∈ ||π * || iff (I, I ) ∈ ||π ≤2 n ||, where n = card(Con(π)) × card(Ind(π)). Therefore: π * ϕ I )∈ π ≤2 n ϕ I = π ≤2 n ϕ I where n = card(Con(π)) × card(Ind(π)) • If ψ I = ∆ I : ψ? ϕ I = (I,I )∈ ψ? ϕ I = ϕ I and ϕ ∧ Uψ I = ϕ I ∩ Uψ I = ϕ I ∩ ∆ I = ϕ I If ψ I = ∆ I : ψ? ϕ

BA∆

  ψ ±A(a) ∃r.ϕ ↔ ∃r. ±A(a) ϕ ±A(a) Uϕ ↔ U ±A(a) ϕ where A, B ∈ Con, r ∈ R and a, b ∈ Ind. Proof. For an arbitrary interpretation I we have: • +A(a) A I = (I,I )∈ +A(a) A I = A I where I = I {+A(a)}. But A I = A I ∪ {a I } = I = B I where I = I {+A(a)} = B I I = A I where I = I {-A(a)}. But A I = A I \ {a I } = A I ∩ (∆ I \ {a} I ) = A ∧ ¬{a} I • -A(a) B I = (I,I )∈ -A(a) B I = B I where I = I {-A(a)} = B I • ±A(a) {b} I = (I,I )∈ ±A(a) {b} I = {b} I where I = I {±A(a)} = {b} I \ ϕ I ) ∪ ψ I = (I,I )∈ ±A(a) (∆ I \ ϕ I ) ∪ (I,I )∈ ±A(a) ψ I . But (I,I )∈ ±A(a) (∆ I \ ϕ I ) = ∆ I \ ϕ I where I = I {±A(a)}. Furthermore, ∆ I = ∆ I and thus ∆ I \ ϕ I = ∆ I \ ϕ I = ∆ I \ (I,I )∈ ±A(a) ϕ I = ∆ I \ ±A(a) ϕ I . This gives that ±A(a) (ϕ → ψ) ϕ) I = {δ ∈ ∆ I | there is δ ∈ ∆ I such that (δ, δ ) ∈ r I and δ ∈ ϕ I , where I = I {±A(a)}}. But ∆ I =∆ I and r I =r I and thus ±A(a) ∃r.ϕ I ={δ ∈ ∆ I | there is δ ∈ ∆ I such that (δ, δ ) ∈ r I and δ ∈ (I,I )∈ ±A(a) I if ϕ I = ∆ I ∅ otherwise , where I = I {±A(a)}.But ∆ I = ∆ I and ϕ I = ±A(a) reduction axioms for the converse operator follow.

  I)∈ +A(a) ϕ I = ∅ as there is no I such that I = I {+A(a)} and (a : A) ∧ ϕ ∨ -A(a) ϕ I = (a : A) I ∩ ϕ ∨ -A(a) ϕ I)∈ +A(a) ϕ I = ϕ I 1 ∪ ϕ I 2 where I 1 = I and I 2 = I {-A(a)}. Indeed, it is easy to check that (I i , I) ∈ + A(a) only for i ∈ {1, 2} when a I ∈ A I . Furthermore: (a : A) ∧ ϕ ∨ -A(a) I )∈ -A(a) ϕ I = ∆ I ∩ (ϕ I ∪ ϕ I ) where I = I {-A(a)} and consequently: (a : A) ∧ ϕ ∨ -A(a) ϕ

  tion 4.2 and the first two of Proposition 4.3 iteratively until no instance of the converse operator exists inside ϕ and all atomic programs are pushed through the boolean connectives as well as the universal/existential quantifiers and the universal operator. Finally, through the first three equivalences of Proposition 4.2 we substitute any atomic program on the left part of each equivalence with the equivalent formula on the right. Since all equivalences are valid the resulting reduced formula is equivalent to ϕ and contains no programs, i.e., ϕ is equivalent to a static formula. Through Theorem 4.1 we can now obtain a unique syntactic representation of the set A U by reducing the formula π U c A to a static one containing no programs. Example 4.1 ( [Liu et al., 2011]). Let A = {John : ∃hasChild.Happy, Mary : Happy Clever} and U = {-Happy(Mary)}. Applying the reduction axioms to: -Happy(Mary) c (John : ∃hasChild.Happy) ∧ (Mary : Happy ∧ Clever) we obtain the static formula: John : ∃hasChild.(Happy ∨ {Mary}) ∧ Mary : ¬Happy ∧ Clever which accurately represents A U .

  1 and (2) deciding whether ψ is (globally) satisfiable through Lemma 4.1. If there exists an interpretation I such that ψ I = ∆ I then ϕ I = ∆ I as well, since ϕ I = ψ I for any I. Similarly if ψ I = ∆ I for all I.

  Example 4.2. Let T = { A ∀r.B } and A = {a : A, b : ¬B, r(a, b)}. Clearly, T ∧ A is unsatisfiable. Any consistent set of update actions containing -A(a) or +B(b) is a weak repair of A. Only the sets U 1 = {-A(a)} and U 2 = {+B(b)} are repairs of A. Note that these definitions are based on the respective weak repairs and PMA repairs we have come across in Chapter 2. We now repair an ABox that is inconsistent with respect to T by means of dynALCO programs. We first define the program: weakRepair = A∈Con a∈Ind + A(a) ∪ -A(a) * ; T ? It is easy to see that, starting from an interpretation I that is a model of an ABox, any interpretation I for which (I, I ) ∈ ||weakRepair|| is a model of a repaired ABox that is consistent with T . Moreover, since by hypothesis T is satisfiable there is at least one such I . Next, we show how to capture (PMA) repairs. The first step is to 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 or removed. 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. The second step is to define the program: undo(A(a)) = (a : A + ) ? ; -A(a) ; -A + (a) ∪ (a : A -) ? ; +A(a) ; -A -(a)

  key ingredient in checking if a repair is minimal with respect to other weak repairs. Consequently:

  For the first item, suppose there exists an interpretation I such that (I, I U ) ∈ A ? ; weakRepair . This means that I is a model of A, since A I = ∆ I by the initial test. By definition then, I U is a model of A U , where U is the consistent set of update actions. Furthermore, the final test of the weakRepair program implies that I U is a model of T . Given these we have that I U is both a model of T and a model of A U , i.e., the formula T ∧ (A U ) is satisfiable. By Definition 4.2 then U is a weak repair of A. For the other direction, let U be a weak repair of A. By Definition 4.2 this means that T ∧ (A U ) is satisfiable, i.e., there is an interpretation I that is both a model of T and a model of A U . By definition again, we have that I is a model of A U iff I has the form I U where I is a model of A. This means that there is a model I of A such that I U is a model of T . So there exists an I such that (I, I) ∈ A ? and (I U, I U ) ∈ T ? . Furthermore, it is easy to see that: (I, I U ) ∈ A∈Con a∈Ind + A(a) ∪ -A(a) * and thus (I, I U ) ∈ A ? ; weakRepair .

  Let us illustrate this by continuing Example 4.2: using the sets U 1 = {-A(a)} and U 2 = {+B(b)} we can see now that they are indeed repairs of A = {a : A, b : ¬B, r(a, b)} with respect to T = { A ∀r.B }, and that they are the only such repairs.

Example 4. 3 .

 3 Consider the TBox T = {Born Alive, Alive Dead}. Consider also the following active TBox which extends T : aT = { Born ¬Alive ⊥, {+Alive} , ¬Alive ¬Dead ⊥, {+Dead} } Furthermore, consider the ABox A = {John : Born ¬Alive ¬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.

  ± (A(a)) * ; T ? ; Founded? as well as the program that searches for founded repairs: foundedRep(A) = foundedWeakRepair ; Minimal(A) ?

  : A + )∧¬(a : A -) ?; foundedWeakRepair; mkFalse ± • U is a founded repair of A iff there exists an I such that: (I, I U ) ∈ A ∧ A∈Con a∈Ind ¬(a : A + ) ∧ ¬(a : A -) ? ; foundedRep(A) ; mkFalse ± Proof. The construction of the Founded formula is based on the respective one of Section 2.4 for propositional databases and thus the arguments for the foundedWeakRepair and foundedRep(A) programs can be easily adapted from the proof of Theorem 2.3. The remaining points are similar to those of Theorem 4.3. Going back to Example 4.3 now we can witness how, taking I to be a model of {John : Born ¬Alive ¬Dead}, the set {+Alive(John)} satisfies both of the conditions of Theorem 4.4. On the other hand, the set {+Alive(John), +Dead(John)} doesn't satisfy them for any interpretation I.

  Example 4.4 (Example 4.3, ctd.). Consider again the active TBox: aT = { Born ¬Alive ⊥, {+Alive} , ¬Alive ¬Dead ⊥, {+Dead} } and the ABox A = {John : Born ¬Alive ¬Dead}, whose only founded weak repair was {+Alive(John)}. There are two dynamic weak repairs of A, namely U 1 = {+Alive(John)} and U 2 = {+Alive(John), +Dead(John)}. Only U 1 is a dynamic repair.

  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 I such that (I, I ) ∈ ||foundedRep(A)|| or (I, I ) ∈ ||dynamicRep(A)||, respectively, and setting U = {+A(a) : (a : A + ) I = ∆ I } ∪ {-A(a) : (a : A -) I = ∆ I }. 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 π U c A as in Example 4.1 or immediately apply the update U in the initial ALCO ABox and characterize A U via a semantic update of A by U .

η 2 :

 2 +Parent if ¬ (Father Male Parent) η 3 : -OnlyChild if ¬ (OnlyChild ∀hasSibling.⊥) η 4 : -Father if ¬ (Father Male Parent) η 5 : -hasSibling. if ¬ (OnlyChild ∀hasSibling.⊥)

  TBoxes and its extension ALCIO with nominals for ABoxes. The TBoxes are composed of concept inclusion axioms and the ABoxes contain (complex) concept assertions a : C and role assertions r(a, b) and r c (a, b), where C is any concept description in ALCIO, r any role and a, b individuals.

  following grammar: ϕ ::= A | {a} | ⊥ | ϕ → ϕ | ∃r.ϕ | ∃r c .ϕ | Uϕ | γ ϕ λ ::= +A | -A | -r.ϕ | -r c .ϕ | ∀r.λ | ∀r c .λ γ ::= λ if ϕ | γ; γ | γ ∪ γ | ϕ? where A ∈ Con, a ∈ Ind and r ∈ R. The logical connectives ¬, , ∧, ∨ and ↔ as well as the universal quantifier ∀ are abbreviated in the usual way. The first level is used to build formulas ϕ which represent TBoxes and ABoxes. For instance, the formula: ϕ = U (A ∧ ∃r c .(A ∨ B)) → ¬A ∧ ∀r.⊥ ∧ UA ∧ U ∀r.∃r.B represents the TBox: T = {A ∃r c .(A B) ¬A ∀r.⊥, A, ∀r.∃r.B} and vice versa. Similarly, the formula: ψ = U {a} → (A ∨ ∀r.B) ∧ U {b} → ∃r c . represents the ABox A = {a : A ∀r.B, b : ∃r c . } and vice versa. So the formula ϕ ∧ ψ represents the KB (T , A) and vice versa. We recall that U is the universal operator that makes a formula true in every individual of an interpretation. In the second level are the programs that are used on individuals. For this reason we call the λ-programs local. More specifically, the programs ±A add or remove the atomic concept A from an individual and the programs -r.ϕ and -r c .ϕ are used to remove roles: when applied to an individual a they remove all r(a, b) (respectively r c (a, b)) such that b has property ϕ. We have already seen this in the example of Section 5.1, in the form of the program -hasSibling. . Although ϕ can represent entire KBs or even incorporate programs, in practice when we use the programs -r.ϕ and -r c .ϕ the formula ϕ will be the representation of a (possibly complex) concept. Furthermore, the programs ∀r.λ and ∀r c .λ are used for going through roles in order to apply a local program λ, i.e., for an individual a they apply λ to all individuals b such that r(a, b) (respectively r c (a, b)).

  abbreviates the formula U({a} → ∃r c .{b}).

=

  {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I and b ∈ ϕ I } ∃r c .ϕ I = {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r c I and b ∈ ϕ I of global programs is: (I, I ) ∈ ±A if ϕ iff ∆ I = ∆ I , a I = a I , r I = r I , B I = B I for B = A and:

  ∃r c .ϕ (I, I ) ∈ ∀r c .λ if ϕ iff (I, I ) ∈ λ if ∃r.ϕ (I, I ) ∈ γ 1 ; γ 2 iff there exists I such that (I, I )∈ γ 1 and (I , I )∈ γ 2 (I, I ) ∈ γ 1 ∪ γ 2 iff (I, I ) ∈ γ 1 ∪ γ 2 (I, I ) ∈ ϕ? iff I = I and ϕ I = ∆ I Remember that the test program is interpreted globally. Furthermore, the semantics for formulas and programs follows the intuition we have given for them in the previous subsection. For example, the following formula: ∀r.-B if ¬A ∧ B ; -r.A if ¬A ∧ B a : (¬A ∧ ∀r.¬B) is true in an interpretation I if the assertion a : ¬A ∀r.¬B is true in the interpretation I , where I is the interpretation I after applying first ∀r.-B and second -r.A to all individuals of I that satisfy the concept ¬A B.

•

  ∀r.λ if ϕ ψ I = (I,I )∈ ∀r.λ if ϕ ψ I = (I,I )∈ λ if ∃r c .ϕ ψ I = λ if ∃r c .ϕ ψ I • ∀r c .λ if ϕ ψ I = (I,I )∈ ∀r c .λ if ϕ ψ I = (I,I )∈ λ if ∃r.ϕ ψ I = λ if ∃r.ϕ ψ I Proposition 5.3. The following equivalences are valid:

  I )∈ -r.ϕ if ϕ (∃r.ψ) I = (∃r.ψ) I for the unique interpretation I such that (I, I ) ∈ -r.ϕ if ϕ . By the definitions then (∃r.ψ)I = {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I and b ∈ ψ I } = {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I \ {(c, d) | c ∈ ϕ I , d ∈ ϕ I } and b ∈ (I,I )∈ -r.ϕ if ϕ ψ I } = {a ∈ ∆ I \ ϕ I | there is b ∈ ∆ I such that (a, b) ∈ r I and b ∈ -r.ϕ if ϕ ψ I } ∪ {a ∈ ϕ I | there is b ∈ ∆ I such that (a, b) ∈ r I and b / ∈ ϕ I and b ∈ -r.ϕ if ϕ ψ I } = ∆ I \ ϕ I ∩ ∃r. -r.ϕ if ϕ ψ I ∪ ϕ I ∩ {a ∈ ∆ I | there is b ∈ ∆ I such that (a, b) ∈ r I and b ∈ ∆ I \ ϕ I ∩ -r.ϕ if ϕ ψ I } = ¬ϕ I ∩ ∃r. -r.ϕ if ϕ ψ I ∪ ϕ I ∩ ∃r.(¬ϕ ∧ -r.ϕ if ϕ ψ) I = ¬ϕ ∧ ∃r. -r.ϕ if ϕ ψ ∨ ϕ ∧ ∃r.(¬ϕ ∧ -r.ϕ if ϕ ψ) I • -r c .ϕ if ϕ ∃r.ψ I = (I,I )∈ -r c .ϕ if ϕ (∃r.ψ) I = (I,I )∈ -r.ϕ if ϕ (∃r.ψ) I = -r.ϕ if ϕ ∃r.ψ I • Otherwise, λ has one of the following forms: +A, -A, -R.ϕ, -R c .ϕ where R = r. It is easy then to see that λ if ϕ ∃r.ψ I = ∃r. λ if ϕ ψ I based on the definitions.

  for the unique interpretation I such that (I, I ) ∈ -r.ϕ 1 if ϕ 2 . By definition thenA I = A I • -r c .ϕ 1 if ϕ 2 A I = (I,I )∈ -r.ϕ 2 if ϕ 1 A I = A I for the unique interpretation I such that (I, I ) ∈ -r.ϕ 2 if ϕ 1 . By definition again A I = A IThe next example showcases such a reduction using many of these reduction axioms. Example 5.1. Consider the atomic program ∀r.-A if B and the assertion a : ¬A ¬B which is represented by the formula U {a} → (¬A ∧ ¬B) . We show how to reduce the formula ϕ = ∀r.-A if B U {a} → (¬A ∧ ¬B) to a static one by means of the equivalences of Propositions 5.2, 5.3 and 5.4. First, ϕ is equivalent to -A if ∃r c .B U {a} → (¬A ∧ ¬B) which is in turn equivalent to U {a} → -A if ∃r c .B (¬A ∧ ¬B) .Second, we have that-A if ∃r c .B (¬A ∧ ¬B) is equivalent to ¬ -A if ∃r c .B A ∧ ¬ -A if ∃r c .B B. Furthermore, -A if ∃r c .B A is equivalent to A ∧ ¬∃r c .B and -A if ∃r c .B B is equivalent to B. These give then that: -A if ∃r c .B (¬A ∧ ¬B) ↔ ¬(A ∧ ¬∃r c .B) ∧ ¬B ↔ (¬A ∨ ∃r c .B) ∧ ¬BSo ϕ is equivalent to the formula U {a} → (¬A ∨ ∃r c .B) ∧ ¬B which represents the assertion a : (¬A ∃r c .B) ¬B. This means that the assertion a : (¬A ∃r c .B) ¬B is equivalent to the assertion a : ¬A ¬B after executing the atomic program ∀r.-A if B

  Proposition 5.5. Let T be a TBox, let A be an ABox, let A be either an assertion or an ABox and let n ∈ N. If the formula A ∧ π n T A is satisfiable then T ∧ A is consistent.Proof. Satisfiability of the formula A ∧ π n T A implies that there exists an interpretation I such that A ∧ π n T A I = ∆ I and more specifically (I,I )∈ π n T A I = ∆ I (1). In general, since the formula A is a conjunction of subformulas all of which begin with the universal operator, it holds that either A I = ∆ I or A I = ∅ for all I. Thus, by (1) there exists an I such that (I, I ) ∈ π n T and A I = ∆ I . Furthermore, if (I, I ) ∈ π n T then (I , I ) ∈ T ? . This means that there exists an I such that A I = ∆ I , T I = ∆ I and ∆ I = ∆ I which gives that T ∧ A I = ∆ I , i.e., T ∧ A is consistent.

  Example 5.2. Consider the following TBox and ABox: T = {Male Person Man, Man ∀hasSpouse.¬Man, ¬Man ∀hasSpouse.Man} A = {John : Man, Peter : Man, hasSpouse(John, Peter), hasSpouse(Peter, John)} For the ABox A 1 = {John : Man, Peter : Man} we have that A ∧ π 1

  Proof. Let StandRep(T , A) = ∅ (1). By Proposition 5.6 it is easy to see that the sets StandRep n (T , A), much like the sets R A n of Chapter 3, are pairwise disjoint and their union is the set StandRep(T , A) of all standard repairs of A with respect to T . Therefore, StandRep(T , A) = ∞ n=0 StandRep n (T , A) and by (1) ∞ n=0 StandRep n (T , A) = ∅. It follows easily that there exists an m ∈ N such that: ∞ n=0 StandRep n (T , A) = ∞ n=m StandRep n (T , A) and StandRep m (T , A) = ∅ which also gives that StandRep k (T , A) = ∅ for all k < m.

Proof.

  For the left to right direction, let MinStandRep(T , A) = StandRep k (T , A). Then StandRep(T , A) = ∅ by the definition of MinStandRep(T , A). More specifically, by Proposition 5.7 we have that (1) StandRep k (T , A) = ∅ and (2) StandRep m (T , A) = ∅ for all m < k. By (1) then there exists an ABox A such that A ∈ StandRep k (T , A)and subsequently the formulaA ∧ π k T A is satisfiable. Satisfiability of the formula A ∧ π k T follows immediately. Furthermore, let A ∧ π k-1T be satisfiable and let I be one of its models. It is easy to see then that there is an ABox A which is relevant toA for which the formula A ∧ π k-1 T A is satisfiable and has I as a model. This means StandRep m (T , A) = ∅ for some m ≤ k-1 which contradicts (2). Therefore A∧ π k-1 T is unsatisfiable.For the right to left direction, since the formula A ∧ π k-1 T is unsatisfiable the same holds for all formulas A ∧ π m T as well, where m < k -1. By Proposition 5.6 it follows that StandRep m (T , A) = ∅ for all m < k (1). Furthermore, since A ∧ π k T is satisfiable we can find an ABox A which is relevant to A that makes the formulaA ∧ π k T A satisfiable. For the same A we have that A ∧ π k-1 T A is unsatisfiable since A ∧ π k-1 T is unsatisfiable. By Proposition 5.6 again StandRep k (T , A) = ∅(2). By (1), (2), Proposition 5.7 and the definition of MinStandRep(T , A) it follows that MinStandRep(T , A) = StandRep k (T , A). So given a standard repair A of A with respect to T , in order to check if A is a minimal standard repair we need two steps: first, pinpoint the (unique) number k such that StandRep k (T , A) = MinStandRep(T , A) through Proposition 5.8 and second, check whether A ∈ MinStandRep(T , A) using Proposition 5.6; more specifically, by the second condition of Proposition 5.8 the third condition of Proposition 5.6 is implied and can be omitted. Moreover, in order to pinpoint the (unique) number k from Proposition 5.8 we can start from n = 1 and increment the value of n until the formula A ∧ π n T becomes satisfiable. If we don't want to exceed a specific bound though and iterate the previous procedure indefinitely, we can start with a satisfiability check of the formula the existence of the number k below the specified bound n we are willing to check.

  Definition 5.9. Let T be a TBox, aT an active TBox extending T and n ∈ N. The dynamic repair program up to n of aT is the following program:π n aT = while ¬T do ≤n η∈aT ηJust like the standard repair programs, the dynamic repair programs apply update actions from pr(ρ) for each ρ ∈ T that is violated until T is ultimately satisfied after a bounded number of steps. The difference is in the actual choice of these λ ∈ pr(ρ): while previously there was no preference between the update actions chosen, the update actions now are exactly those indicated by the active axioms of aT . In practice, despite their slightly different nature, dynamic repair programs are a special case of standard repair programs as is shown in the following proposition.Proposition 5.9. Let T be a TBox, aT an active TBox extending T and n ∈ N. from the fact that, unlike PDL where the program '(ϕ?; γ) ≤n ; ¬ϕ?'isnot equivalent to the program 'γ ≤n ; ¬ϕ?' since the latter can apply γ at most n times even if ¬ϕ is satisfied from the start, for active TBoxes aT with static(aT ) = T we have: This happens because applying any atomic program (λ if ¬ρ) ∈ aT from the nondeterministic composition η∈aT η in an interpretation I translates into applying the local program λ to the set (¬ρ) I = ∆ I \ ρ I . If T I = ∆ I then ρ I = ∆ I for every ρ ∈ T and thus (I, I ) ∈ η∈aT η iff I = I . It is easy to check then that: If T I = ∆ I then ρ I = ∆ I for some ρ ∈ T . More specifically, it will be the case that T I = ∅ and ρ I = ∅ due to the use of the universal operator in their representation. This means that (¬T ) I = ∆ I \ T I = ∆ I and consequently (I, I) ∈ ¬T ? . It follows that:(I, I ) ∈ ¬T ? ;

A 1 =

 1 {John : Male Father Parent, Mary : ¬OnlyChild, hasSibling(Mary, John)} A 2 = {John : Male ¬Father ¬Parent, Mary : OnlyChild} are indeed dynamic repairs of: A = {John : Male Father ¬Parent, Mary : OnlyChild, hasSibling(Mary, John)}

η 2 ;

 2 η 3 A 1 ↔ John : (Male ∧ Father) ∧ Mary : (¬OnlyChild ∨ ∃hasSibling. ) ∧ hasSibling(Mary, John) η 4 ; η 5 A 2 ↔ John : (Male ∧ ¬Parent) ∧ Mary : OnlyChild and thus A → η 2 ; η 3 A 1 and A → η 4 ; η 5 A 2 are both valid. Definitions 5.5 and 5.6 and Propositions 5.6, 5.7 and 5.8 then extend in the obvious way, with DynRep n (aT , A) comprising the dynamic repairs that can be achieved with a minimum of n computations and MinDynRep(aT , A) comprising the dynamic repairs which require the least amount of computations. So similarly with standard repairs, given a dynamic repair A of A with respect to aT , in order to check if A is a minimal dynamic repair we first pinpoint the (unique) number k such that DynRep k (aT , A) = MinDynRep(aT , A) and then check whether A ∈ MinDynRep(aT , A) by the obvious extensions of the decision procedures from standard to dynamic repairs.

  . But since aT = {λ if ¬ρ | ρ ∈ T and λ ∈ pr(ρ)} then static(aT ) = T and η∈aT η = ρ∈T λ∈pr(ρ)λ if ¬ρ which gives: A is a standard repair of A with respect to T then A is relevant to A and the formula A ∧ π n T A is satisfiable for some n ∈ N. This means that A ∧ π n aT A is satisfiable and, by Definition 5.10, A is a dynamic repair of A with respect to aT . The fact that MinDynRep(aT , A) = MinStandRep(T , A) follows similarly.

'

  ∃r.C'. This could in principle be done by either allowing the addition of roles, i.e., local programs of the form +r.ϕ and +r c .ϕ, or the addition/removal of a concept to only one individual through a role, i.e., local programs of the form ∃r.±A and ∃r c .±A. The reason is the following: in the first case (addition of roles), adding to an individual a relation between the individual and any member of the domain that has property C may produce a big change in the resulting interpretation, thus creating possible repairs that are very undesirable. Consider, for instance, the following KB: T = { ∃hasFather.Male} A = {John : Male ∀hasFather.¬Male} Applying to John the update action +hasFather.Male then will result in the ABox A = {hasFather(John, John), John : Male} being a possible repair (and also other repairs with the role assertions hasFather(John, X), for every other possible individual X in the ABox who may have the property Male) which is obviously not what a repair should be. Similarly for the addition of inverse roles. On the other hand, both (1) adding to an individual a relation between the individual and only one (abstract) member of the domain and (2) adding or removing a concept only to one individual through a role cannot be pursued because of technical limitations: it is true that enhancing the logic with these extra local programs would produce more repairs in practice, but the reduction axioms wouldunfortunately fail and the logic would no longer be reducible to its static part.

  {α 1 , α 2 , . . . }• A I = {α 1 } • (α n , α n+1 ) ∈ r I for all n ∈ N Then we have that (∀r.+A if A) * A I = ∆ I and (∀r.+A if A) ≤n A I ⊂ ∆ I for all n ∈ N, i.e.,the program (∀r. + A if A) * cannot be reduced to (∀r. + A if A) ≤n for any n ∈ N.

  3 to incorporate nominals and Propositions 3.1 and 3.2 are still valid. The same goes for removing roles: since one of the distinguishing features of Chapter 5 is the ability to remove roles through the programs -r.ϕ and -r c .ϕ, we can extend Definition 3.4 so that A ∼ 1 A if also A is the outcome of removing a role assertion from A. This implies that A and A are semantically different from one another and once again the remaining definitions and propositions stay intact. We also write A = A [-r(a, b)] when this happens and U A A = {r(a, b) → ⊥} if A = A [-r(a, b)].

  Let us showcase an example of what has been said so far. We return to the initial example of Section 1.1 and the way we represented it in Chapter 5 through the following active TBoxes:aT 1 = {+Male if ¬ (Father Male Parent) , +Parent if ¬ (Father Male Parent) , -OnlyChild if ¬ (OnlyChild ∀hasSibling.⊥)} aT 2 = {-Father if ¬ (Father Male Parent) , -hasSibling. if ¬ (OnlyChild ∀hasSibling.⊥)}Remember also that the initial ABox was the following: A = {John : Male Father ¬Parent, Mary : OnlyChild, hasSibling(Mary, John)} We can see how, taking S A 1 A = {¬Parent → Parent}, {OnlyChild → ¬OnlyChild} and S A 2 A = {Father → ¬Father}, {hasSibling(Mary, John) → ⊥} , we have A S A 1 A = A 1 and A S A 2 A = A 2 where: A 1 = {John : Male Father Parent, Mary : ¬OnlyChild, hasSibling(Mary, John)} A 2 = {John : Male ¬Father ¬Parent, Mary : OnlyChild} Thus A 1 , A 2 ∈ R A 2 and they are minimal repairs with respect to the number of syntactic modifications needed. Furthermore, we saw in Chapter 5 that both of the formulas A ∧ π 2 aT 1 A 1 and A ∧ π 2 aT 2 A 2 are satisfiable and A 1 , A 2 ∈ MinDynRep(aT , A), so they are minimal dynamic repairs as well. Let us note though that dynamic repairs that are minimal with regards to the number of syntactic modifications are not necessarily minimal dynamic repairs and vice versa. Consider, for instance, the following active TBox and ABox: aT = {+Man if ¬ (Person Male Man) , ∀hasFather.+Male if ¬ (Person ∀hasFather.Male) , -hasFather.¬Male if ¬ (Person ∀hasFather.Male)} A = {Anna : Person, Mary : Person, Peter : Person, John : Person ¬Male ¬Man, hasFather(Anna, John), hasFather(Mary, John), hasFather(Peter, John)} For the ABox A 1 = {Anna : Person, Mary : Person, Peter : Person, John : Person ¬Male ¬Man} we have that A ∧ π 1 aT A 1 is satisfiable and thus A 1 ∈ DynRep 1 (aT , A) = MinDynRep(aT , A). Furthermore, A 1 ∈ R A 3 since: A 1 = A {hasFather(Anna, John) → ⊥}, {hasFather(Mary, John) → ⊥}, {hasFather(Peter, John) → ⊥} and it is not minimal with regards to the number of syntactic modifications because there are dynamic repairs of A that are achieved in less syntactic steps, e.g.: A 2 = {Anna : Person, Mary : Person, Peter : Person, John : Person Male Man, hasFather(Anna, John), hasFather(Mary, John), hasFather(Peter, John)}

  Conditional Logic is primarily concerned with the logical and semantic analysis of the rich class of conditional statements, identified with the sentences conforming with the 'if A then B' structure. The topic has roots in antiquity and the medieval times but its contemporary development seems to start with F. Ramsey in the '30s and has blos-

	somed after the late '60s [Arlo-Costa, 2014]. There exist various conditionals of interest
	in Philosophy, Logic, Computer Science and Artificial Intelligence, including counterfac-
	tual conditionals, open conditionals, causal conditionals, deontic conditionals, normality
	conditionals (see

  ∨D 2 , +D 1 which declares that if D 1 ∨D 2 is violated and an employee is not assigned to any department then s/he should be assigned to D 1 . Furthermore, since the database is for permanent employees, if an employee is assigned only to D 1 then this should be rectified by assigning him/her to D 2 as well. This is expressed by the active constraint ¬D 1 ∨ D 2 , +D 2 . Finally, consider that the database loses track of an employee, i.e., a permanent employee is declared as working at neither D 1 nor D 2 . How would the status

	(propositional) scenario. Consider a company with two departments, D 1 and D 2 , where
	temporary employees (e.g. interns) are assigned to D 1 and permanent employees work
	at D 2 (so D 1 has no permanent members and D 2 has no temporary members). Every
	employee must be in a department, i.e., we have the integrity constraint D 1 ∨ D 2 . Further-
	more, consider that every person working on D 2 has previously worked on D 1 , i.e., D 1 is
	like a 'training ground' for becoming a permanent member. Consider now a database for
	permanent members which keeps track of their status. Every employee should be declared Dynamic Logic Account of Active Integrity in the database as starting to work on D 1 and we can express this by the active constraint
	Constraints 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Contents 2.2 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 D 1 of this employee, which is inconsistent w.r.t. the active constraints, be repaired according
	2.3 Repairs and Weak Repairs in DL-PA . . . . . . . . . . . . . . 35 to the available repair procedures? Whereas founded and justified repairs cannot provide
	2.4 Founded and Justified Repairs in DL-PA . . . . . . . . . . . . 37 a solution to this problem (see Section 2.2.2 for more details), a dynamic procedure which
	2.5 A New Definition of Repair in DL-PA . . . . . . . . . . . . . . 44
	2.6 Complexity of Dynamic Repairs . . . . . . . . . . . . . . . . 55
	2.7 History-Based Repairs . . . . . . . . . . . . . . . . . . . . . . 63
	2.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
	2.1 Introduction
	As we have seen in Section 1.2.2, the setting of active integrity constraints is well es-
	tablished and thoroughly explored. Despite this however, there exist cases where even
	founded and justified repairs cannot provide a satisfactory solution to the problem of
	repairing a database under a set of AICs. A more dynamic procedure could provide
	solutions to inconsistencies that arise between a database and a set of active constraints
	that build upon and extend one another. We showcase such an example in the following

  Let V = ∅ and C = {p∨q}. The weak repairs of V achieving C are all those subsets of the set of positive update actions {r ← : r ∈ P} that contain either p ← , or q ← , or both.

	t. V iff p ← ∈ U implies p / ∈ V and
	p ←⊥ ∈ U implies p ∈ V . The definition of a weak repair immediately follows.
	Definition 2.1. Let V be a database and let C be a set of static constraints. A weak repair
	of V achieving C is a consistent set of update actions U ⊆ U such that V U |= C
	and such that U is relevant w.r.t. V .
	The next example illustrates that weak repairs are indeed very weak.
	Example 2.1. As the following result shows, if we consider what is true in all possible weak repairs
	then we obtain what is called a drastic update in the literature on belief revision and
	update. 1

  , {x? ← } ask for a truth value for x a 2 : ¬A+? ∨ A+! ∨ B+? ∨ B+! ∨ ¬x? ∨ x! ∨ x , {x ← , x! ← } toggle x or set it to false a 3 : ¬A+? ∨ A+! ∨ B+? ∨ B+! ∨ ¬x? ∨ x! ∨ ¬x , {x! ← } set x to true a 4 : ¬A+? ∨ A+! ∨ B+? ∨ B+! ∨ ¬x? ∨ ¬x! , {x? ←⊥} end the choice of x a 5 : ¬A+? ∨ A+! ∨ B+? ∨ B+! ∨ x? ∨ ¬x! , ¬A+? ∨ ¬A+! ∨ B+? ∨ B+! ∨ x? ∨ x! ∨ ¬x , {x ←⊥} remove x if it is set to true a 10 : ¬A+? ∨ ¬A+! ∨ B+? ∨ B+! ∨ x? ∨ x! ∨ x , {A+? ←⊥} end the request for A Lemma 2.4. Let A ∈ subf ∃ (G) and V ⊆ subf v (G). Furthermore, consider that the induction hypothesis holds for B, where A = ∃x.B, i.e., at least one of IndHyp(B, V \ {x})

		{B+? ← }	ask for B to be true
	a 6 : ¬A+? ∨ A+! ∨ B+? ∨ ¬B+! ∨ x? ∨ ¬x! ,	{A+! ← }	A is now proved true
	a 7 : ¬A+? ∨ ¬A+! ∨ B+? ∨ ¬B+! ∨ x? ∨ ¬x! ,	{x! ←⊥}	free x
	a 8 : ¬A+? ∨ ¬A+! ∨ B+? ∨ ¬B+! ∨ x? ∨ x! ,	{B+! ←⊥}	remove the result for B
	a 9 :

+

or IndHyp(B, V ∪ {x}) + holds. Then:

V |= A iff there is a dynamic weak repair of V ∪ {A+?} by {a 1 , . . . , a 10 } Proof. Consider A = ∃x.B, the database V and the set of active constraints η = {a 1 , . . . , a 10

  Having complex concept descriptions inside TBox axioms means that Married ≡ Person ∃hasSpouse.Person Divorced ≡ Person ∃hadSpouse.Person ¬∃hasSpouse.Person Bachelor ≡ Person ¬∃hadSpouse.Person ¬∃hasSpouse.Person Widowed ≡ Person ∃hadSpouse.Deceased ¬∃hasSpouse.Person

	Bachelor Married ⊥
	Divorced Widowed ⊥
	Person Married Divorced Bachelor Widowed
	Figure 3.1: Example of a TBox

'simple' update actions like additions or deletions of atomic concepts is not enough, since

  Definition 4.7. 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 )

INTRODUCTION

A DYNAMIC LOGIC ACCOUNT OF ACTIVE INTEGRITY CONSTRAINTS

It is actually also a drastic revision because V is a complete database and update and revision coincide in that case[START_REF] Peppas | Revision vs. update: Taking a closer look[END_REF].

We have reformulated the original definition so that it applies to our more general definition of active constraints. Both are equivalent as far as standard active constraints are concerned.

The original definition of justified weak repairs is slightly different than the one given here. However it is shown that the two are equivalent in[Caroprese and Truszczynski, 2011, Theorem 1].

The difference with[Herzig, 2014] is that our programs memorise that a variable has been flipped instead of storing its previous value.

Note that by definition of toggle(p), p ∈ D(V , V ) is equivalent to p ± ∈ D(V , V ) thus the inclusion D(V , V ) ⊂ D(V , V) is not affected by the variables in P C ± .

This may happen if, for instance, A = ∀x.A and the truth value for A needs to be checked twice while checking if A is true.2. A DYNAMIC LOGIC ACCOUNT OF ACTIVE INTEGRITY CONSTRAINTS

A literal in the DL setting is defined similarly to the propositional, i.e., either an atomic concept or the negation thereof.

Whereas the latter seems like a better candidate for a repair (taking into account the open-world nature of DLs we discussed in Section

3.2) we do not give a preference to any of them as long as the inconsistencies are eliminated. Regarding minimality of change, this will be defined syntactically to be the least amount of syntactic changes made in the ABox, once again providing no preference between the two.

A SEMANTIC APPROACH TO REPAIRING ABOXES: THE LOGIC dynALCO

the active TBox aT = { ∃hasFather.Female ⊥, ∅ }. Remember that we talked about this limitation at the end of Chapter 3. 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. Nevertheless, we pursue this direction through a star-free approach in the next chapter.Summing up, we have taken our first semantic approach to repairing ABoxes with regard to active TBoxes, the latter being an extension of regular TBoxes with update actions in a similar fashion to Chapter 3. To that end we have exploited a dynamic logic framework on which various repairing procedures are introduced and discussed, based on their propositional counterparts of Chapter 2. In the following we investigate a more elaborate logic that builds upon the results achieved in this chapter.

Acknowledgements

A semantic approach seems to behave better in general and provide solutions to problems that the syntactic one is unable to handle. This doesn't mean though that the syntactic investigations of this chapter are to no avail: the way to reconstruct new ABoxes through syntactic modifications of an initial ABox will prove very useful in combination with the subsequent semantic approaches, since the effectiveness of the latter will be mainly in evaluating whether an ABox is repaired but not in constructing it. We will thus revisit this chapter's ideas in the concluding Chapter 6 together with the semantic investigations to come.

Looking ahead, the most crucial thing will be to make the landscape of active TBoxes and the associated repairs more clear and intuitive. The logics that we will define are inspired by the way DL-PA was utilised to provide new kinds of repairs in the database literature. In this chapter we provided a first (small) step into this direction, carefully discussing the difficulties and differences of the DL setting as well as important limitations that we have to tackle. In Chapter 4 we give an emphasis on overcoming limitation (1), whereas Chapter 5 goes further and mainly focuses on limitation (2).

Introduction

In this chapter we take a semantic approach and investigate how the various definitions of repairs from the database literature behave in the DL setting. As with Chapter 2, 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. As we have seen before, this contrasts with active integrity constraint-based repairs where the update is applied in one go and later checked if it adheres to the preferences using certain CHAPTER 5

Repairing ABoxes Semantically: the more Elaborate dynALCIO

Introduction

The semantic approach we take in this chapter is based again on Dynamic Logic, but this time we show how repaired ABoxes (which constitute the repairs from now on) can be assessed by complex programs. Since we want to be as general as possible, we once again consider that TBoxes are composed of concept inclusion axioms but now we work with the language of ALCI (without the unique name assumption). As we noted in the introduction of Chapter 4, a first difficulty is that after updating an ALCI ABox the resulting repair may not be expressible in ALCI anymore (the same simple example