One-sentence Summary

University of Oslo and Cardiff University formalize model change for description logic concepts through eviction, reception, and revision operations, showing that revision does not reduce to a simple combination of eviction and reception and establishing compatibility results for $\mathcal{EL}_\perp$EL⊥​ and $\mathcal{ALC}$ALC concepts.

Key Contributions

• A formal model change framework is introduced for description logic concepts that are modified relative to pointed interpretations, with three change operations: eviction for removing models, reception for adding models, and revision for combining removal and addition.

• A formal notion of model revision is defined, and negative results show that revision is not reducible to a simple combination of eviction and reception for description logic concepts.

• Positive and negative compatibility results are established for eviction and reception of $\mathcal{EL}_\perp$EL⊥​ and $\mathcal{ALC}$ALC concepts across classes of models, with compatibility holding under broader model classes for $\mathcal{EL}_\perp$EL⊥​ than for $\mathcal{ALC}$ALC.

Introduction

Belief change asks how an agent updates what it believes when new evidence arrives, a core problem in knowledge representation and ontology construction. In many applications, especially learning from interpretations and description logic modeling, it is more natural to specify a change by the pointed models that should remain or be introduced than by logical formulae. For example, observing or learning about a concept may require discarding one possible world, adding another, or doing both at once while preserving as much of the existing concept as possible.

Prior work has addressed model based updates mainly through ontology learning, least common subsumers, and learnability of description logic concepts using positive and negative pointed interpretations. These lines of work clarify when models characterize concepts, but they do not fully cover operators for removing and adding models under minimal change postulates, and they do not treat the combined operation needed when a single update both rejects old models and accepts new ones. The missing challenge is to define and study such model change operations directly for description logic concepts.

The authors study eviction and reception for description logic concepts in ALC and EL_bottom, giving theoretical results about when minimal removal or addition of models can be represented. They also introduce model revision as a more general operation that adds and removes models in one step, show that it is not just eviction followed by reception, and provide results and negative results for description logic concepts.

Method

The method is built around an abstract change operator that updates a finite logical base when the available semantic evidence changes. The framework treats a description logic as a satisfaction system $\Lambda = (\mathcal{L}, \mathfrak{M}, \models)$Λ=(L,M,⊨), where $\mathcal{L}$L is a concept language, $\mathfrak{M}$M is a collection of interpretations, and $\models$⊨ maps concepts to their models. A finite base $B \in \wp_f(\mathcal{L})$B∈℘f​(L) denotes a finite set of formulas, and $\mathrm{mod}(B)$mod(B) is the class of models satisfying $B$B. The central operator is a model change operator defined on a chosen class of models $\mathcal{C} \subseteq \wp(\mathfrak{M})$C⊆℘(M):

This operator receives a finite base and a set of models and returns another finite base. The main design challenge is that some desired model updates cannot be represented finitely in the target language. Therefore, the framework does not simply perform set union or set difference. It searches for a closest finite representable base, where minimality is controlled by rationality postulates.

The framework separates two basic operations, reception and eviction, and then generalizes them into a revision operator.

Reception is designed to add a set of models $\mathbb{M}$M to the models of a base $B$B. It is denoted by $\mathsf{rcp}(B,\mathbb{M})$rcp(B,M) and must satisfy success, meaning that every model in $\mathbb{M}$M must become a model of the updated base. It also satisfies persistence, which forbids removing existing models during reception. The key finiteness principle is finite temperance: if extra models are added beyond $\mathrm{mod}(B) \cup \mathbb{M}$mod(B)∪M, those extra models must be required for finite representability. Uniformity ensures that the result depends on the semantic content of the update rather than on syntactic accidents or structural differences that are not detectable by the logic.

The selection mechanism for reception is expressed through minimal finite representable supersets. Let $\mathrm{FR}(\Lambda)$FR(Λ) be the collection of model sets that are representable by finite bases over $\Lambda$Λ. The operator defines

as the family of minimal finite representable supersets of $\mathrm{mod}(B) \cup \mathbb{M}$mod(B)∪M. A rational reception operator selects a base whose model set comes from this family:

