In this work, we consider the problem of modifying a knowledge base in the light of a (set of) models, while preserving the ifnite representation of the new knowledge base. We analyse the operation of removing models, called eviction, and the operation of adding models, called reception. Given that not all description logics (DLs) are eviction- and reception-compatible, we analyse natural restrictions of the general problem. In particular, we investigate eviction and reception in DL knowledge bases (ontologies), focusing on the very popular ℰℒ language and ℒ extended with boolean operators over the axioms. First, we extend existing negative results of incompatibility. Then, we place restrictions on the domains of eviction and reception functions on these logics that allows us to recover compatibility.
In traditional paradigms of Belief Change, such as the
AGM paradigm [
To address these shortcomings, Guimarães et al. [
In this work, we generalize the framework by
Guimarães et al. [
Our contribution We define the generalised
framework using the notion of compartments, we prove some
properties associated with the new framework, in
particular, that eviction (and reception) compatibility with a
satisfaction system implies eviction (and reception)
compatibility of any compartment of that system. We then
consider ℰℒ⊥, where we present two strategies for
reception for the case in which the input is a single finite
model. ℒ is neither eviction nor reception
compatible (assuming an infinite signature for the reception
case). We prove that it is not eviction compatible (the
proof works with finite or infinite signature). Then, we
build on our previous work [
Let NC, NR and NI be countably infinite and pairwise
disjoint sets of concept names, role names, and individual
names, respectively. ℰℒ concepts are built according to
Organisation In the next section, we provide basic the rule: ::= ⊤ | | ( ⊓ ) | ∃., where ∈ NC.
notions and notation relevant for this paper. In Section 3 ℰℒ⊥ concepts extend ℰℒ by allowing ⊥ (interpreted as
we recall the framework by Guimarães et al. [
We first provide basic general definitions and then we provide the necessary definitions for the DLs we consider.
The power set of a set is denoted by (), while the set of all finite subsets of is denoted by f (). We write * () to denote the non-empty subsets of . Following Aiguier et al. [15], Delgrande et al. [16], and [17], we use satisfaction systems to define logics. A satisfaction system is a triple Λ = (ℒ, M, |=), where ℒ is a language, M is a set of models, also called interpretations, and |= is a satisfaction relation which contains all pairs (, ℬ), where is an interpretation and ℬ is a base (that is, a subset of ℒ), such that satisfies ℬ (i.e., |= ℬ). We denote by ModΛ(ℬ) the set ::= | ¬( ) | ( ∧ ) where is an ℒ concept, , ∈ NI, and ∈ NR. We may omit parentheses if there is no risk of confusion. The usual concept inclusions ⊑ can be expressed with ⊤ ⊑ ¬ ⊔ and ¬ ⊔ ⊑ ⊤, which is (¬ ⊔ = ⊤). Assertions are expressions of the form (, ) and (), with ∈ NR, , ∈ NI, and ∈ NC. Whenever we speak of an ℰℒ⊥ ifnite base we mean a finite set of concept inclusions and assertions built from ℰℒ⊥ concepts. The same holds for ℰℒ and ℒ. The semantics of ℰℒ, ℰℒ⊥, ℒ, and ℒ are defined using interpretations, as usual for DLs [18, 19].
{M ⊆
M | ∃ℬ ∈ f (ℒ) : Mod(ℬ) = M}.
Guimarães et al. [17] defined two types of model change operations (functions from f (ℒ) × (M) to f (ℒ)) for modifying finite bases via a set of input models: eviction and reception. Eviction yields a base preserving as many { ∈ M | |= ℬ}. models of the original as possible, while excluding the input models. Eviction operations are constructed usWe will write simply Mod(ℬ) when the satisfaction sys- ing maximal subsets of the ideal resulting set of models, tem is clear from the context. formalised in Definition 1.
Satisfaction systems allow us to be more flexible and precise regarding the precise scope of the operations and Definition 1. Let Λ = (ℒ, M, |=) be a satisfaction sysconstructions we define. This view also facilitates the tem. Also, let M ⊆ M. gperonpeerartliiesastoiofnthoefcsoonmseequreesnucletsretlhaatitodnoofntohtedleopgeicn.d on MaxFRSubs(M, Λ) := {M′ ∈ FR(Λ) | M′ ⊆ M
A arbitrary set of models M ⊆ M within Λ is and ̸ ∃M′′ ∈ FR(Λ) with M′ ⊂ M′′ ⊆ M}. ifnitely representable if there is ℬ ∈ f (ℒ) such that Mod(ℬ) = M. FR(Λ) denotes the collection of all ifnitely representable sets of models in Λ, that is, the set
Eviction can only be adequately defined in satisfaction systems that are eviction-compatible, that is, in those where MaxFRSubs is never empty. Hence, we can use a FR selection function, that is, a function sel : Theorem 3 ([17]). A model change operation evc, deifned on an eviction-compatible satisfaction system Λ, is a maxichoice eviction function if it satisfies the following postulates: * (FR(Λ)) → FR(Λ), we can define eviction functions as follows.
Definition 2 ([17]). Let Λ be an eviction-compatible satisfaction system and sel a FR selection function on Λ.
The maxichoice eviction function on Λ defined by sel is a map evcsel : f (ℒ) × (M) → f (ℒ) such that:
Mod(evcsel(ℬ, M)) =
sel(MaxFRSubs(Mod(ℬ) ∖ M, Λ)). (success) M ∩ Mod(evc(ℬ, M)) = ∅. (inclusion) Mod(evc(ℬ, M)) ⊆
Mod(ℬ). (finite retainment) If Mod(evc(ℬ, M)) ⊂ Mod(ℬ) ∖ M then M′ ̸∈ FR(Λ). (uniformity) MaxFRSubs(Mod(ℬ) ∖ MaxFRSubs(Mod(ℬ′) ∖ M′, Λ) Mod(evc(ℬ, M)) = Mod(evc(ℬ′, M′)).
M′ ⊆ M, Λ) =
implies
Reception produces a base that has all the models of the original and the input. Definition 4 details the construction employed for characterising and defining reception functions.
Definition 4. Let Λ = (ℒ, M, |=) be a satisfaction system. Also, let M ⊆ M.
MinFRSups(M, Λ) := {M′ ∈ FR(Λ) | M ⊆ and ̸ ∃M ′′ ∈ FR(Λ) with M ⊆
′′ M ⊂
M′
M′}.
As with eviction, reception can only be constructed in reception-compatible satisfaction systems. Receptioncompatibility allows to define reception functions using FR selection function functions.
Definition 5 ([17]). Let Λ = (ℒ, M, |=) be a receptioncompatible satisfaction system and sel a FR selection function on Λ. The maxichoice model reception function on Λ defined by sel is a map rcpsel : f (ℒ) × (M) → f (ℒ) such that:
Mod(rcpsel(ℬ, M)) =
sel(MinFRSups(Mod(ℬ) ∪ M, Λ)).
Maxichoice reception functions can also be characterised via a set of postulates.
43–51 ⊆
M′ ⊂ M, Λ) =
implies Theorem 6 ([17]). A model change operation rcp, deifned on a reception-compatible satisfaction system Λ, is a maxichoice reception function if it satisfies the following postulates: (success) M ⊆
Mod(rcp(ℬ, M)). (persistence) Mod(ℬ) ⊆
Mod(rcp(ℬ, M)). (finite temperance) If Mod(ℬ) ∪ M Mod(rcp(ℬ, M)) then M′ ̸∈ FR(Λ).
Next, in light of the negative results on compatibility of important satisfaction systems [17], we will modify the framework discussed in this section by restricting the input space of model change operations.
While eviction and reception can be defined and characterised in some satisfaction systems, such as the usual for propositional logic and Kleene’s three-valued logic, there are also important satisfaction systems that are neither eviction- nor reception-compatible, as it is the case of the DL ℒ [17].
Here, we will attempt to circumvent the incompatibilities of a satisfaction system by placing restrictions on which bases and sets of models are allowed as input. We formalise these additional constraints with the notion of compartment.
Definition 7. A compartment of a satisfaction system Λ = (ℒ, M, |=), is a pair (B, I) such that B ⊆ f (ℒ) and I ⊆ (M).
Formally, given a satisfaction system Λ, a model change operation modulo a compartment (B, I) is a function C : B × I → FR(Λ).
In the following, we generalise the notions of evictionand reception-compatibility.
Let Λ be a satisfaction system, 1. A compartment (B, I) of Λ is evictioncompatible if for all ℬ ∈ B and M ∈ I:
MaxFRSubs(Mod(ℬ) ∖ M, Λ) ̸= ∅. 2. A compartment (B, I) of Λ is receptioncompatible if for all ℬ ∈ B and M ∈ I:
MinFRSups(Mod(ℬ) ∪ M, Λ) ̸= ∅.
If we consider an eviction-compatible compartment In the next two sections we study the cases of the clas(B, I), we can adapt the notion of maxichoice evic- sical DLs ℰℒ and ℒ. Several DLs are neither eviction tion function from Definition 2, by defining it as a not reception-compatible [17]. These impossibility remodel change operator modulo (B, I). The eviction- sults are proved specifically for each of the investigated compatibility of the compartment will ensure that the logics. We identify suficient conditions for a DL to not domain of the function is non-empty. Consequently, we be reception compatible. obtain a version of Theorem 3 when the input is restricted to reception-compatible compartments.
Theorem 12. Let ℒ be a monotonic DL with ⊤, that can represent inconsistencies and it is interpreted over an inCorollary 9. Let (B, I) be a eviction-compatible com- finite signature. Then Λ(ℒ) is not reception-compatible. partment of a satisfaction system Λ and evc be a model change operator modulo (B, I). The operator evc is a maxichoice eviction function modulo (B, I) if it satisfies the postulates success, inclusion, finite retainment, and uniformity from Theorem 3, for all ℬ ∈ B and M ∈ I.
Most of the expressive and interesting DLs can
express inconsistencies (either with full negation or just
⊥) and include the concept ⊤. Therefore, according to
Theorem 12, if one wants to perform reception in these
logics the only alternative is restricting to finite
signaProof sketch. The proof is analogous to the proof of The- tures. Eviction compatibility is lost if there is no way of
orem 3 [17, Theorem 5]. representing inconsistencies [
Similarly, in a reception-compatible compartment C, wise stated we consider only DLs over finite signatures we can define maxichoice reception functions modulo and that can express inconsistencies. It is worth recallC by constraining the domain of maxichoice reception ing that we are considering only compartments on finite functions from Definition 5. We get the following result models. as a consequence.
Corollary 10. Let (B, I) be a reception-compatible compartment of a satisfaction system Λ and rcp be a model change operator modulo (B, I). The operator rcp is a maxichoice reception function modulo (B, I) if it satisifes success, persistence, finite temperance, and uniformity from Theorem 6, for all ℬ ∈ B and M ∈ I.
We investigate the case of the very popular ℰℒ ontology language. In particular, we devise two strategies for reception in ℰℒ⊥ for the case in which the input is a single ifnite model. Since these approaches are only defined for compartments in which the model class contains only Proof sketch. The proof is analogous as the proof of The- singletons, we abuse the notation and write ℐ instead of orem 6 [17, Theorem 10]. {ℐ} whenever the meaning is clear. 5. The Case of ℰℒ⊥ Proof. Let C = (B, I) be a compartment of Λ = (ℒ, M, |=). For the first point, if Λ = (ℒ, M, |=) is eviction-compatible, then for any ℬ ∈ B ⊆ f ℒ and any M ∈ I ⊆ f (M), it holds that MaxFRSubs(ℬ ∖ M, Λ) ̸= ∅. Hence C is eviction-compatible.
The proof is analogous for the second point.
The new definitions and results based on compartments generalise the original ones because considering 5.1. A Model Product Approach for ℰℒ⊥ the compartment (f (ℒ), FR(Λ)) of Λ = (ℒ, M, |=) In this subsection, we consider an approach for performyields the original constructions and properties defined ing reception in compartments of the DL ℰℒ⊥. We profor a satisfaction system Λ. Proposition 11 shows that the pose the following strategy to perform the reception of a compatibility of a satisfaction system regarding eviction base ℬ with a single model (interpretation) ℐ: we turn ℬ or reception is transferred to all of its compartments. into one of its models, and we combine this model with Proposition 11. Given a compartment C of the satisfac- ℐ to produce the reception result. To combine these two tion system Λ: models, we define a product operation which preserves exactly the information satisfied by both models. We • If Λ is eviction-compatible then C is eviction- then produce the finite base for reception from the model compatible. obtained by the product operation. If ℬ is unsatisfiable the resut of the reception is a base that represents the • If Λ is reception-compatible then C is reception- input model exactly.
compatible. The main hurdle is to find a suitable model of the base. We need a model that satisfies exactly and only the information entailed by the knowledge base. Such models are called fit models: Definition 13. A model ℐ fits a base ℬ, if (i) ℐ is finite and (ii) for every ℰℒ⊥ formula , ℬ |= if ℐ |= .
Equivalently, we say that ℬ fits ℐ. Example 14 illustrates a base and one of its fit models. an extra concept name ⊥. As ⊥ is a concept name, we can define ensuring the obtained concept is not Example 14. Let ℬ = { ≡ ∃ .⊤, ≡ ∃ .}. Also, logically equivalent to ⊥, and for every model ℐ in this let ℐ = (Δℐ , · ℐ ) defined over {, } and such that desired class of models, we have Δℐ = {1, 2} ℐ = {1}
ℐ = {(1, 1)}.
Observation 15 shows that ℐ fits ℬ.
Observation 15. The interpretation ℐ from Example 14 ifts the base ℬ at that same example.
Indeed, in ℰℒ⊥, every finite model fits some finite set of concept inclusions (TBox). This result follows from the existence of algorithms that construct TBoxes that fit a given finite model [ 20, 21]. The existence of fit bases for any finite model also allows us to handle the case in which ℬ is unsatisfiable. Therefore, in the remainder of this subsection, we consider only compartments (B, I) of Λ(ℰℒ⊥) such that (1) all bases in B present a fit model ℐ such that {ℐ} ∈ I and (2) |M| = 1 for all M ∈ I. Such compartments are called fit compartments . As usual, the product operation on models is as follows.
Definition 16. The product of two models ℐ1 and ℐ2 is the model ℐ = ℐ1 × ℐ 2 where • Δℐ := Δℐ1 ×
Δℐ2 ; • ℐ := {(, ) | ∈ ℐ1 , ∈ ℐ2 }, for all
∈ NC; • ℐ := {((, ), (′, ′)) | (, ′) ∈ ℐ1 and
(, ′) ∈ ℐ2 }, for all ∈ NR. • The interpretation of complex concepts is defined
as usual.
Proposition 17. Let ℐ = ℐ1 × ℐ 2. For all ℰℒ⊥ concepts : (, ) ∈ ℐ if ∈ ℐ1 and ∈ ℐ2 .
The purpose of the product, say ℐ1 × ℐ 2, is to obtain a model that preserves precisely the information satisfied by both models ℐ1 and ℐ2. Although this is not true in general, there is a specific class of models in which the product satisfies such behaviour as long as the formulae of interest do not contain concepts logically equivalent to ⊥ (Theorem 25).
Definition 18. For every two models ℐ1 and ℐ2 in such a class, and ℰℒ⊥ concepts and , weak-preservation: if ∅ ̸|= ≡ ≡ ⊥ , then ℐ1 × ℐ 2 |= ⊑ if ℐ1 |= ⊑ and ℐ2 |= ⊑ .
Ideally, the property above should also cover concept inclusions involving concepts that are logically equivalent to ⊥. This issue can be easily overcome by applying a rewriting function that swaps each ⊥ symbol with
Definition 19. Let Σ ⊂ NC ∪ NR ∪ NI be a signature and ⊥ ∈ NC∖Σ. We define : ℰℒ⊥(Σ) → ℰℒ⊥(Σ∪{⊥}) inductively: • (⊥) = ⊥, • () = , if ∈ NC ∖ {⊥}, • (∃.) = ∃. (), • ( ⊓ ) = () ⊓ (), • (()) = ( ()()), • ((, )) = (, ).
The missing ingredient is to frame precisely the so well-behaved class of models mentioned above. In order to capture the weak-preservation condition, we consider models in which the extension of every concept that is not tautologically equivalent to ⊥ must be non-empty.
We start showing that every model can be turned into an equivalent model satisfying weak-preservation. By equivalent, we mean that the original model satisfies a formula if the new model satisfies its rewriting ( ).
This model is called an -extension.
Definition 20. Let ⊥ ∈ NC, Σ ⊂ ((NC ∖ {⊥}) ∪ NR ∪ NI) be a signature, and ℐ = (Δℐ , · ℐ ) be a model defined over Σ. The -extension of ℐ is the interpretation (ℐ) = (Δℐ ∪ {}, · (ℐ)) such that: • (⊥)(ℐ) = {}. • (ℐ) = ℐ ∪ {} for all ∈ NC ∖ {⊥}. • (ℐ) = ℐ ∪ {(, )} for all ∈ Σ ∪ NR.
• (ℐ) = ℐ , for all ∈ Σ ∪ NI.
Where we assume w.l.o.g. that ∈/ Δℐ and ⊥ ∈ NC ∖ Σ.
Proposition 21 states that the -extension of an interpretation ℐ extends each concept with a fixed sentinel symbol , as long as is satisfiable.
Proposition 21. Let ℐ = (Δℐ , · ℐ ) be a model defined over a finite signature Σ and (ℐ) = (Δℐ ∪{}, · (ℐ)) its -extension. For all ℰℒ⊥ concepts , either ∅ |= ≡ ⊥ or ∈ (ℐ).
An -extension also preserves entailments over the original signature, as shown in Lemma 22. Lemma 22. Let ⊥ ∈ NC, let Σ ⊂ ((NC ∖ {⊥}) ∪
([17]). A satisfaction system Λ = NR ∪ NI) be a finite signature, and let ℐ = (Δℐ , · ℐ ) be (ℒ, M, |=) has the RMBP property if for every ℬ1, ℬ2 ⊆ a model over Σ, and an ℰℒ⊥ formula over Σ. Then ℒ, and ℐ ∈ M: ℐ ∈ Mod(ℬ1 ∪ ℬ2) if ℐ ∈ Mod(ℬ1) and ℐ ∈ Mod(ℬ2).
The RBMP induces a ‘uniqueness’ property of the functions MinFRSups and MaxFRSubs.
Corollary 31 ([17]). Let Λ be the usual satisfaction system of ℰℒ⊥. |MinFRSups(M, Λ)| ≤ 1.
In fit compartments of
For every set of models M, ℰℒ⊥, the product reception ℐ |= if (ℐ) |= .
Propositions 23 and 24 depict a convenient relationship between the translation function and -extensions. , ( ())(ℐ) = ℐ ∪ {}.
Proposition 23. For all -extension (ℐ) and concept Proposition 24. Let ℐ be a model defined over the finite signature Σ ⊆
(NC ∖ {⊥}) ∪ NR ∪ NI and an ℰℒ⊥
It is worth stressing that -extensions are models by definition, and therefore we can apply the product operation to them. This guarantees that the product of two -extensions satisfies weak-preservation (Definition 18), leading to Theorem 25. (ℐ2) |= ( ⊑ ).
Theorem 25. For all ℰℒ⊥ concepts , , we have that (ℐ1) × (ℐ2) |= ( ⊑ ) if (ℐ1) |= ( ⊑ ) and of ℰℒ⊥
Distel [20], Guimarães et al. [21] have shown that in ℰℒ⊥, every finite model fits some finite base be a function that maps each finite model that ℐ fits. We say that fitis a fit assignment.
ℬ. Let fit (·) ℐ to some base
At this point, we have all the necessary ingredients to define our reception operation on products. The construction is suitable for all fit compartments in
ℰℒ⊥.
Let C = (B, I) be a fit compartment , and fita fit assignment. A product reception operation on C is a function rcp× : B × I → B, s.t rcp× (ℬ, ℐ) = ︂{
fit(ℐ) fit((ℐℬ) × (ℐ)) if ℬ |= ⊥; otherwise. where ℐℬ is a finite model that fits ℬ
.
Proposition 27. The -extensions are closed under the product operation. over the finite signature (ℐ) |= if (ℐ) |= ( ).
Σ ⊆ (NC ∖ {⊥}) ∪ NR ∪ NI.
The product reception operation retains exactly the formulae entailed by the base and input model.
Corollary 29. Let C = (B, I) be a fit compartment of ℬ |= ⊑ and ℐ |= ⊑ . ℰℒ⊥, and rcp×
a product operation on C. For all ℰℒ⊥ concept inclusions ⊑ , rcp× (ℬ, ℐ) |= ⊑ if
The ℰℒ⊥ satisfaction system presents some interest- then |M| = {ℐ} for some finite model ℐ . ing behaviours regarding reception operations. One of such properties is the reverse monotonic bijection property
As the result of the reception must be finite, we extract from the incoming model only formulae with size less or (RMBP).
equal to a given number . concept over Σ. It holds that ( ())(ℐ) = (ℐ) ∪ {}. operations are exactly those reception operations that satisfy all four postulates from Theorem 6.
Lemma 28. Let ℐ be a model and an ℰℒ⊥ formula
ℐ in C.
Theorem 32. Let C = (B, I) be a fit compartment of ℰℒ⊥. A model change operation rcp on C satisfies all four postulates on Theorem 6 if there is some product reception operation rcp ×
such that Mod(rcp(ℬ, ℐ)) = Mod(rcp× (ℬ, ℐ)), for all bases ℬ and all interpretations
While the restriction to fit compartments yields an elegant construction, it does not cover every ℰℒ⊥ base, not even when restricting ourselves only to concept inclusions (TBoxes) as Example 33. be a finite model of ≥ Example 33. Let ℬ = { ⊑ ∃.}. For all ≥ 1 it holds that ℬ |= ∃. ⊑ ∃(+).. Also, let ℐ
0 and ℬ. Since Δℐ is finite, for every
ℰℒ⊥ concept , there will be at most 2 possible extensions under ℐ, where = Δℐ . However, consider now the set of concepts {∃. | 1 ≤ ≤
2 + 1}. By the piand ∃. in this set such that ℐ |
= ∃. ≡ ∃ geonhole principle, there will be distinct concepts ∃.
..
W.l.o.g., let us assume < , then we have that ℐ | ∃. ⊑ ∃. but ℬ ̸| = ∃. ⊑ ∃.. Since ℐ is
= an arbitrary finite model of ℐ, ℬ has no fit model.
In the next subsection, we explore another interesting approach which covers all reception-compatible compartments of Λ(ℰℒ⊥).
The product operation we defined in the previous subsection works only for fit compartments. In this section, we propose a broader approach. We extract from the incoming model some specific formulae that it satisfies and we retain from such a set only the formulae that are entailed by the base. The obtained set corresponds to the reception result. This strategy works on every compartment (B, I) that is reception-compatible for DLs that are monotonic and idempotent and such that if M ∈ I
The length of the greatest concept of an ℰℒ⊥ formula DLs (Theorem 38). In this section, we investigate how
is given by to extend model change operations to one such logic as
a study case. We look precisely at the logic ℒ1,
⎧⎪max(||, ||) if = ⊑ which corresponds to the DL ℒ enriched with boolean
gcp( ) = ⎨|| if = () operators over ℒ axioms. As ℒ is a prototypical
⎪⎩1 if = (, ) DL, it shares many similarities with other logics in the of
DL family. Our results are built on proofs for the ℒ
We also extend this notion to finite bases: gcp(ℬ) = case without boolean operators over the axioms [
Theorem 38. Λ(ℒ) is Observation 35. For every positive integer and in- compatible nor reception-compatible. terpretation ℐ, if ∈ ℬℐ then ℐ |= .
neither eviction
Proof. The fact that Λ(ℒ) is not reception, compatible follows from Theorem 12 (the case for when ℐ |= ℬ then ℬ ⊆ ℬ ℐ the signature is finite is open). We then show that Λ(ℒ) is not eviction-compatible (the proof works if the signature is finite or infinite). Let Lemma 36. If ℬ is finite and where = gcp(ℬ).
Proof. Let us assume that ℬ is finite, = gcp(ℬ), and
be the saturation of ℐ bounded to . ℐ |= ℬ. Let ℬℐ Let ∈ ℬ. As = gcp(ℬ), we get that gcp( ) ≤ .
Therefore, as ℐ |= ℬ, we get that ℐ |= . This means that ∈ ℬℐ.
In order to perform the reception of a knowledge base ℬ with a model ℐ, we saturate ℐ to an upper bound , and we intersect such a set with the all information entailed by ℬ. Precisely, we define our reception operation as (ℬ) ∩ ℬℐ.
Theorem 37. A compartment C = (B, I) is receptioncompatible if for all pairs (ℬ, ℐ) ∈ B × I there is some positive integer such that
Mod(ℬ′) ∈ MaxFRSubs(Mod(ℬ) ∪ {ℐ}, Λ), where ℬ′ = Cn(ℬ) ∩ ℬℐ.
Theorem 37 characterises all reception-compatible compartments, including the maximal ones, via the saturation construction when the input is a single finite model. Although Theorem 37 focuses on ℰℒ⊥, it can be easily extended to other satisfaction systems, as the proof requires only the logic to be both monotonic and idempotent, as well as presenting a notion of length of formulae analogous to gcd. 6. The Case of ℒ The framework we presented in Section 4 is general enough to cover several satisfaction systems without imposing much constraints upon the logics being used to represent an agent’s beliefs. However, there are interesting logics used for knowledge representation that are not reception-compatible, as it is the case of some
Λ(ℒ) = (ℒℒbool , Mℒbool , |=ℒbool ) be the usual satisfaction system for ℒbool. For conciseness, we will write |= instead of |=ℒbool within this proof. Let ℬ⊤ = {⊥ ⊑ ⊤}, that is, Mod(ℬ⊤) = M. Also, given a fixed but arbitrary= (∈NN,· Ian )d w h∈erNeR, we define models of the form
= {(, + 1) | ∈ N, 0 ≤ < } and = 0, and similarly ∞ = (N, · ∞ ) where ∞
= {(, + 1) | ∈ N} and ∞ = 0. Let M be the set of all models such that for some ∈ N we have that ∈ (∀.⊥) . That is, there is no loop or infinite chain of elements connected via the role starting from . By definition of M, we have that ∞ ̸∈ M since this model has an infinite chain of elements connected via the role starting from , while ∈ M for all ∈ N.
To prove that Λ(ℒ) is not eviction-compatible, we need to prove that there is no ℬ ∈ f (ℒℒbool ) such that Mod(ℬ) ∈ MaxFRSubs(M, Λ(ℒ)), that is, MaxFRSubs(M, Λ(ℒ)) = ∅. Intuitively, we want to show that we cannot find a maximal ℒbool ontology that finitely represents the result of removing the models in M ∖ M from ℬ⊤. First, we recall the following claims.
Claim 39 ([
We are now ready to show that Λ(ℒ) is not eviction-compatible. Suppose to the contrary that there is ℬ ∈ f (ℒℒbool ) such that Mod(ℬ) ∈ MaxFRSubs(M, Λ(ℒ)). If there is ∈ N such that ̸|= ℬ then2
+1 ℬ′ := ℬ ∨ ( ⨆︁ (∃.⊤ ⊓ ¬∃+1.⊤) = ⊤), =0 • for every concept , if ¬( = ⊤) ∈ f then there
is c ∈ such that ̸∈ c; • is not empty.
Theorem 42 establishes the connection between quasimodels and formulae in ℒ.
Theorem 42 (Theorem 2.27 [19]). An ℒ-formula is satisfiable if has a quasimodel.
One can associate a model ℐ to each quasimodel for such that ℐ |= (see Definition 43).
Definition 43. Given a quasimodel = ( , , f ) is such that |= ℬ′. Moreover, Mod(ℬ) ⊂ for an ℒ-formula , we define a model ℐ = Mod(ℬ′). By definition of ℬ′ and M, we also (Δℐ , · ℐ ) as follows: have that Mod(ℬ′) ∈ MaxFRSubs(M, Λ(ℒ)).
This contradicts the assumption that Mod(ℬ) ∈ • Δℐ := MaxFRSubs(M, Λ(ℒ)). So, for all ∈ N, we • ℐ := { ∈ | ∈ } for all ∈ NC; have that |= ℬ.
Then, by Claims 39 and 40, it follows that • ℐ := {(, ′) ∈ 2 | ¬∃. ∈ ⇒ ¬ ∈ ′} ∞ |= ℬ. Since, as already mentioned, for all ∈ NR. ∞ ̸∈ M, this contradicts the assumption that Mod(ℬ) ∈ MaxFRSubs(M, Λ(ℒ)). Thus, MaxFRSubs(M, Λ(ℒ)) = ∅.
Given a class of models I, the class of ℒformulae induced by is the class of ℒ-formulae that contains and any ℒ-formulae that is a boolean combination of atoms in .
Quasimodels Now, we employ quasimodels in a new strategy for belief change in ℒ. Our approach is based on the translation of formulae in ℒ into DNF. Let be an ℒ formula. Let f( ) and c( ) be the set of all subformulae and subconcepts of closed under single negation, respectively. A concept type for is a subset c ⊆ c( ) such that: ∈ c if ¬ ̸∈ c, for all ∈ c( ); and (2) ⊓ ∈ c if {, } ⊆ c, for all ⊓ ∈ c( ). A formula type for is a subset f ⊆ f( ) such that: (1) ∈ f if ¬ ̸∈ f , for all ∈ f( ); and (2) ∧ ∈ f if {, } ⊆ f , for all ∧ ∈ f( ).
We may omit ‘for ’ if this is clear from the context. A model candidate for is a triple ( , , f ) such that is a set of concept types, is a function from ind( ) to , f a formula type, and ( , , f ) satisfies the conditions: ∈ f ; () ∈ f implies ∈ (); (, ) ∈ f implies {¬ | ¬∃. ∈ ()} ⊆ ().
Definition 41 (Quasimodel). A model candidate ( , , f ) for is a quasimodel for if the following holds • for every concept type c ∈ and every ∃. ∈ c, there is c′ ∈ such that {} ∪ {¬ | ¬∃. ∈ c} ⊆ c′; • for every concept type c ∈ and every concept
, if ¬ ∈ c then this implies ( = ⊤) ̸∈ f ; 2Recall that has a chain of + 1 elements connected via the role .
Theorem 44. Consider the compartment (B , I ) where (1) I is the class of all subsets of models ℐ with a quasimodel for an ℒ-formula and (2) B is the class of ℒ-formulae induced by . Then, (B , I ) is both eviction and reception-compatible.
Proof. This theorem follows from the results on model
expansion and contraction presented earlier [
In this work, we investigate the model change operations of eviction and reception when applied to description logics such as ℰℒ and ℒ. We provide a more general negative result for reception in a large class of DLs. Moreover, generalise the framework proposed by Guimarães et al. [17] with the notion of compartments. These compartments allows us to define two reception functions in restricted domains, which satisfy the existing postulates for this operation. In particular, we restricted the input to singleton sets of finite models defined over finite signatures. While one of these reception functions applies specifically for fit ℰℒ⊥ compartments, the other can be employed in a broader class of compartments, including other DLs. Furthermore, we frame previous constructions for ℒ in the same framework, while