非单调推理 · aiwiki.page

非单调推理是一种推理方式：新增信息可能使先前有依据的结论失效，而不必撤回原有前提。它将暂定推理形式化：根据对通常情形、未知信息或优先考虑的可能性的假设，接受相应结论。这一研究主题在人工智能的知识表示与推理中占据核心地位，尤其涉及不完整知识和带有例外的规则的表示。它涵盖多种不同的逻辑框架，而不是一套普遍认可的演算体系。(sciencedirect.com)

单调性与可撤销结论

在经典逻辑中，逻辑后承具有单调性。如果前提集 $\Gamma$ 能推出命题 $\varphi$ ，那么增加前提后，这一推导关系仍然成立：

\Gamma\vdash\varphi \quad\Longrightarrow\quad \Gamma\cup\Delta\vdash\varphi.

非单调后承关系通常记作 $\mathrel{\sim}$ ，不一定满足这一条件。对于某些命题，可能出现以下情况：

\Gamma\mathrel{\sim}\varphi, \qquad \Gamma\cup\Delta\not\mathrel{\sim}\varphi.

“非单调”意味着后承关系有可能因新增信息而不再成立，并不意味着每次增加信息都会改变结论。(u.cs.biu.ac.il)

一个常见例子涉及鸟与飞行。假设知识库中记载了崔蒂是一只鸟，以及鸟通常会飞，那么系统可以暂时得出崔蒂会飞的结论。得知崔蒂是一只企鹅后，这一结论就被推翻了，但崔蒂是一只鸟这一事实仍然保留。仅仅撤回“崔蒂会飞”并不等于推导出它的否定；后者需要额外依据，例如企鹅不会飞的规则。这体现了可撤销推理：一项推断即使有依据，也仍然可能被推翻。(u.cs.biu.ac.il)

历史发展

这一领域源于在计算机程序中表示常识推理的尝试。乔恩·多伊尔在1979年关于真值维护系统的研究中，描述了记录信念依据并修正依赖于假设的结论的机制。1980年，雷蒙德·赖特提出了缺省逻辑，约翰·麦卡锡则发表了限界理论，由此确立了两种颇具影响力的形式化非单调推理方法。(sciencedirect.com)

罗伯特·C. 穆尔于1985年对自认知逻辑的研究，将智能体针对自身信念的推理形式化。迈克尔·格尔方德和弗拉基米尔·利夫希茨于1988年提出了逻辑程序的稳定模型语义。1990年，萨里特·克劳斯、丹尼尔·莱曼和梅纳赫姆·马吉多尔系统研究了非单调后承关系与优先模型，这项研究通常被称为 KLM框架。这些进展将基于规则、认知和模型论的方法联系起来，但并未使它们的语义变得相同。(sciencedirect.com)

主要框架

缺省逻辑

缺省逻辑在普通背景陈述之外，增加了适用性取决于一致性的规则。在赖特的记法中，缺省规则具有以下形式：

\frac{\alpha:\beta_1,\ldots,\beta_n}{\gamma}.

其中，前提条件为 $\alpha$ ，合理性依据为 $\beta_1,\ldots,\beta_n$ ，结论为 $\gamma$ 。大致而言，当 $\alpha$ 已经成立，且这些合理性依据与最终形成的信念集合保持一致时，该规则便允许推出 $\gamma$ 。因此，判断规则是否适用，并不只是检查它是否与初始事实相容。(sciencedirect.com)

例如，

\frac{\operatorname{Bird}(x):\operatorname{Flies}(x)} {\operatorname{Flies}(x)}

表达了一条缺省规则：鸟会飞，除非这一假定受到反驳。一个缺省理论可能有多个扩展，即由其事实和缺省规则生成的、彼此不同且各自保持一致的结论集。有些理论则没有扩展。这些可能性使得扩展的选择以及相互冲突的缺省规则的处理成为语义的一部分。(sciencedirect.com)

限界

限界通过在理论的模型中最小化选定的谓词来表示缺省假设。例如，一条规则可以规定：鸟会飞，除非它们在相关方面存在异常：

\operatorname{Bird}(x)\land \neg\operatorname{Abnormal}(x) \rightarrow\operatorname{Flies}(x).

最小化异常谓词，意味着优先选择例外尽可能少、同时又符合显式信息的解释。新增事实可能迫使系统承认某些例外，并改变优先模型所支持的结论。(www-formal.stanford.edu)

具体设定十分重要：限界必须明确哪些部分需要最小化、哪些部分保持固定，以及哪些部分可以变化。麦卡锡在1986年的表述中进一步细化了这些区分，并将最小化应用于继承层次结构和行动推理。因此，限界改变的是哪些模型被视为相关模型，而不是仅仅在原有后承关系不变的情况下，增加一些能处理例外的规则。(www-formal.stanford.edu)

自认知逻辑

自认知逻辑研究智能体对自身信念的推理。它使用一个通常记作 $L$ 的信念算子，其中 $L\varphi$ 表示智能体相信 $\varphi$ 。例如，公式

\operatorname{Bird}(t)\land \neg L\neg\operatorname{Flies}(t) \rightarrow\operatorname{Flies}(t)

表达了一条认知层面的缺省规则：如果 $t$ 是一只鸟，且智能体不相信 $t$ 不会飞，就得出它会飞的结论。缺少某种信念，与明确相信相反命题，是两回事。这一逻辑的语义采用稳定展开，使理论与有关智能体相信什么、不相信什么的假设相协调。(sciencedirect.com)

