{'fraction_non_alphanumeric': 0.04078815261044177, 'fraction_numerical': 0.006902610441767068, 'mean_word_length': 4.3961625282167045, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Revising Ontologies via Models: The ALC-formula Case

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 specified 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 refined or updated. In such situations, the syntactical form is often irrelevant and the incoming information is not necessarily given as a formula. We define general operations and conditions on which they are applicable, and instantiate our approach to the case of ALC-formulae.


Introduction
Formal specifications often have to be updated either due to modelling errors or because they have become obsolete. When these specifications are description logic (DL) ontologies, it is possible to use one of the many approaches to fix missing or unwanted behaviours. Usually these methods involve the removal or replacement of formulae responsible by the undesired aspect [2,16,20,28,29].
The problem of changing logical representations of knowledge upon the arrival of new information is the subject matter of Belief Change [13]. The theory developed in this field provides constructions suitable for various formalisms and applications [13,23,24,27]. In most approaches for Belief Change and for repairing ontologies, it is assumed that a set of formulae represents the entailments to be added or removed. However, in some situations, it might be easier to obtain this information as a model instead. This idea relates with Model Checking [3] whose main problem is to determine whether a model satisfies a set of constraints; and with the paradigm of Learning from Interpretations [4], where a formula needs to be created or changed so as to have certain interpretations as part of its models and remove others from its set of models. Example 1 illustrates the intuition behind using models as input. Assume that a user finds 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 define 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 = {P rof essors = {M ary}, Courses = {DL, AI}, teaches = {(M ary, AI)}}, (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 define belief change operations. This logic satisfies 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.

The Classical Setting
Belief Change [1,13] studies the problem of how an agent should modify its knowledge in light of new information. In the original paradigm of Belief Change, the AGM theory, an agent's body of knowledge is represented as a set of formulae closed under logical consequence, called a belief set, and the new information is represented as a single formula. Belief sets, however, are not the only way for representing an agent's body of knowledge, and another way of representing an agent's knowledge is via belief bases: arbitrary sets of formulae, not necessarily closed under logical consequence [11]. In the AGM paradigm, an agent may modify its current belief base B in response to a new piece of information ϕ through three kinds of operations: Expansion: ex(B, ϕ), simply add ϕ to B; Contraction: con(B, ϕ), reduce B so that it does not imply ϕ; Revision: rev(B, ϕ), incorporate ϕ and keep consistency of the resulting belief 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 different classes of belief change constructions. The AGM paradigm was initially proposed for classical logics that satisfy specific requirements, dubbed AGM assumptions, among them Tarskianicity, compactness and deduction. See [6,24] for a complete list of the AGM assumptions and a discussion on the topic. Recently, efforts have been applied to extend Belief Change to logics that do not satisfy such assumptions. For instance, logics that are not closed under classical negation of formulae (such as is the case for most DLs) [24,26], and temporal logics and logics without compactness [21][22][23].
In what follows, we define kernel contraction [13], one of the most studied constructions in Belief Change and which is closely related to the most common ways to repair ontologies. Kernel operations rely on calculating the minimal implying sets (MinImps), also known as justifications [15] or kernels [13]. A MinImp is a minimal subset that does entail a formula ϕ. The set of all MinImps of a belief base B w.r.t. a formula ϕ is denoted by MinImps(B, ϕ). A kernel contraction removes from each MinImp at least one formula using an incision function.
Kernel contraction operators are built upon incision functions. The application of an incision function to a set of MinImps is a hitting set [2,16].
Definition 3. Let L be a language and f an incision function. The kernel contraction on B ⊆ L determined by f is the operation con f : 2 L × L → 2 L defined as: con f (B, ϕ) = B \ f (MinImps(B, ϕ)).
Kernel contraction operations are characterised precisely by a set of rationality postulates, as shown in the following representation theorem: Theorem 4 ([14]). Let Cn be a consequence operator satisfying monotonicity and compactness defined for a language L. Then con : 2 L × L → 2 L is an operation of kernel contraction on B ⊆ L iff for all sentences ϕ ∈ L: con(B, ϕ) = con(B, ψ).

Changing Finite Bases by Models
The Belief Change setting discussed in this section represents an epistemic state by means of a finite base. While this essentially differ from the traditional approach [1,11], it aligns with the KM paradigm established by Katsuno and Mendelzon [17]. In Section 4 we discuss other studies in Belief Change which also take finite representability into account. In this work, unlike the standard representation methods in Belief Change, we consider that an incoming piece of information is represented as a finite model. Belief Change operations defined 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. Moreover, we assume a semantic system that, for each set of formulae B of the language L gives a set of models Mod(B) := {M ∈ M | ∀ϕ ∈ B : M |= ϕ}. Let P fin (L) denote the set of all finite bases in L. We also say that a set of models M is finitely representable in L if there is a finite base B ∈ P fin (L) such that When compared to traditional methods in Belief Change and Ontology Repair [2,13,16], where the incoming information comes as a single formula, our approach receives instead a single model as input. Although, the initial body of knowledge is represented as a finite base, the operations we define do not aim to preserve its syntactic structure.
The first 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 [14], considering an incoming piece of information represented as a model instead of a single formula.
Definition 5 (Model Contraction). Let L be a language. A function con : P fin (L) × M → P fin (L) is a finitely representable model contraction function iff for every B ∈ P fin (L) and M ∈ M it satisfies the following postulates: 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.
Definition 6 (Model Expansion). Let L be a language. A function ex : P fin (L) × M → P fin (L) is a finitely representable model expansion iff for every B ∈ P fin (L) and M ∈ M it satisfies the postulates: Definition 7. Let L be a language and Cn a Tarskian consequence operator defined over L. Also let M be a fixed set of models. We say that a triple Λ = (L, Cn, M) is an ideal logical system if the following holds. . The first condition in Definition 7 implies that there is a connection between the models satisfied and the logical consequences of the base obtained and the second ensures that the result always exists. An example that fits these requirements is to consider classical propositional logic with a finite signature Σ, together with its usual consequence operator and models. In this situation, we can define FR prop as follows: Next, we show that the construction proposed with FR has the properties stated in Definitions 5 and 6. Proof. Definition 7 ensures that the result exists and that M |= ϕ, for all ϕ ∈ Λ, giving us success. By construction we do gain models, thus we have  Proof. Definition 7 ensures that the result exists and that M |= ϕ, for all ϕ ∈ Λ, giving us success. Due to the first condition in Definition 7 we gain vacuity: if M ∈ 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 A revision operation incorporates new formulae, and removes potential conflicts 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.

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 finite representable logics, such as the classical propositional logics, we can easily add and remove models while keeping the representation finite. 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 finitely representable. As for instance in the following infinite set: {C ⊑ ∃r n .⊤ | n ∈ N >0 }, where ∃r n+1 .⊤ is a shorthand for ∃r.(∃r n .⊤) and ∃r 1 .⊤ := ∃r.C. As a workaround for the ALC-formula case, we propose a new strategy based on the translation of ALC-formulae into DNF.

ALC-formulae and Quasimodels
Let N C , N R and N I be countably infinite and pairwise disjoint sets of concept names, role names, and individual names, respectively. ALC concepts are built according to the rule: C ::= A | ¬C | (C ⊓ C) | ∃r.C, where A ∈ N C and r ∈ N R . ALC-formulae are defined as expressions φ of the form where C is an ALC concept, a, b ∈ N I , and r ∈ N R 3 . Denote by ind(ϕ) the set of all individual names occurring in an ALC-formula ϕ.
The semantics of ALC-formulae and the definitions related to quasimodels are standard [8, page 70]. In what follows, we reproduce the essential definitions 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.
Definition 11. A formula type for ϕ is a subset f ⊆ f(ϕ) such that: Theorem 13 motivates the decision of using quasimodels to implement our operations for finite bases described in ALC-formulae.

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 define ϕ † as where α is of the form (C = ⊤), C(a), r (a, b).
Theorem 14 confirms the equivalence between a formula and its translation into DNF. As downside, the translation can be potentially exponentially larger than the original formula.
In the next subsections, we present finite base model change operations for ALC-formulae, i.e., functions from L × M → L. We can represent the body of knowledge as a single formula because every finite 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 Definition 15.

Model Contraction for ALC-formulae
We define model contraction for ALC-formulae using the notion of quasimodels discussed previously and a correspondence between models and quasimodels.
We use the following operator, denoted µ, to define model contraction in Definition 16. Let ϕ be an ALC-formula and let M be a model. Then, and ftypes(ϕ) is the set of all formula types in all quasimodels for ϕ, that is: Let lit(f ) := {ℓ ∈ f | ℓ is a literal } be the set of all literals in a formula type f . As we see later in this section, there are models M, M ′ such that M ≡ L M ′ but our operations based on quasimodels cannot distinguish them. Given ALCformulae ϕ, ψ, we say that ψ is in the language of the literals of ϕ, written ψ ∈ L lit (ϕ), if ψ is a boolean combination of the atoms in ϕ. Our operations partition the models according to this restricted language. We write Theorem 17. Let M be a model and ϕ an ALC-formula. A finite base model function con * (ϕ, M ) is equivalent to con(ϕ, M ) iff con * satisfies: 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 finite 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 ′ 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, Definition 18. Let ϕ be an ALC-formula and M a model. Also, let (T, o, f ) = qm(ϕ, M ). The function con s (ϕ, M ) is defined follows: Example 19 illustrates how con s works. Both model contraction operations con and con s are equivalent.

Model Expansion in ALC-formulae
In this section, we investigate model expansion for ALC-formulae. Recall that 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 finite formula. The operation 'ex' maps a current knowledge base represented as a single formula ϕ and maps it to a new knowledge base that is satisfied by the input model M . The intuition is that 'ex' modifies the current knowledge base only if M does not satisfy ϕ. This modification is carried out by making a disjunct of ϕ with a formula ψ that is satisfied by M . This guarantees that M is present in the new epistemic state and that models of ϕ are not discarded. The trick is to find 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 |= ϕ, 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 ϕ. 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 finite base expansion function of the form ex * : L × M → L.
Our next step is to investigate the rationality of 'ex * '. As expected adding the whole equivalence class of M with respect to L lit (ϕ) does not come freely, and some rationality postulates are captured, while others are lost: 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.

Related Work
In the foundational paradigm of Belief Change, the AGM theory, bases have been used in the literature with two main purposes: as a finite representation of the knowledge of an agent [5,19], and as a way of distinguishing agents knowledge explicitly [11]. Even though the AGM theory cannot be directly applied to DLs because most of these logics do not satisfy the prerequisites known as the AGMassumptions [7], it has been studied and adapted to DLs [6,25].
The syntactic connectivity in a knowledge base has a strong consequence of how an agent should modify its knowledge [13]. This sensitivity to syntax is also present in Ontology Repair and Evolution. Classical approaches preserve the syntactic form of the ontology as much as possible [16,28]. However, these approaches may lead to drastic loss of information, as noticed by Hansson [10]. This problem has been studied in Belief Change for pseudo-contraction [27]. In the same direction, Troquard et al. [29] proposed the repair of DL ontologies by weakening axioms using refinement operators. Building on this study, Baader et al. [2] devised the theory of gentle repairs, which also aims at keeping most of the information within the ontology upon repair. In fact, gentle repairs are closely related to pseudo-contractions [18].
Other remarkable works in Belief Change in which the body of knowledge is represented in a finite way include the formalisation of revision due to Katsuno and Mendelzon [17] and the base-generated operations by Hansson [12]. In the former, Katsuno and Mendelzon [17] formalise traditional belief revision operations using a single formula to represent the whole belief set. This is possible because they only consider finitary propositional languages. Hansson provides a characterisation of belief change operations over finite bases but restricted for logics which satisfy all the AGM-assumptions (such as propositional classical logic). Guerra and Wassermann [9] develop operations for rational change where an agent's knowledge or behaviour is given by a Kripke model. They also provide two characterisations with AGM-style postulates.
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 finite model, and it is compelled to modify its current epistemic state, represented as a single finite formula, either incorporating the new model, called model expansion; or removing it, called model contraction.
The price for such finite 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 finite representability. We will also explore the effects of relaxing some constraints on Belief Base operations, allowing us to rewrite axioms with different levels of preservation in the spirit of Pseudo-Contractions, Gentle Repairs, and Axiom Weakening.

A Proofs for Section 3
We have already given the syntax of ALC-formulae in the main text and we provide the semantics here for the convenience of the reader. The semantics is given by interpretations. As usual, an interpretation I is a pair (∆ I , · I ) where ∆ I is a countable non-empty set, called the domain of invidivuals, and · I is a function mapping each concept name A ∈ N C to a subset A I of ∆ I and each role name r ∈ N R to a subset r I of ∆ I × ∆ I . The interpretation of concepts in I is The interpretation of formulae is as expected I |= ¬(ϕ) iff not I |= ¬(ϕ) I |= (ϕ ∧ ψ) iff I |= ϕ and I |= ψ Formally, we inductively define the sets f(ϕ) and c(ϕ) as follows.
Definition 26 (Subformulae). Given an ALC-formula ϕ, we have that Definition 27 (Subconcepts). Given a an ALC-formula ϕ, c(ϕ) is the minimal set satisfying the following conditions: Definition 28. Let (T, o, f ) be a model candidate for ϕ. Then, the interpretation I (T,o,f ) is defined as: a I := a, for all a ∈ ind(ϕ); Example 29. Let ϕ = (C = ⊤) ∧ ¬(C(a) ∧ ¬(r(a, b))). Then, we have: In any quasimodel (T, o, f ) for ϕ, we have that ϕ ∈ f . However this also implies that (C = ⊤), ¬(C(a) ∧(¬r(a, b))) ∈ f . Consequently (C(a) ∧(¬r(a, b))) ∈ f and thus, C(a) ∈ f or ¬r(a, b) ∈ f . Hence, there are only three possible formula types for f : Assuming that for each of these possible formula types there is at least one quasimodel of f , we get that: It is easy to check that the formula above is equivalent to ϕ.
Proof. The proof follows by induction in the structure of φ. Base: φ is atomic.
Lemma 31. For every ALC-formula φ and formula type f for φ, if φ, ϕ ∈ f then f ∩ f(ϕ) is a formula type for ϕ.
Therefore, we conclude that f is a formula type.
We still need to show that The case (ii) is trivial. So we focus only on case (i).
To show Theorem 14, we use Lemma 38.
Lemma 38. Let ϕ be an ALC-formula. If f ∈ τ (ϕ) then Proof. The proof follows by induction in the degree of φ.
In this case, we know from Lemma 37 that (T ′ , o ′ , f ′ ) = qm(ϕ, M ) is a quasimodel for ϕ. From Theorem 14, we know that: