一句话总结

奥斯陆大学和卡迪夫大学通过驱逐、接纳和修订操作，形式化描述逻辑概念的模型变更，表明修订不能归约为驱逐与接纳的简单组合，并为 $\mathcal{EL}_\perp$EL⊥​ 和 $\mathcal{ALC}$ALC 概念建立兼容性结果。

核心贡献

• 引入一个形式化模型变更框架，用于相对于带点解释被修改的描述逻辑概念，包含三种变更操作：驱逐用于移除模型，接纳用于添加模型，修订用于组合移除和添加。

• 定义修订的形式化概念，并通过否定结果表明，对于描述逻辑概念，修订不能归约为驱逐与接纳的简单组合。

• 建立 $\mathcal{EL}_\perp$EL⊥​ 和 $\mathcal{ALC}$ALC 概念在不同模型类别上的驱逐与接纳兼容性的正向和否定结果，其中 $\mathcal{EL}_\perp$EL⊥​ 的兼容性在更广泛的模型类别下成立。

引言

信念变更研究一个 agent 在新证据到来时如何更新其相信的内容，这是知识表示和本体构建中的核心问题。在许多应用中，特别是在基于解释的学习和描述逻辑建模中，用应当保留或应当引入的带点模型来指定变更，往往比用逻辑公式更自然。例如，观察或学习一个概念时，可能需要舍弃一个可能世界、加入另一个可能世界，或同时做这两件事，同时尽可能保留现有概念。

相关工作主要通过本体学习、最小公共上位概念，以及利用正负带点解释对描述逻辑概念可学习性的研究来处理基于模型的更新。这些工作澄清了模型何时能刻画概念，但未完全覆盖在最小变更公设下移除和添加模型的操作，也未处理一次更新既拒绝旧模型又接受新模型时所需的组合操作。缺失的挑战是直接为描述逻辑概念定义并研究这些模型变更操作。

作者研究 ALC 和 EL_bottom 中描述逻辑概念的驱逐和接纳，给出模型最小移除或添加可表示性的理论结果。作者还引入模型修订作为一步完成添加和移除模型的更一般操作，证明它并不只是先驱逐后接纳，并为描述逻辑概念给出正向结果与否定结果。

方法

该方法围绕一个抽象变更算子构建，该算子在可用语义证据发生变化时更新一个有限逻辑基。框架将描述逻辑视为满足系统 $\Lambda = (\mathcal{L}, \mathfrak{M}, \models)$Λ=(L,M,⊨)，其中 $\mathcal{L}$L 是概念语言，$\mathfrak{M}$M 是解释集合，$\models$⊨ 将概念映射到其模型。有限基 $B \in \wp_f(\mathcal{L})$B∈℘f​(L) 表示一个公式有限集，$\mathrm{mod}(B)$mod(B) 是满足 $B$B 的模型类。核心算子是在选定模型类 $\mathcal{C} \subseteq \wp(\mathfrak{M})$C⊆℘(M) 上定义的模型变更算子：

$$\circ : \wp_f(\mathcal{L}) \times \mathcal{C} \to \wp_f(\mathcal{L}).$$∘:℘f​(L)×C→℘f​(L).

该算子接收一个有限基和一个模型集合，并返回另一个有限基。主要设计挑战是，某些期望的模型更新在目标语言中无法有限表示。因此，框架并不简单执行并集或差集运算，而是寻找最接近的可有限表示基，其中最小性由合理性公设控制。

框架首先分离出两个基本操作，接纳与驱逐，随后将它们推广为修订算子。

接纳旨在向基 $B$B 的模型添加一个模型集合 $\mathbb{M}$M。它记作 $\mathsf{rcp}(B,\mathbb{M})$rcp(B,M)，必须满足成功性，即 $\mathbb{M}$M 中的每个模型都必须成为更新后基的模型。它也满足持久性，禁止在接纳期间移除现有模型。关键的有限性原则是有限克制性：如果向 $\mathrm{mod}(B) \cup \mathbb{M}$mod(B)∪M 之外添加了额外模型，则这些额外模型必须是为了实现有限可表示性所必需的。均匀性确保结果取决于更新的语义内容，而非句法偶然或逻辑无法检测的结构性差异。

