L5谓词演算.ppt

Lu Chaojun, SJTU * 使用中的注意事项 多个量词下的量词消去与引入规则: (?x)(?y)?(x,y) ? (?y)?(x,y) 右端不能写成(?y)?(y,y) (?x)?(x,c) ? (?y)(?x)?(x,y) 右端不能写成(?x)(?x)?(x,x) (?x)(?y)?(x,y) ? (?y)?(x,y) ??(x,c) 但不能再反推出(?x)?(x,c)和(?y)(?x)?(x,y) 原因是(?x)(?y)?(x,y)成立时,对每个x所找到的y是依赖于x的,从而?(x,y)的成立是有条件的,不是对所有的x都有同一个y. Lu Chaojun, SJTU * 推理演算 在谓词逻辑里,真值表法不能使用,又不存在判明? →? 普遍有效的一般方法.从而使用推理规则的推理演算是谓词逻辑的基本推理方法. 推理演算过程: 首先将以自然语句表示的推理问题形式化表示 若不能直接使用基本的推理公式便消去量词,在无量词下使用规则和公式推理 最后再引入量词． Lu Chaojun, SJTU * 例:推理演算 前提: (?x)(P(x)→Q(x)),(?x)(Q(x)→R(x)) 结论: (?x)(P(x)→R(x)) 证明 (1) (?x)(P(x)→Q(x)) 前提 (2) P(x)→Q(x) ?消去 (3) (?x)(Q(x)→R(x)) 前提 (4) Q(x)→R(x) ?消去 (5) P(x)→R(x) (2),(4)三段论 (6) (?x)(P(x)→R(x)) ?引入 Lu Chaojun, SJTU * 例:推理演算(续) 人皆有死,苏格拉底是人,所以苏格拉底会死. 令P(x):x是人,Q(x):x会死.于是问题可改述为 (?x)(P(x)→Q(x)) ? P(Socrates) → Q(Socrates) 证明 (1) (?x)(P(x) → Q(x)) 前提 (2) P(x)→Q(x) ?消去 (3) P(Socrates) → Q(Socrates) 代入 (4) P(Socrates) 前提 (4) Q(Socrates) (3)(4)分离 Lu Chaojun, SJTU * 例:推理演算(续) 前提: (?x)P(x)→(?x)((P(x)?Q(x))→R(x)), (?x)P(x) 结论: (?x)(?y)(R(x)?R(y)) 证明 (1) (?x)P(x)→(?x)((P(x)?Q(x))→R(x)) 前提 (2) (?x)P(x) 前提 (3) (?x)((P(x)?Q(x))→R(x)) (1)(2)分离 (4) P(c) (2) ?消去 (5) (P(x)?Q(x))→R(x) (3) ?消去 (6) (P(c)?Q(c))→R(c) 代入 (7) P(c)?Q(c) (4) (8) R(c) (6)(7)分离 (9) (?x)R(x) (8) ?引入 (10) (?y)R(y) (8) ?引入 (11) (?x)R(x) ? (?y)R(y) (9)(10) (12) (?x)(?y)(R(x)?R(y)) (11)分配 Lu Chaojun, SJTU * 例:推理演算(续) 分析下面推理的正确性. (1) (?x)(?y)(x y) 前提 (2) (?y)(z y) ?消去 (3) z b ?消去 (4)(?z)(z b) ?引入 (5) b b ?消去 (6) (?x)(x x) ?引入 从(1)到(2),应记住y是依赖于z的. 从(2)到(3), b是依赖于z的. 从(3)到(4)不成立: 因为b是依赖于z的. 从(5)到(6)也错: 因为b是常项. Lu Chaojun, SJTU * 谓词逻辑的归结推理法 归结证明法可推广到谓词逻辑,证明过程同命题逻辑,只不过要考虑量词和个体变元带来的复杂性. 使用推理规则的推理演算灵活而技巧性强;归结法较为机械,容易使用计算机来 实现. Lu Chaojun, SJTU * 归结证明过程 (1)回忆:为证明? ? ? ,可等价地证明? ??? 是矛盾式. (2)建立? ??? 的子句集S 将G =? ???化成等值的