一阶逻辑线性归结原理：子句集可满足性判定及与输入归结不完备性的关联

咱们先把问题拆成两部分来拆解：线性归结如何处理可满足性判定，以及它和输入归结不完备性的内在关联。

一、线性归结判定可满足性的核心逻辑 #

首先得明确：线性归结的核心特性是反驳完备——也就是说，只要子句集是不可满足的，在命题逻辑场景下它一定能在有限步骤内推导出空子句；在一阶逻辑场景下，理论上存在这样的推导路径，但实际执行时可能陷入无限搜索。但要判定可满足性，得分两种情况来看：

1. 命题逻辑子句集 #

命题逻辑的子句数量是有限的，所有可能生成的归结式数量也有上限。当用线性归结推导时：

• 如果某一步推导出空子句，直接判定子句集不可满足；
• 如果遍历所有可能的线性归结路径后，再也生成不出新的归结式，且始终没得到空子句，那就能判定子句集可满足。此时你可以构造一个模型：给每个命题变元赋值，让所有原始子句和生成的归结式都为真，这样的赋值必然存在。

2. 一阶逻辑子句集 #

这里要受限于哥德尔一阶逻辑不可判定性定理——不存在能判定所有一阶子句集可满足性的通用算法，线性归结也不例外：

• 对于不可满足的一阶子句集，线性归结是反驳完备的，即存在推导序列能得到空子句，但实际执行时可能因搜索空间过大，无限循环找不到这条路径；
• 对于可满足的一阶子句集，线性归结可能会无限生成新的归结式，永远无法终止并给出“可满足”的结论。这时你无法区分是还没找到反驳路径，还是根本不存在反驳路径（即可满足）。

二、与输入归结不完备性的关联 #

先回顾输入归结：它是线性归结的一个子集，要求每次归结的两个子句中，至少有一个是原始子句集里的子句（不能是中间生成的归结式）。输入归结是反驳不完备的——举个经典例子：子句集 {P∨Q, ¬P∨Q, P∨¬Q, ¬P∨¬Q} 是不可满足的，但用输入归结根本推不出空子句。

这种不完备性和可满足性判定的关系体现在两点：

• 输入归结的不完备性意味着：即使子句集是不可满足的，它也可能找不到空子句。此时你无法判断是子句集真的可满足，还是输入归结本身能力不足。而线性归结作为更通用的形式，是反驳完备的，所以在命题逻辑下，只要线性归结终止且未得到空子句，就能确定子句集是可满足的；
• 但到了一阶逻辑层面，不管是输入归结还是线性归结，都绕不开逻辑本身的不可判定性。输入归结的不完备性是方法本身的能力缺陷，而线性归结无法判定所有可满足子句集是一阶逻辑的固有属性，二者是不同层面的问题。

内容的提问来源于stack exchange，提问作者Qwerto