接纳的选择机制通过极小可有限表示上集表达。令 $\mathrm{FR}(\Lambda)$FR(Λ) 表示可由 $\Lambda$Λ 上有限基表示的模型集合类。该算子定义

$$\mathrm{MinFRSups}(\mathrm{mod}(B) \cup \mathbb{M}, \Lambda)$$MinFRSups(mod(B)∪M,Λ)

作为 $\mathrm{mod}(B) \cup \mathbb{M}$mod(B)∪M 的极小可有限表示上集族。一个理性接纳算子选择一个模型集属于该族的基：

$$\mathrm{mod}(\mathsf{rcp}(B,\mathbb{M})) \in \mathrm{MinFRSups}(\mathrm{mod}(B) \cup \mathbb{M}, \Lambda).$$mod(rcp(B,M))∈MinFRSups(mod(B)∪M,Λ).

如果语言无法将所需模型与另一个不期望的模型区分开来，接纳可能被迫同时添加两者。因此，理性设计只添加达到有限可表示性所不可避免的模型。当存在多个极小可有限表示上集时，由选择函数选出一个。这些极大选择与理性接纳算子类重合。

驱逐是对偶操作。它从 $B$B 的模型中移除一个模型集合 $\mathbb{M}$M。该算子记作 $\mathsf{evc}(B,\mathbb{M})$evc(B,M)，必须满足成功性，即 $\mathbb{M}$M 中没有模型仍留在更新后的基中。包含性确保驱逐不会添加新模型。有限保留性确保任何被额外移除的模型都是有限可表示性所必需的。均匀性同样消除对句法和无关模型结构的敏感性。

有限性要求通过极大可有限表示子集处理。给定期望的剩余模型集合 $\mathrm{mod}(B) \setminus \mathbb{M}$mod(B)∖M，框架定义

$$\mathrm{MaxFRSubs}(\mathrm{mod}(B) \setminus \mathbb{M}, \Lambda)$$MaxFRSubs(mod(B)∖M,Λ)

作为包含于 $\mathrm{mod}(B) \setminus \mathbb{M}$mod(B)∖M 中的极大可有限表示子集族。一个理性驱逐算子从该族中选择一个成员：

$$\mathrm{mod}(\mathsf{evc}(B,\mathbb{M})) \in \mathrm{MaxFRSubs}(\mathrm{mod}(B) \setminus \mathbb{M}, \Lambda).$$mod(evc(B,M))∈MaxFRSubs(mod(B)∖M,Λ).

如果该族为空，则对于给定模型类不存在理性驱逐算子。对于每个可接受输入，该族都非空的类称为驱逐兼容。在这类中，极大选择驱逐算子通过在极大可有限表示结果中选择来实现理性驱逐。

框架将模型修订引入为更强操作。修订接收一个基 $B$B 和两个不相交模型集合：要添加的模型集合 $\mathbb{M}^+$M+，以及要移除的模型集合 $\mathbb{M}^-$M−。结果记作 $\mathsf{rev}(B,\mathbb{M}^+,\mathbb{M}^-)$rev(B,M+,M−)。此操作不能通过简单组合接纳和驱逐实现，因为接纳可能重新引入修订要求移除的模型，而驱逐可能删除添加 $\mathbb{M}^+$M+ 所需模型。因此，修订直接在模型集合对上定义。

第一个要求是成功性：

$$\mathbb{M}^+ \subseteq \mathrm{mod}(\mathsf{rev}(B,\mathbb{M}^+,\mathbb{M}^-))$$M+⊆mod(rev(B,M+,M−))

以及

$$\mathbb{M}^- \cap \mathrm{mod}(\mathsf{rev}(B,\mathbb{M}^+,\mathbb{M}^-)) = \varnothing.$$M−∩mod(rev(B,M+,M−))=∅.

即使 $\mathbb{M}^+$M+ 与 $\mathbb{M}^-$M− 不相交，成功性也可能失败。当逻辑在语义上将不同模型等同，例如通过互仿真闭包，就会发生这种情况。在这种情况下，任何满足一个模型的基也必须满足修订本应排除的模型。因此，框架将关注范围限制在修订可实现类上，在其中要求添加和移除并不内在地矛盾。

