3.2.2命题逻辑中的归结原理 ◆要证明在前提P下结论Q成立,即是证明P→Q永真, 这只须证明P∧_Q不可满足。根据定理1,只须证 明P∧Q的子句集不可满足。由于子句之间是合取 关系,只要有一个子句不可满足,则整个子句集不 可满足。由于空子句是不可满足的,所以如果子句一 集中包含空子句,则该子句集是不可满足的。若子 句集中不包含空子句,则可通过 Robinson提出的归 结原理对子句集进行归结,归结过程保证子句集的 不可满足性不变。一旦归结出空子句,则证明结束 因此,归结原理把定理的证明化为子句集中归结出 空子句的过程。3.2.2 命题逻辑中的归结原理 要证明在前提P下结论Q成立，即是证明P → Q永真， 这只须证明P  Q不可满足。根据定理1，只须证 明P  Q的子句集不可满足。由于子句之间是合取 关系，只要有一个子句不可满足，则整个子句集不 可满足。由于空子句是不可满足的，所以如果子句 集中包含空子句，则该子句集是不可满足的。若子 句集中不包含空子句，则可通过Robinson提出的归 结原理对子句集进行归结，归结过程保证子句集的 不可满足性不变。一旦归结出空子句，则证明结束。 因此，归结原理把定理的证明化为子句集中归结出 空子句的过程