We study belief change for the case in which beliefs are expressed as concepts in description logic. We consider that the incoming information is in the format of a set of pointed interpretations and investigate eviction (removal of pointed models) and reception (addition of pointed models). We provide preliminary results in this setting, establishing whether ℰℒ⊥ and ℒ-concepts are eviction/reception compatible. In Belief Change[1, 2, 3], when confronted with a piece of information, an agent must modify its beliefs minimally: only beliefs in conflict with the incoming information can be removed. The principle of minimal change is conceptualised via sets of rationality postulates, whilst several classes of operators that abide by such postulates were proposed. The standard paradigms of belief change, such as the AGM paradigm[1] of belief revision and the KM paradigm[4] of belief update, assume the incoming information to be represented as formulae. In other areas, however, diferent forms of representing incoming information, such as sets of finite models, have been addressed. In the learning from interpretations setting [5], for example, the goal is to identify a concept that is satisfied by a given set of interpretations, classified as positive, while falsified by another given set of interpretations (classified as negative). Ideally, the concept should also follow the principle of minimal change, in the sense that the identified concept should be as close as possible to the set of positive interpretations. Guimaraes et al. [6] have generalised the belief change paradigm to the setting where the incoming information is expressed as a set of interpretations, while the new corpus of beliefs should be finitely representable. Two main operations were proposed: eviction, which consists in removing the given set of interpretations; and reception, which consists in accommodating the given set of interpretations. Keeping the principle of minimal change and finite representation in this setting is challenging, and the authors have identified that eviction and reception are not definable in some logics. In this work, we deepen this investigation and consider concepts expressed in the ℰℒ⊥ and ℒ description logics (DLs). We show that while eviction is definable in ℰℒ⊥, reception is not definable in ℰℒ⊥ nor ℒ.
Following [
This view also facilitates the generalisation of some results that do not depend on properties of the consequence relation of the logic.
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 . An arbitrary set of models M ⊆ M within Λ is ifnitely representable if there is ℬ ∈ f (ℒ) such that mod(ℬ) = M. FR(Λ) denotes the collection of all finitely representable sets of models in Λ , that is, the set {M ⊆ M | ∃ℬ ∈ f (ℒ) : mod(ℬ) = M}. Also, we say that a set of formulae ℬ ⊆ ℒ is finitely representable if there is a ℬ′ ∈ f (ℒ) with mod(ℬ) = mod(ℬ′).
Eviction turns the current belief state into a new one not satisfied by any of the input models. Reception turns the current belief state into a new one satisfied by all the input models. Definition 1. For all satisfaction systems Λ = ( ℒ, M, |=) and M ⊆ M, MaxFRSubs(M, Λ) := {M′ ∈ FR(Λ) | M′ ⊆ MinFRSups(M, Λ) := {M′ ∈ FR(Λ) | M ⊆
M and ̸ ∃M′′ ∈ FR(Λ) with M′ ⊂ M′ and ̸ ∃M′′ ∈ FR(Λ) with M ⊆
′′ M ⊆
′′ M ⊂
M}.
M′}.
Definition 2. An eviction operation for a satisfaction system Λ = ( ℒ, M, |=) is a function evc : f (ℒ)× (M) → f (ℒ) that satisfies the following postulates, for all M, M′ ⊆ M and for all ℬ ∈ f (ℒ): (success) M ∩ mod(evc(ℬ, M)) = ∅. (inclusion) mod(evc(ℬ, M)) ⊆
mod(ℬ). (uniformity) MaxFRSubs(mod(ℬ) ∖ mod(evc(ℬ, M)) = mod(evc(ℬ′, M′)). (finite retainment) If mod(evc(ℬ, M)) ⊂
M′ ⊆
mod(ℬ) ∖ M then M′ ̸∈ FR(Λ) .
M, Λ) =
M′, Λ) implies Definition 3. A reception operation for a satisfaction system Λ = ( ℒ, M, |=) is a function rcp : f (ℒ)× (M) → f (ℒ) that satisfies the following postulates, for all M, M′ ⊆ M and for all ℬ ∈ f (ℒ): (success) M ⊆
mod(rcp(ℬ, M)). (persistence) mod(ℬ) ⊆
mod(rcp(ℬ, M)). (finite temperance) If mod(ℬ) ∪ M ⊆ (uniformity) MinFRSups(mod(ℬ) ∪ mod(rcp(ℬ, M)) = mod(rcp(ℬ′, M′)).
M′ ⊂ M, Λ) mod(rcp(ℬ, M)) then M′ ̸∈ FR(Λ) .
=
M′, Λ) implies
For a discussion on the postulates presented in this section, see [
DL Concepts Let NC and NR be countably infinite and pairwise disjoint sets of concept names and role
names, respectively. ℰℒ-concepts are built according to the rule: , ::= ⊤ | | ( ⊓ ) | (∃.),
where ∈ NC and ∈ NR. ℰℒ⊥-concepts extend ℰℒ by allowing ⊥ (interpreted as the empty set).
ℒ-concepts extend ℰℒ-concepts with the rule ¬ (recall that ⊓ ¬ is equivalent to ⊥, so ℒ
extends ℰℒ⊥). We may omit parentheses if there is no risk of confusion. A pointed interpretation is a
pair (ℐ, ) where ℐ = (· ℐ , ∆ ℐ ) is an interpretation and ∈ ∆ ℐ . A pointed interpretation (ℐ, ) satisfies
a concept if ∈ ℐ . The semantics of ℰℒ, ℰℒ⊥, and ℒ is defined using interpretations, as usual
for DLs [
Canonical Model Given a satisfiable ℰℒ⊥-concept , we inductively define the tree-shaped interpretation ℐ of , with the root denoted , as follows. When is ⊤, we define ℐ⊤ as the interpretation with ∆ ℐ⊤ := {⊤} and all concept and role names interpreted as the empty set. For a concept name ∈ NC we define ℐ as the interpretation with ∆ ℐ := {}, ℐ := {}, and all other concept and role names interpreted as the empty set. For = ∃., we define ℐ as the interpretation with ∆ ℐ := {} ∪ ∆ ℐ . All concept and role name interpretations are as for ℐ and we add (, ) to ℐ , and assume is fresh (i.e., it is not in ∆ ℐ ). Finally, for = 1 ⊓ 2 we define ∆ ℐ := ∆ ℐ1 ∪ (∆ ℐ2 ∖ {2 }), assuming ∆ ℐ1 and ∆ ℐ2 are disjoint, and with all concept and role name interpretations as in ℐ1 and ℐ2 , except that we connect 1 with the elements of ∆ ℐ2 in the same way as 2 is connected. In other words, we identify 1 with the root 2 of ℐ2 . Homomorphism Given two pointed interpretations (ℐ, 0), ( , 0), a homomorphism from (ℐ, 0) to ( , 0) is a function ℎ : ∆ ℐ → ∆ that satisfies: (i) ℎ(0) = 0; (ii) for all ∈ NC, if ∈ ℐ then ℎ() ∈ ; and (iii) for all ∈ NR, if (, ′) ∈ ℐ then (ℎ(), ℎ(′)) ∈ .
Our proof strategy for Theorem 2 is to invoke Theorem 1 (see [
Theorem 1 (Theorem 16[
[Adapted [15]] For all satisfiable ℰℒ⊥-concepts and , we have that |= ⊑ if there is a homomorphism from (ℐ, ) to (ℐ , ).
For all satisfiable ℰℒ⊥-concepts , if is satisfiable then there is an |= ⊥ ⊏ ′ ⊏ .
Let Λ( ℰℒ⊥-concepts) be the satisfaction system for ℰℒ⊥-concepts. ℰℒ⊥-concept ′ such that
Proof. We show that every non-empty M ⊆ M has an immediate predecessor in (FR(Λ( ℰℒ⊥-concepts)) ∪ {M}, ⊂ ) (the case M is empty is easy as ℰℒ⊥ has the ⊥ concept). Recall that an immediate predecessor of M in this case is a set of models M′ ∈ FR(Λ( ℰℒ⊥-concepts)) such that M′ ⊂ M and there is no M′′ such that M′ ⊂ M′′ ⊂ M. For this, we show that given a finitely representable set of models M, there is no infinite chain M1 ⊂ M2 ⊂ . . . of sets of models in (FR(Λ( ℰℒ⊥-concepts)) such that M ⊂ M for all ∈ N. Indeed, given M, M′ ∈ (FR(Λ( ℰℒ⊥-concepts)), with M′ ⊂ M, let , be ℰℒ⊥-concepts such that mod() = M and mod() = M′. By the semantics of ℰℒ⊥, we have that |= ⊏ . We want to show that there are finitely many ℰℒ⊥-concepts such that |= ⊏ ⊏ . Suppose there is no M′ ∈ MaxFRSubs(Λ( ℰℒ⊥-concepts)) such that M′ ⊂ M with M′ ̸= ∅. That is, ⊥ is the only ℰℒ⊥-concept such that |= ⊥ ⊑ , or, in other words, there is no (satisfiable) ℰℒ⊥-concept ′ such that |= ⊥ ⊏ ′ ⊏ . However, as M′ ⊂ M, we have that M ̸= ∅, so is satisfiable. This cannot be the case for ℰℒ⊥-concepts due to Section 3. By Section 3, if is satisfiable then there is ′ such that |= ⊥ ⊏ ′ ⊏ .
Then, there is M′ ∈ (FR(Λ( ℰℒ⊥-concepts)) such that M′ ⊂ M and M′ ̸= ∅, so is satisfiable. Let
be an ℰℒ⊥-concept such that |= ⊏ ⊏ (if there is no such concept then we are done). Since
|= ⊏ we have that is satisfiable. Then, by Lemma 3, there is a homomorphism from (ℐ, ) to
(ℐ, ). As is finite, the number of concept and role names that occur in is nfiite. Denote with
sig() the set of concept and role names occurring . Also, the existence of a homomorphism from
(ℐ, ) to (ℐ, ) and the definition of ℐ and ℐ imply that the set of concept and role names
occurring in is a subset of sig(). That is, there are finitely many concept and role names occurring in
and they are subset of sig(). Moreover, by definition of ℐ and ℐ, these interpretations correspond
to tree-shaped labelled structures where the depth of (the tree corresponding to) ℐ is less or equal to
the depth of ℐ. Since was an arbitrary ℰℒ⊥-concept such that |= ⊏ this holds for all such
concepts. As there are finitely many tree-shaped labelled structures with symbols in sig() and depth
bounded by , there are finitely many ℰℒ⊥-concepts (up to logical equivalence) such that |= ⊏ .
Then there are finitely many ℰℒ⊥-concepts (up to logical equivalence) such that |= ⊏ ⊑ .
This means that, by Theorem 16 in [
The previous result does not hold for ℰℒ (without ⊥) as it cannot express inconsistencies [
Theorem 3. Λ( ℰℒ⊥-concepts) and Λ( ℒ-concepts) are not reception-compatible.
The proof of Theorem 4 is based on [
Ana Ozaki is supported by the Research Council of Norway, project number 316022. This work is partly supported by the Research Council of Norway through its Centre of Excellence Integreat - The Norwegian Centre for knowledge-driven machine learning, project number 332645. [14] K. Agi, F. Wolter, M. Zakharyaschev, D. Gabbay, Many-dimensional modal logics : theory and applications, Elsevier North Holland, Amsterdam Boston, 2003. [15] F. Baader, R. Küsters, R. Molitor, Computing least common subsumers in description logics with existential restrictions, in: T. Dean (Ed.), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99, Stockholm, Sweden, July 31 - August 6, 1999. 2 Volumes, 1450 pages, Morgan Kaufmann, 1999, pp. 96–103. URL: http://ijcai.org/Proceedings/99-1/ Papers/015.pdf.