最小变更由额外公设刻画。空洞扩展指出，如果 $\mathbb{M}^+$M+ 中的所有模型已经满足 $B$B，则修订应仅移除模型，不应添加任何新内容。空洞移除指出，如果 $\mathbb{M}^-$M− 中的所有模型已经违反 $B$B，则修订应仅添加模型，不应移除 $B$B 的任何模型。惰性结合两者：如果 $\mathbb{M}^+$M+ 已被接受且 $\mathbb{M}^-$M− 已被拒绝，则基应保持不变。

更强的最小性原则是审慎性，用于控制为实现有限可表示性而需要额外添加或移除的情形。它指出，如果移除额外模型集合 $X^-$X− 并添加额外模型集合 $X^+$X+，产生一个可有限表示的修订候选，则任何更小的候选都必须不是可有限表示的。换言之，额外变更必须不可省略。当存在更保守的可有限表示结果时，框架使用该原则排除那些丢弃或获取不必要模型的修订。

算子构造使用已经满足基本添加与移除约束的候选模型集合。对于一个满足系统 $\Lambda$Λ，定义

$$\chi_\Lambda(\mathbb{M}^+,\mathbb{M}^-) = \{Y \in \mathrm{FR}(\Lambda) \mid \mathbb{M}^+ \subseteq Y \text{ and } \mathbb{M}^- \cap Y = \varnothing\}.$$χΛ​(M+,M−)={Y∈FR(Λ)∣M+⊆Y and M−∩Y=∅}.

这是所有可有限表示模型集合的集合，它们接受 $\mathbb{M}^+$M+ 中的每个模型并拒绝 $\mathbb{M}^-$M− 中的每个模型。下一步是选择最接近原始基 $\mathrm{mod}(B)$mod(B) 的候选。

接近程度由对称差衡量。对于模型集合 $Y_1$Y1​、$Y_2$Y2​ 和参考集合 $\mathbb{M}$M，定义

$$Y_1 \preceq_{\mathbb{M}} Y_2 \quad\text{iff}\quad (\mathbb{M} \oplus Y_1) \subseteq (\mathbb{M} \oplus Y_2).$$Y1​⪯M​Y2​iff(M⊕Y1​)⊆(M⊕Y2​).

直观上，$Y_1 \preceq_{\mathbb{M}} Y_2$Y1​⪯M​Y2​ 表示将 $\mathbb{M}$M 变换为 $Y_1$Y1​ 所需的变更不多于将 $\mathbb{M}$M 变换为 $Y_2$Y2​。将其应用于 $\mathbb{M} = \mathrm{mod}(B)$M=mod(B)，可得到 $\chi_\Lambda(\mathbb{M}^+,\mathbb{M}^-)$χΛ​(M+,M−) 中候选上的一个排序。朴素关系型修订算子从该族中选择一个极小候选。这体现了审慎性，但仍可能违反空洞扩展或空洞移除。

完整的对称差分修订算子通过上下文相关约束强化选择。如果 $\mathbb{M}^+ \subseteq \mathrm{mod}(B)$M+⊆mod(B)，算子不得添加模型，因此它将 $B$B 的每个反模型视为一个需要额外移除的模型。这表示为从

$$\chi_\Lambda(\mathbb{M}^+, \mathbb{M}^- \cup (\mathfrak{M} \setminus \mathrm{mod}(B))).$$χΛ​(M+,M−∪(M∖mod(B))).

中选择。

如果 $\mathbb{M}^+ \not\subseteq \mathrm{mod}(B)$M+⊆mod(B) 但 $\mathbb{M}^- \cap \mathrm{mod}(B) = \varnothing$M−∩mod(B)=∅，算子不得移除模型，因此它将 $B$B 的每个模型视为一个需要额外添加的模型。这表示为从

$$\chi_\Lambda(\mathbb{M}^+ \cup \mathrm{mod}(B), \mathbb{M}^-).$$χΛ​(M+∪mod(B),M−).

中选择。

在剩余的混合情形中，算子从

$$\chi_\Lambda(\mathbb{M}^+,\mathbb{M}^-).$$χΛ​(M+,M−).

中选择一个极小候选。