If the language cannot distinguish a needed model from another undesired model, reception may be forced to add both. The rational design therefore adds only what is unavoidable to reach finite representability. When several minimal finite representable supersets exist, a choice function selects one. These maxichoice selections coincide with the class of rational reception operators.

Eviction is the dual operation. It removes a set of models $\mathbb{M}$M from the models of $B$B. The operator is denoted by $\mathsf{evc}(B,\mathbb{M})$evc(B,M) and must satisfy success, meaning that no model in $\mathbb{M}$M remains in the updated base. Inclusion ensures that eviction does not add new models. Finite retainment ensures that any additional removed models are necessary for finite representability. Uniformity again removes sensitivity to syntax and irrelevant model structure.

The finiteness requirement is handled through maximal finite representable subsets. Given the desired residual model set $\mathrm{mod}(B) \setminus \mathbb{M}$mod(B)∖M, the framework defines

as the family of greatest finite representable subsets contained in $\mathrm{mod}(B) \setminus \mathbb{M}$mod(B)∖M. A rational eviction operator selects one member from this family:

If this family is empty, then no rational eviction operator exists for the given class of models. Classes for which the family is nonempty for every admissible input are called eviction compatible. In such classes, maxichoice eviction operators implement rational eviction by choosing among the maximal finite representable outcomes.

The framework introduces model revision as a stronger operation. Revision takes a base $B$B and two disjoint model sets: $\mathbb{M}^+$M+, the models to be added, and $\mathbb{M}^-$M−, the models to be removed. The result is denoted by $\mathsf{rev}(B,\mathbb{M}^+,\mathbb{M}^-)$rev(B,M+,M−). This operation cannot be implemented by simply composing reception and eviction, because reception may reintroduce models that revision is required to remove, and eviction may delete models needed for adding $\mathbb{M}^+$M+. Therefore, revision is defined directly over pairs of model sets.

The first requirement is success:

and

Success may fail even when $\mathbb{M}^+$M+ and $\mathbb{M}^-$M− are disjoint. This happens when the logic identifies distinct models semantically, for example through bisimulation closure. In such cases, any base that satisfies one model must also satisfy a model that the revision is supposed to exclude. The framework therefore restricts attention to revision realisable classes, where the required addition and removal are not inherently contradictory.

Minimal change is captured by additional postulates. Vacuous expansion says that if all models in $\mathbb{M}^+$M+ already satisfy $B$B, revision should only remove models and should not add anything new. Vacuous removal says that if all models in $\mathbb{M}^-$M− already violate $B$B, revision should only add models and should not remove any model of $B$B. Lethargy combines the two: if $\mathbb{M}^+$M+ is already accepted and $\mathbb{M}^-$M− is already rejected, the base should remain unchanged.

A stronger minimality principle, circumspection, controls cases where extra additions or removals are needed for finite representability. It says that if a set $X^-$X− of extra models is removed and a set $X^+$X+ of extra models is added to produce a finite representable revision candidate, then any smaller candidate must fail to be finite representable. In other words, the extra changes must be indispensable. The framework uses this principle to exclude revisions that discard or acquire unnecessary models when a more conservative finite representable result exists.

The operator construction uses candidate model sets that already satisfy the basic add and remove constraints. For a satisfaction system $\Lambda$Λ, define

This is the set of all finite representable model sets that accept every model in $\mathbb{M}^+$M+ and reject every model in $\mathbb{M}^-$M−. The next task is to choose a candidate that is closest to the original base $\mathrm{mod}(B)$mod(B).

Closeness is measured by symmetric difference. For model sets $Y_1$Y1​, $Y_2$Y2​, and reference set $\mathbb{M}$M, define

Intuitively, $Y_1 \preceq_{\mathbb{M}} Y_2$Y1​⪯M​Y2​ means that transforming $\mathbb{M}$M into $Y_1$Y1​ requires no more change than transforming $\mathbb{M}$M into $Y_2$Y2​. Applying this to $\mathbb{M} = \mathrm{mod}(B)$M=mod(B) yields an ordering over candidates in $\chi_\Lambda(\mathbb{M}^+,\mathbb{M}^-)$χΛ​(M+,M−). A naive relational revision operator selects a minimal candidate from this family. This captures circumspection, but it can still violate vacuous expansion or vacuous removal.