逻辑编程与稳定模型

逻辑编程为非单调推理提供了另一种环境。规则中可以包含失败即否定，其示意形式如下：

flies(X) :- bird(X), not abnormal(X).

表达式 not abnormal(X) 是缺省否定，而不是普通的经典否定断言。处理它需要针对整个程序的语义。(cs.utexas.edu)

在稳定模型语义中，候选原子集合 $M$ 决定了一个约简。对于有限的基正常程序，先删除所有包含如下条件的规则：该条件是对属于 $M$ 的原子的缺省否定；然后，擦除剩余规则中的缺省否定条件。如果候选集合恰好等于所得正程序的最小模型，它就是稳定的。一个程序可能没有稳定模型，也可能有一个或多个稳定模型。这一语义是回答集编程的基础，后者是一种处理知识密集型搜索问题的声明式方法。(cs.utexas.edu)

优先后承关系

优先语义在与前提相容的情形中，选取最优先或最正常的情形来评估结论。条件式

\alpha\mathrel{\sim}\beta

在相关的优先 $\alpha$ 情形均满足 $\beta$ 时成立。新增信息可能改变哪些情形具有优先地位，从而推翻先前的结论。KLM框架将语义模型条件与推理的结构性质联系起来。它区分了多个后承关系族，而不是认为只要不满足单调性，就足以刻画推理行为。(sciencedirect.com)

不同结论与受控推理

当一个理论允许存在多个扩展、展开或稳定模型时，可以采用两种重要的推理策略：

轻信推理：只要一个命题属于至少一种可接受结果，就接受它。
怀疑推理：只有一个命题属于每一种可接受结果，才接受它。

这两种策略回答的是不同的问题：一个结论是否得到某种自洽解释的支持，或者它是否在所有这类解释下都成立。对于不存在可接受结果的情况，需要作出明确约定，因为对空集进行全称量化，否则可能导致命题被空泛地接受。(academic.oup.com)

放弃单调性并不意味着必须放弃所有结构性约束。KLM式系统研究诸如谨慎单调性之类的性质：如果 $\alpha$ 同时支持 $\beta$ 和 $\gamma$ ，那么显式加入已经接受的结论 $\beta$ 后，仍应保留 $\gamma$ 。这一性质与相应的切割性质共同支持累积性：将已接受的结论显式加入前提，不会改变结论。这类原则将受控的可撤销推理与任意的信念变化区分开来。(u.cs.biu.ac.il)

应用与实现

非单调推理可以将日常预期形式化，而不必列举所有可能的例外。其中一个应用是框架问题，即表示某个行动之后哪些事物保持不变。持续不变可以作为缺省假设处理，而关于行动效果的信息则可以覆盖这一假设。另一个应用是资格问题：某个行动能否成功，可能取决于数量不定、未被明说的条件。缺省规则允许假定通常的条件成立，而不必将这些条件视为毫无例外的事实。(www-formal.stanford.edu)

回答集编程将这些思想发展成一种计算范式。问题通过规则和约束来描述，解则由回答集表示。其求解器机制借鉴了与布尔可满足性问题相关的技术，而不是简单地按规则的书写顺序逐条执行。真值维护系统则处理一个互补的实现问题：保留结论的依据，以便修正并解释那些依赖于已被推翻的假设的结论。(cs.utexas.edu)

局限与语义选择

非单调推理并不能唯一确定哪些缺省规则应当优先。不同的形式体系对一致性、正常性、无知以及可接受的信念状态作出了不同承诺。即使关系密切的缺省逻辑与自认知逻辑方法，也使用不同的语义算子；因此，两者之间的转换必须保留指定的后承概念，而不能只是复现外观相似的规则。(arxiv.org)

表示方式的选择也会影响结果。选择哪些谓词进行最小化、允许哪些特定假设，或者采用怀疑推理而非轻信推理，都可能改变所能得出的结论。要解释系统的结论，就必须记录这些选择：缺省结论的支持是相对于其形式化假设而言的，并不保证它在所有情形下都为真。(www-formal.stanford.edu)

计算复杂性是另一项局限。对于不加限制的命题赖特缺省逻辑，判定是否存在扩展，以及判定某个命题是否属于至少一个扩展，都是 $\Sigma_2^P$ 完全问题；判定某个命题是否属于每一个扩展，则是 $\Pi_2^P$ 完全问题。这些是针对特定推理任务的最坏情况结果，并不是对所有非单调系统的统一复杂性分类。它们表明，选择自洽假设的难度可能超过普通命题逻辑后承检验的难度。(academic.oup.com)

参考来源

Circumscriptionwww-formal.stanford.edu
Semantical Considerations on Nonmonotonic Logiciiif.library.cmu.edu
Vladimir Lifschitz: Selected Papers Published before 1996cs.utexas.edu
Nonmonotonic Reasoning, Preferential Models and Cumulative Logicsu.cs.biu.ac.il
Applications of Circumscription to Formalizing Common Sensewww-formal.stanford.edu
Applications of Circumscription to Formalizing Common Sense Knowledgewww-formal.stanford.edu
Thirteen Definitions of a Stable Modelcs.utexas.edu
What Is Answer Set Programming?cs.utexas.edu