Most approaches for repairing description logic (DL) ontologies aim at changing the axioms as little as possible while solving inconsistencies, incoherences and other types of undesired behaviours. As in Belief Change, these issues are often speci ed using logical formulae. Instead, in the new setting for updating DL ontologies that we propose here, the input for the change is given by a model which we want to add or remove. The main goal is to minimise the loss of information, without concerning with the syntactic structure. This new setting is motivated by scenarios where an ontology is built automatically and needs to be re ned or updated. In such situations, the syntactical form is often irrelevant and the incoming information is not necessarily given as a formula. We de ne general operations and conditions on which they are applicable, and instantiate our approach to the case of ALC-formulae.
Formal speci cations often have to be updated either due to modelling errors or
because they have become obsolete. When these speci cations are description
logic (DL) ontologies, it is possible to use one of the many approaches to x
missing or unwanted behaviours. Usually these methods involve the removal or
replacement of formulae responsible by the undesired aspect [
The problem of changing logical representations of knowledge upon the
arrival of new information is the subject matter of Belief Change [
Example 1. Suppose that a system, which serves a university, uses an internal logical representation of the domain with a open world behaviour and unique names. Let B be its current represention:
B = fP rof essors : fM aryg; Courses : fDL; AIg;
fteaches : f(M ary; AI); (M ary; DL)gg :
Assume that a user nds mistakes in the course schedule and this is caused by the wrong information that Mary teaches the DL course. The user may lack knowledge to de ne the issue formally. An alternative would be to provide the user with an interface where one can specify, for instance, that the following model should be accepted M = fP rof essors = fM aryg; Courses = fDL; AIg; teaches = f(M ary; AI)gg; (in this model Mary does not teach the DL course). Given this input, the system should repair itself (semi-)automatically.
We propose a new setting for Belief Change, in particular, contraction and expansion functions which take models as input. We analyse the case of ALCformula using quasimodels as a mean to de ne belief change operations. This logic satis es properties which facilitate the design of these operations and it is close to ALC, which is a well-studied DL. Additionally, we identify the postulates which determine these functions and prove that they characterise the mathematical constructions via representation theorems. The remaining of this work is organised as follows: in Section 2 we introduce the concepts from Belief Change which our approach builds upon and detail the paradigm we propose here. Section 3 presents ALC-formula, the belief operations that take models as input and their respective representation theorems. In Section 4, we highlight studies which share similarities with our proposal and we conclude in Section 5. Missing proofs can be found in the long version of this paper [24]. 2 2.1
Belief Change [
base, as long as ' is consistent.
When modifying its body of knowledge an agent should rationally modify its
beliefs conserving most of its original beliefs. This principle of minimal change
is captured in Belief Change via sets of rationality postulates. Each of the three
operations (expansion, contraction and revision) presents its own set of
rationality postulates which characterize precisely di erent classes of belief change
constructions. The AGM paradigm was initially proposed for classical logics that
satisfy speci c requirements, dubbed AGM assumptions, among them
Tarskianicity, compactness and deduction. See [
In what follows, we de ne kernel contraction [
De nition 2. Given a set of formulae B of language L, a function f is an incision function for B i for all ' 2 L: (i) f (MinImps(B; ')) S MinImps(B; ') and (ii) f (MinImps(B; ')) \ X 6= ;, for all X 2 MinImps(B; ').
Kernel contraction operators are built upon incision functions. An incision
function is responsible to pick at least one formula from each MinImp. Intuitively,
one can see an incision function as a Hitting Set on all the MinImps, as in [
that relates each set of formulae A to all formulae that are entailed from A.
Kernel contraction operations are characterised precisely by a set of rationality
postulates, as shown in the following representation theorem:
Theorem 4 ([
B such that 2 Cn(B0), then 2.2
The Belief Change setting discussed in this section represents an epistemic state
by means of a nite base. While this essentially di er from the traditional
approach [
In this work, unlike the standard representation methods in Belief Change, we consider that an incoming piece of information is represented as a nite model. Belief Change operations de ned in this format will be called model change operations. Recall that a model M is simply a structure used to give semantics to an underlying logic language. The set of all possible models is given by M.
language L gives a set of models Mod(B) := fM 2 M j 8' 2 B : M j= 'g. Let
Mod(B) = M. Additionally, if for all ' 2 L it holds that M j= ' i M 0 j= ' then we write M L M 0. We also de ne [M ]L := fM 0 2 M j M 0 L M g.
When compared to traditional methods in Belief Change and Ontology
Repair [
The rst model change operation we introduce is model contraction, which eliminates one of the models of the current base (which in Section 3 is instantiated as an ontology). Model contraction is akin to a belief expansion, where a formula is added to the belief set or base, reducing the set of accepted models. The counterpart operation, model expansion, changes the base to include a new model. This relates to belief contraction, in which a formula is removed, and thus more models are seen as plausible.
We rewrite the rationality postulates that characterize kernel contraction [
De nition 5 (Model Contraction). Let L be a language. A function con :
for every B 2 P n(L) and M 2 M it satis es the following postulates: (success) M 62 Mod(con(B; M )) = ;, (inclusion) Mod(con(B; M )) Mod(B), (retainment) if M 0 2 Mod(B) n Mod(con(B; M )) then M 0 L M , (extensionality) con(B; M ) = con(B; M 0), if M L M 0.
We might also need to add a model to the set of models of the current base. This addition relates to classical contractions in Belief Change, which reduces the belief base.
De nition 6 (Model Expansion). Let L be a language. A function ex :
B 2 P n(L) and M 2 M it satis es the postulates: (success) M 2 Mod(ex(B; M )); (persistence) Mod(B) Mod(ex(B; M )); (vacuity) Mod(ex(B; M )) = Mod(B); if M 2 Mod(B), (extensionality) ex(B; M ) = ex(B; M 0), if M L M 0.
De nition 7. Let L be a language and Cn a Tarskian consequence operator de ned over L. Also let M be a xed set of models. We say that a triple = (L; Cn; M) is an ideal logical system if the following holds.
{ For every B { For each M
L and ' 2 L, B j= ' (i.e. ' 2 Cn(B)) i Mod(B) Mod(').
M there is a nite set of formulae B such that Mod(B) = M.
If = (L; Cn; M) is an ideal logical system, we can de ne a function FR : 2M 7! P n(L) and such that Mod(FR(M)) = M. Then, we can de ne model contraction as con(B; M ) = FR(Mod(B) n [M ]L) and expansion as ex(B; M ) = FR(Mod(B) [ [M ]L). The rst condition in De nition 7 implies that there is a connection between the models satis ed and the logical consequences of the base obtained and the second ensures that the result always exists. An example that ts these requirements is to consider classical propositional logic with a nite signature , together with its usual consequence operator and models. In this situation, we can de ne FRprop as follows:
0 FRprop(M) = _
@ M2M a2 jMj=a ^ a ^
^ a2 jMj=:a
1 :aA :
Next, we show that the construction proposed with FR has the properties stated in De nitions 5 and 6.
Theorem 8. Let (L; Cn; M) be an ideal logical system as in De nition 7. Then iCon(B; M ) := FR Mod(B) n [M ]L satis es the postulates in De nition 5. Proof. De nition 7 ensures that the result exists and that M j= ', for all ' 2 , giving us success. By construction we do gain models, thus we have inclusion. If M L M 0, then [M ]L = [M 0]L, thus extensionality is satis ed.
satis es retainment.
Theorem 9. Let (L; Cn; M) be an ideal logical system as in De nition 7. Then iExp(B; M ) := FR Mod(B) [ [M ]L satis es the postulates in De nition 6. Proof. De nition 7 ensures that the result exists and that M j= ', for all ' 2 , giving us success. Due to the rst condition in De nition 7 we gain vacuity: if M 2 Mod(B), then there will be no changes in the accepted models. By construction we do not lose models, thus we have persistance. Extensionality also holds because whenever M L M 0 we have then [M ]L = [M 0]L.
A revision operation incorporates new formulae, and removes potential conicts in behalf of consistency. In our setting, incorporating information coincides with model contraction which could lead to an inconsistent belief state. In this case, model revision could be interpreted as a conditional model contraction: in some cases the removal might be rejected to preserve consistency. We leave the study on revision as a future work. 3
The case of ALC-formula The logic ALC-formula corresponds to the DL ALC enriched with boolean operators over ALC axioms. As discussed in Section 2.2, in nite representable logics, such as the classical propositional logics, we can easily add and remove models while keeping the representation nite. For ALC-formula, however, it is not possible to uniquely add or remove a new model M since, for instance, the language does not distinguish quantities (e.g., a model M and another model that has two duplicates of M ).
Even if quantities are disregarded and our input is a class of models indistinguishable by ALC-formulae, there are sets of formulae in this language that are not nitely representable. As for instance in the following in nite set: f9Cr1:>v :9=rn9:r>:Cj. nAs2a Nw>o0rkga,rwouhnedre fo9rrnt+h1e:>ALisC-afosrhmourltahacnadse,fowre9prr:(o9prons:e>a) naenwd strategy based on the translation of ALC-formulae into DNF. Let NC, NR and NI be countably in nite and pairwise disjoint sets of concept names, role names, and individual names, respectively. ALC concepts are built according to the rule: C ::= A j :C j (C u C) j 9r:C, where A 2 NC and r 2 NR. ALC-formulae are de ned as expressions of the form ::= j :( ) j ( ^ ) ::= C(a) j r(a; b) j (C = >); where C is an ALC concept, a; b 2 NI, and r 2 NR3. Denote by ind(') the set of all individual names occurring in an ALC-formula '. 3 We may omit parentheses if there is no risk of confusion. The usual concept inclusions C v D can be expressed with > v :C t D and :C t D v >, which is (:C t D = >).
standard [8, page 70]. In what follows, we reproduce the essential de nitions and results for this work. Let ' be an ALC-formula. Let f(') and c(') be the set of all subformulae and subconcepts of ' closed under single negation, respectively. De nition 10. A concept type for ' is a subset c c(') such that: 1. D 2 c i :D 62 c, for all D 2 c('); 2. D u E 2 c i fD; Eg c, for all D u E 2 c(').
De nition 11. A formula type for ' is a subset f f(') such that: 1. 2.
2 f i : 62 f , for all 2 f('); ^ 2 f i f ; g f , for all ^
2 f(').
We may omit `for '' if this is clear from the context. A model candidate for ' is a triple (T; o; f ) such that T is a set of concept types, o is a function from ind(') to T , f a formula type, and (T; o; f ) satis es the conditions: ' 2 f ; C(a) 2 f implies C 2 o(a); r(a; b) 2 f implies f:C j :9r:C 2 o(a)g o(b). De nition 12 (Quasimodel). A model candidate (T; o; f ) for ' is a quasimodel for ' if the following holds { for every concept type c 2 T and every 9r:D 2 c, there is c0 2 T such that fDg [ f:E j :9r:E 2 cg c0; { for every concept type c 2 T and every concept C, if :C 2 c then this implies (C = >) 62 f ; { for every concept C, if :(C = >) 2 f then there is c 2 T such that C 62 c; { T is not empty.
Theorem 13 motivates the decision of using quasimodels to implement our operations for nite bases described in ALC-formulae.
Theorem 13 (Theorem 2.27 [
ALC-formulae in Disjunctive Normal Form Next, we propose a translation method which converts an ALC-formula into a disjunction of conjunctions of (possibly negated) atomic formulae. Let S(') be the set of all quasimodels for '. We We de ne 'y as _ ( ^ ^
^ : ): (T;o;f)2S(') 2f : 2f where is of the form (C = >); C(a); r(a; b).
Theorem 14 con rms the equivalence between a formula and its translation into DNF. As downside, the translation can be potentially exponentially larger than the original formula.
Theorem 14. For every ALC-formula ', we have that ' 'y.
In the next subsections, we present nite base model change operations for
knowledge as a single formula because every nite belief base of ALC-formulae can be represented by the conjunction of its elements. We use our translation to add models in a \minimal" way by adding disjuncts, while removing a model amounts to removing disjuncts. We also need to obtain a model candidate relative to our translated formula, as show in De nition 15.
De nition 15 ([
discussed previously and a correspondence between models and quasimodels.
We use the following operator, denoted , to de ne model contraction in
('; M ) = ftypes(') n ff g; where qm('; M ) = (T; o; f ) and ftypes(') is the set of all formula types in all quasimodels for ', that is: ftypes(') = ff j (T; o; f ) 2 S(')g: Let lit(f ) := f` 2 f j ` is a literal g be the set of all literals in a formula type f . De nition 16. A nite base model contraction function is a function con : L M 7! L such that con('; M )= 8 W >< f2 (';M) > : ? ' V lit(f ); if M j= ' and if M j= ' and otherwise: ('; M ) 6= ; ('; M ) = ;
but our operations based on quasimodels cannot distinguish them. Given ALCformulae '; , we say that is in the language of the literals of ', written
partition the models according to this restricted language. We write M ' M 0 instead of M Llit(') M 0, and [M ]' instead of [M ]Llit(') for conciseness. Theorem 17. Let M be a model and ' an ALC-formula. A nite base model function con ('; M ) is equivalent to con('; M ) i con satis es: (success) M 6j= con ('; M ), (inclusion) Mod(con ('; M )) Mod('), (atomic retainment): For all M0 M, if Mod(con (B; M ))
[M ]' then M0 is not nitely representable in ALC-formula. (atomic extensionality) if M 0 ' M then
Mod(con ('; M )) = Mod(con ('; M 0)):
The postulate of success guarantees that M will be indeed relinquished, while inclusion imposes that no model will be gained during a contraction operation. Recall that in order to guarantee nite representability, it might be necessary to remove M jointly with other models. The postulate atomic retainment captures a notion of minimal change, dictating which models are allowed to be removed together with M .
On the other hand, atomic extensionality imposes that if two models M and M 0 satisfy the same formulae within the literals of the current knowledge base ', then they should present the same result.
A simpler way of implementing model contraction, also using the notion of a quasimodel, De nition 18. Let ' be an ALC-formula and M a model. Also, let (T; o; f ) = qm('; M ). The function cons('; M ) is de ned follows: cons('; M ) = ' ^ :(V lit(f )) if M j= '
' otherwise.
Example 19 illustrates how cons works.
Example 19. Consider the following ALC-formula and interpretation M : ' :=P (M ary) ^ C(DL) ^ C(AI) ^ ((teaches(M ary; DL) ^
:teaches(M ary; AI)) _ (:teaches(M ary; DL) ^ teaches(M ary; AI))) and M = ( I ; I ), where I = fm; d; ag, CI = fd; ag, P I = fmg, teachesI = f(m; d)g, M aryI = m, AII = a, and DLI = d. Assume we want to remove M from Mod('). Let qm('; M ) = (T; o; f ). Thus,
lit(f ) = f:teaches(m; a); teaches(m; d); C(d); C(a); P (m)g cons('; M ) = ' ^ : ^ lit(f )
= ' ^ : (:teaches(m; a) ^ teaches(m; d) ^ C(d) ^ C(a) ^ P (m)) : Both model contraction operations con and cons are equivalent. Theorem 20. For every ALC-formula ' and model M , con('; M ) cons('; M ).
we assume that a knowledge base is represented as a single ALC-formula '. Expansion consists in adding an input model M to the current knowledge base ' with the requirement that the new epistemic state can be represented also as a nite formula.
De nition 21. Given a quasimodel (T; o; f ), we write V(T; o; f ) as a short-cut for V lit(f ). A nite base model expansion is a function ex : L M ! L s.t.: ex('; M ) =
' if M j= ' ' _ V qm(:'; M ) otherwise:
Example 22 illustrates how ex works.
Example 22. Consider the interpretation M from Example 19 and ' := P (M ary) ^ C(DL) ^ C(AI) ^ teaches(M ary; AI) ^ :teaches(M ary; DL): Assume we want to add M to Mod(') and qm(:'; M ) = (T; o; f ). Thus, lit(f ) = f:teaches(m; a); teaches(m; d); C(d); C(a); P (m)g ex('; M ) = ' _ ^ lit(f )
= ' _ (:teaches(m; a) ^ teaches(m; d) ^ C(d) ^ C(a) ^ P (m)) :
The operation `ex' maps a current knowledge base represented as a single formula ' and maps it to a new knowledge base that is satis ed by the input model M . The intuition is that `ex' modi es the current knowledge base only if M does not satisfy '. This modi cation is carried out by making a disjunct of ' with a formula that is satis ed by M . This guarantees that M is present in the new epistemic state and that models of ' are not discarded. The trick is to nd such an appropriate formula which is obtained by taking the conjunction of all the literals within the quasimodel qm(:'; M ). Here, the quasimodel needs to be centred on :' because M 6j= ', and therefore it is not possible to construct a quasimodel based on M centred on '. As discussed in the prelude of this section, this strategy not only adds M to the new knowledge base but also the whole equivalence class modulo the literals of '.
Lemma 23. For every ALC-formula ' and model M :
Mod(ex('; M )) = Mod(') [ [M ]':
Actually, any operation that adds precisely the equivalence class of M modulo the literals is equivalent to `ex'. In the following, we write ex ('; M ) to refer to an arbitrary nite base expansion function of the form ex : L M 7! L. Theorem 24. For every ex , if Mod(ex ('; M )) = Mod(') [ [M ]' then (i) ex ('; M ) (ii) ex ('; M ) ', if M j= '; and ' _ V qm(:'; M ), if M 6j= '.
Our next step is to investigate the rationality of `ex '. As expected adding the whole equivalence class of M with respect to Llit(') does not come freely, and some rationality postulates are captured, while others are lost: Theorem 25. Let M be a model and ' an ALC-formula. A function ex ('; M ) is equivalent to ex('; M ) i ex satis es: nite base model (success) M 2 Mod(ex ('; M )). (persistence): Mod(') Mod(ex ('; M )). (atomic temperance): For all M0 M, if Mod(')[[M ]'
fM g then M0 is not nitely representable in ALC-formula. (atomic extensionality) if M 0 ' M then
M0
Mod(ex ('; M )) = Mod(ex ('; M 0)):
The postulates success and persistence come from requiring that M will be absorbed, and that models will not be lost during an expansion. The atomic extensionality postulate states that if two models satisfy exactly the same literals within ', then they should present the same results. Atomic temperance captures a principle of minimality and guarantees that when adding M , the loss of information should be minimised. Precisely, the only formulae allowed to be given up are those that are incompatible with M modulo the literals of '. Lemma 23 and Theorem 25 prove that the `ex' operation is characterized by the postulates: success, persistence, atomic temperance and atomic extensionality. Mod(ex ('; M ))[ 4
In the foundational paradigm of Belief Change, the AGM theory, bases have been
used in the literature with two main purposes: as a nite representation of the
knowledge of an agent [
The syntactic connectivity in a knowledge base has a strong consequence of
how an agent should modify its knowledge [
Other remarkable works in Belief Change in which the body of knowledge is
represented in a nite way include the formalisation of revision due to Katsuno
and Mendelzon [17] and the base-generated operations by Hansson [
In this work, we have introduced a new kind of belief change operation: belief change via models. In our approach, an agent is confronted with a new piece of information in the format of a nite model, and it is compelled to modify its current epistemic state, represented as a single nite formula, either incorporating the new model, called model expansion; or removing it, called model contraction. The price for such nite representation is that the single input model cannot be removed or added alone, and some other models must be added or removed as well. As future work, we will investigate model change operations in other DLs, still taking into account nite representability. We will also explore the e ects of relaxing some constraints on Belief Base operations, allowing us to rewrite axioms with di erent levels of preservation in the spirit of Pseudo-Contractions, Gentle Repairs, and Axiom Weakening.
Part of this work has been done in the context of CEDAS (Center for Data Science, University of Bergen, Norway). The rst author is supported by the German Research Association (DFG), project number 424710479. Ozaki is supported by the Norwegian Research Council, grant number 316022. [29] Boontawee Suntisrivaraporn. Polynomial time reasoning support for design and maintenance of large-scale biomedical ontologies. PhD thesis, Dresden University of Technology, Germany, 2009. [30] Nicolas Troquard, Roberto Confalonieri, Pietro Galliani, Rafael Pen~aloza, Daniele Porello, and Oliver Kutz. Repairing Ontologies via Axiom Weakening. In Proceedings of the 22nd AAAI Conference on Arti cial Intelligence, AAAI 2018, pages 1981{1988. AAAI Press, 2018.