形式上，结果是一个满足以下条件的模型集合 $\mathbb{M}$M：

$$\mathbb{M} \in \min_{\preceq_{\mathrm{mod}(B)}} \chi_\Lambda(\mathbb{M}^+,\mathbb{M}^- \cup (\mathfrak{M} \setminus \mathrm{mod}(B)))$$M∈⪯mod(B)​min​χΛ​(M+,M−∪(M∖mod(B)))

当 $\mathbb{M}^+ \subseteq \mathrm{mod}(B)$M+⊆mod(B) 时；

$$\mathbb{M} \in \min_{\preceq_{\mathrm{mod}(B)}} \chi_\Lambda(\mathbb{M}^+ \cup \mathrm{mod}(B), \mathbb{M}^-)$$M∈⪯mod(B)​min​χΛ​(M+∪mod(B),M−)

当 $\mathbb{M}^+ \not\subseteq \mathrm{mod}(B)$M+⊆mod(B) 且 $\mathbb{M}^- \cap \mathrm{mod}(B) = \varnothing$M−∩mod(B)=∅ 时；否则

$$\mathbb{M} \in \min_{\preceq_{\mathrm{mod}(B)}} \chi_\Lambda(\mathbb{M}^+,\mathbb{M}^-).$$M∈⪯mod(B)​min​χΛ​(M+,M−).

该构造的设计确保空洞扩展、空洞移除和审慎性均得到保持。所得到的对称差分修订算子恰好是满足修订核心合理性原则的那些算子。

该设计也将修订与两个原语操作关联。如果一个模型对的二元类是可分解的，即对于每个对 $(\mathbb{M}^+,\mathbb{M}^-)$(M+,M−) 也包含 $(\mathbb{M}^+,\varnothing)$(M+,∅) 和 $(\varnothing,\mathbb{M}^-)$(∅,M−)，则正分量构成一个接纳候选类，负分量构成一个驱逐候选类。修订在此类可分解类上的兼容性意味着接纳在添加侧的兼容性以及驱逐在移除侧的兼容性。反过来，理性接纳算子和理性驱逐算子会在对应的添加为空或移除为空情形上诱导理性修订算子。

对于描述逻辑概念学习，框架将满足系统特化为 EL$_\perp$⊥​ 概念或 ALC 概念的语义。一般方法要求所选模型对二元类是修订兼容的。在某些设定中，即使是有限树形带点解释，也不足以确保 EL$_\perp$⊥​ 和 ALC 概念满足系统的修订兼容性。对于 ALC，当所考虑的模型集合在有限签名上对互仿真封闭时，可得到正向兼容性结果。此限制使该逻辑的语义边界与修订算子使用的候选模型集合一致，从而在保持必需添加与移除约束的同时，可以选择可有限表示的结果。

实验

实验评估基于 EL⊥ 和 ALC 描述逻辑概念、在带点解释上的满足系统的驱逐与接纳兼容性。结果显示，EL⊥ 概念是驱逐兼容的，并在限制为有限树形带点解释集合时成为接纳兼容，而普通 EL 和 ALC 不满足驱逐兼容性。在许多树形或有限签名限制下，EL⊥ 和 ALC 的接纳兼容性更广泛地失败，其中 ALC 只有在对模型集合和签名都施加强有限性假设时才实现兼容。

对于扩展了 bottom 的 EL 概念，驱逐兼容性成立，而接纳兼容性通常不成立。将模型限制为有限树形带点解释可恢复该系统的接纳兼容性。对于 ALC 概念，两种性质通常都不成立，只有在有限签名上施加更强的有限性和树形限制时才成立。带 bottom 的 EL 是驱逐兼容的，但通常不是接纳兼容的。有限树形模型使带 bottom 的 EL 具备接纳兼容性。在缺少强模型限制时，ALC 概念既不驱逐兼容，也不接纳兼容。组合有限、树形和有限签名限制可恢复 ALC 的两种性质。

实验评估描述逻辑概念扩展的驱逐与接纳兼容性。结果显示，带 bottom 的 EL 是驱逐兼容的，而接纳兼容性需要有限树形带点模型。对于 ALC 概念，两种兼容性在缺乏强限制时都失败，只有在组合有限、树形和有限签名条件下才恢复。