名词解释： 归结原理

为了证明子句集S的不可满足，只要对S中可进行归结的子句进行归结，并把归结式加入子句集S.得到新子句集S1，则S与S1在不可满足的意义上是等价的，归结原理的本质思想是去检查子句集S是否包含一个空子句•，如果S包含•，则S是不可满足的。
如果S不包含•，则去检查•是否可由S推导出来。
当然这个推理规则必须保证推出的子句是原亲本子句的逻辑结果。