The full symmetric differential revision operator strengthens this selection with context dependent constraints. If $\mathbb{M}^+ \subseteq \mathrm{mod}(B)$M+⊆mod(B), the operator must not add models, so it treats every countermodel of $B$B as an additional model to be removed. This is represented by selecting from

If $\mathbb{M}^+ \not\subseteq \mathrm{mod}(B)$M+⊆mod(B) but $\mathbb{M}^- \cap \mathrm{mod}(B) = \varnothing$M−∩mod(B)=∅, the operator must not remove models, so it treats every model of $B$B as an additional model to be added. This is represented by selecting from

In the remaining mixed case, the operator selects a minimal candidate from

Formally, the result is a model set $\mathbb{M}$M satisfying:

when $\mathbb{M}^+ \subseteq \mathrm{mod}(B)$M+⊆mod(B);

when $\mathbb{M}^+ \not\subseteq \mathrm{mod}(B)$M+⊆mod(B) and $\mathbb{M}^- \cap \mathrm{mod}(B) = \varnothing$M−∩mod(B)=∅; and otherwise

This construction is designed so that vacuous expansion, vacuous removal, and circumspection are all preserved. The resulting symmetric differential revision operators are exactly those satisfying the core rationality principles for revision.

The design also relates revision to the two primitive operations. If a binary class of model pairs is decomposable, meaning that for every pair $(\mathbb{M}^+,\mathbb{M}^-)$(M+,M−) it also contains $(\mathbb{M}^+,\varnothing)$(M+,∅) and $(\varnothing,\mathbb{M}^-)$(∅,M−), then the positive components form a reception candidate class and the negative components form an eviction candidate class. Compatibility of revision on such a decomposable class implies compatibility of reception on the add side and eviction on the remove side. Conversely, rational reception and eviction operators induce rational revision operators on the corresponding empty add or remove cases.

For description logic concept learning, the framework specializes the satisfaction system to the semantics of EL$_\perp$⊥​ concepts or ALC concepts. The general method requires that the selected binary class of model pairs be revision compatible. In some settings, even finite tree shaped pointed interpretations are not enough to ensure revision compatibility for EL$_\perp$⊥​ and ALC concept satisfaction systems. For ALC, a positive compatibility result is obtained when the considered model sets are closed under bisimulation over a finite signature. This restriction aligns the semantic boundaries of the logic with the candidate model sets used by the revision operator, making it possible to select finite representable outcomes while preserving the required add and remove constraints.

Experiment

The experiments evaluate eviction and reception compatibility for satisfaction systems based on EL⊥ and ALC description logic concepts over pointed interpretations. They find that EL⊥ concepts are eviction compatible and become reception compatible when restricted to sets of finite tree shaped pointed interpretations, while plain EL and ALC do not satisfy eviction compatibility. Reception compatibility fails more broadly for both EL⊥ and ALC under many tree shaped or finite signature restrictions, with ALC achieving compatibility only under strong finiteness assumptions on both the model set and signature.

For EL concepts extended with bottom, eviction compatibility holds while reception compatibility fails in general. Restricting models to finite tree-shaped pointed interpretations restores reception compatibility for this system. For ALC concepts, both properties fail in general, and they hold only under stronger finiteness and tree-shaped restrictions over finite signatures. EL with bottom is eviction compatible but not generally reception compatible Finite tree-shaped models make EL with bottom reception compatible ALC concepts are neither eviction nor reception compatible without strong model restrictions Combined finite, tree-shaped, finite-signature restrictions restore both properties for ALC

The experiments evaluate eviction and reception compatibility for description-logic concept extensions. They show that EL with bottom is eviction compatible, while reception compatibility requires finite tree-shaped pointed models. For ALC concepts, both compatibility properties fail without strong restrictions and are restored only under combined finite, tree-shaped, and finite-signature conditions.