chpt3分析.ppt

习题4 有以下知识： 约翰喜欢吃牛排，或者约翰喜欢吃土豆 如果约翰既喜欢吃牛排又喜欢吃土豆，那么约翰是一个不偏食的人 如果某人喜欢吃牛排，那么他喜欢吃土豆 如果某人喜欢吃土豆，那么他喜欢吃牛排 应用归结演绎推理方法证明：约翰是一个不偏食的人 * Herbrand定理只是从理论上给出证明子句集不可满足性的可行性和方法。但要在计算机上实现时非常困难的。 1965年，Robinson提出了归结原理，这是对自动推理的重大突破，使得机器定理证明变为现实。 * P→Q永真 P∧~Q不可满足 子句集S在D 上不可满足 子句集S在H 上不可满足 * 归结原理(1) 又称为消解原理，是Robinson提出的证明子句集不可满足性，从而实现了定理证明的一种理论和方法 子句集中各子句间的关系是合取关系，因此，只要有一个子句是不可满足的，则子句集就是不可满足的 空子句是不可满足的，因此只要子句集中包含一个空子句，则该子句集就是不可满足的 Robinson原理正是基于这一点提出的，基本思想是：检查子句集中是否有空子句，若有，则表明S是不可满足的；若没有，就在子句集中选择合适的子句对其进行归结推理，如果能推出空子句，就说明子句集S是不可满足的 * 归结原理(2) 那么什么是归结，如何进行归结推理？ 若P是原子谓词公式或原子命题，则称P与～P为互补文字。 * 命题逻辑中的归结原理 设C1与C2是子句集中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，则从C1和C2中可以分别消去L1和L2，并将二子句中余下的部分做析取构成一个新的子句C12，称这一过程为归结，所得到的子句C12称为C1和C2的归结式，而称C1和C2为C12的亲本子句。 例 * 上例中这一消去互补对的过程就是归结/没有互补对的两个子句没有归结式 归结过程就是一种推理规则，实际上归结原理就只有这样一条规则 为了说明归结原理的正确性，要证明C12为C1和C2的逻辑结论，即要证明C1∧C2→ C12。也就是要证明，使C1和C2为真的解释I，也必然使C12为真 证明：设I是使C1和C2为真的任意假设，若I下P为真，则~P为假；由于C2为真，则C2’为真；则C12为真。若I下P为假，由于C1为真，则C1’为真；则C12为真。得证。 定理6 归结式C12是其亲本子句C1和C2的逻辑结论。 * 推论： 设C1和C2是子句集S上的子句，C12是C1和C2的归结式。如果把C12加入子句集S后得到新子句集S1，则S1和S在不可满足的意义下是等价的。 即： S是不可满足的 = S1是不可满足的 命题逻辑中子句集S不可满足性的归结推理过程： 从子句集中选择一对亲本子句。 将选定的亲本子句归结成一个归结式。 若归结式为非空子句，将其加入子句集，转(1)步；若归结式为空子句，则归结结束。 * 例 证明子句集S={~P∨Q, ~Q，P}是不可满足的 证明： (1)~P ∨Q (2)~Q (3)P (4) ~P (1)和(2)进行归结 (5)NIL (3)和(4)进行归结 由于S中出现了空子句NIL，从而证明了S的不可满足性 * 在命题逻辑中，对不可满足的子句集S，归结原理是完备的. 即，如果子句集S是不可满足的，则必然存在一个从S到空子句的归结推理过程；反之，若存在一个从S到空子句NIL的归结推理过程，则S一定是不可满足的。 对于那些可满足的子句集S，使用归结推理规则将得不到任何结果 * 一阶谓词逻辑中的归结推理 首先使用合一置换的思想，对子句中的某些变元进行合一置换，对置换后的新子句再使用归结规则 设C1和C2是两个没有相同变元的子句，L1 和L2分别是C1 和C2的文字，如果L1与～ L2有mguμ，则把 C12 =( C1 μ －{L1 μ})∪(C2 μ －{L2 μ}) 称作子句C1 和C2的一个二元归结式，而L1 和L2是被归 结的文字。 * 例： 其中P(x)与~（~P(a)）存在mgu μ={a/x}， 则 * 在对谓词逻辑进行归结时，要注意以下几个问题： （1）若被归结的子句C1 和C2中具有相同的变元时，需要将其中一个子句的变元更名，否则可能无法做合一置换。从而没有办法进行归结。如C1=P(x), C2=P(f(x)), （2）在求归结式时，不能同时消去两个互补文字对，消去两个互补文字对所得的结果不是两个亲本子句的逻辑推论。 如C1=P∨Q， C2=~P∨~Q， （3）如果在参加归结的子句内含有可合一的文字，则在进行归结之前，应对这些文字进行合一，以实现这些子句内部的化简。 * 一般情况下，如果一个子句C的几个文字具有最一般的合一置换θ, 则称Cθ为子句C的因子。如果Cθ