离散数学中的归结原理

简介：
《离散数学中的归结原理》一文深入探讨了在离散数学框架下，通过逻辑推演实现定理证明的方法，特别是自动推理技术中归结法的应用与理论基础。 归结原理是一种推理规则，在谓词公式转化为子句集的过程中显得尤为重要。在这个转化过程中，可以观察到在生成的子句集中，各个子句之间的关系是合取（即逻辑与）。这意味着如果其中任何一个子句不可满足，则整个集合就不可满足。此外，若一个子句集中包含空子句，则这个子句集一定也是不满足条件的。 归结原理正是基于上述观察而提出的：当有两个命题P->Q和Q->R时，可以得出结论P->R。从逻辑的角度来看，P->Q等同于￢P∨Q（即如果非P则为真），同样地，Q->R等价于￢Q∨R。 因此，在这种情况下，归结原理实质上是将共同的元素合并的过程：比如对于两个子句 P∨{∑1} 和 ￢P∨{∑2} ，它们可以被归约为 {∑1}∨{∑2}。这里的 ∑1, ∑2 表示文字集合（即命题变量或其否定形式）。