命题逻辑归结方法-Read.PPT

第 3 章 谓词逻辑和归结原理 命题逻辑的推理规则 推理规则是用一些命题公式A1, A2,… 推导出另外一些命题公式B1, B2,… 附加: A = A∨B 简化: A∧B =A 假言推理: A→B, A = A 拒取式: A→B, ┐ B = ┐ A 析取三段论: A∨B, ┐ A =B 假言三段论: A→B, B→C = A→C 命题逻辑的推理规则 例 1证明{(P?Q)，(P??R)， (S?T), (? S?R), ?T}?Q 1. S?T 前提引入 2. ?T 前提引入 3. ? S 1,2, 拒取规则 4. ? S?R 前提引入 5. R 3,4 假言推理 6. P? ? R 前提引入 7. ?P 5，6；拒取规则 8. P?Q 前提引入 9. Q 7,8, 析取三段论 命题逻辑的推理规则 写出对应下面推理的证明 如果今天下雨. 则要带伞或雨衣, 如果走路上班, 则不带雨衣,今天下雨,走路上班, 所以带伞. P:今天下雨 Q:带伞 R:带雨衣 S:走路上班 命题逻辑的推理规则 {P ? (Q∨R)，(S??R)， P, S}?Q 1. P ? (Q∨R) 前提引入 2. P 前提引入 3. Q∨R 1,2,假言推理 4. S??R 前提引入 5. S 前提引入 6. ? R 4,5,假言推理 7. Q 3,6, 析取三段论 命题逻辑归结方法 前面给出的命题逻辑的证明过程需要很多思考过程， 人可以用来实施推理，但却不适用于计算机。 本节我们介绍一中推理方法——归结方法，它以机械的方式实施推理， 容易使用计算机实现，我们先介绍它的简单情形，即命题逻辑的归结， 然后在下一节介绍谓词逻辑归结。 命题逻辑证明过程之所以复杂的一个重要原因是命题公式的形式是各种各样的。 证明系统必须有处理各种各样命题公式的能力。 为了简化命题公式的形式， 人们提出了一种简单而又有足够表达能力的形式，这就是子句。 命题逻辑归结方法 命题逻辑归结方法 一个命题逻辑公式可以采用如下方式转换成等价的子句的合取形式, 即合取范式： 1. 利用等价公式 P←→　Q =( P→Q)∧ (Q←P)和P→Q=~P∨Q删去公式中的←→　符号和→符号. 2. 利用De Morgan 律把所有的否定符号移到每个原子之前. 3. 利用分配律得到子句的合取形式 命题逻辑归结方法 例 把命题逻辑公式 ~ (~(P→Q) ∧(~ Q∨ R))转换成等价的子句的合取形式. ~ (~(P→Q) ∧(~ Q∨ R)) = ~ (~ (~P∨Q) ∧(~ Q∨ R)) = (~P∨Q) ∨~ (~ Q∨ R)) = (~P∨Q) ∨( Q∧~ R)) = (~P∨Q) ∧(~P∨Q∨~ R)) 上式即为子句的合取形式 命题逻辑归结方法 命题归结式 设　c1, c2是两个子句，　c1=L1∨D1, c2=L2∨D2 , 其中L1 =~ L2，　L1 ， L2也称作互补文字，　D1和D2 为子句．　则D1∨D2称作c1, c2的归结式， 记为R(c1, c2), c1, c2称做是归结式的亲本子句。 例如， 设　c1, c2是两个子句，　c1 = ~P∨Q, c2 = P∨R∨~ S, 则~P和P为互补文字, c1, c2的归结式是Q∨R∨~ S. 命题逻辑归结方法 在利用归结推导证明某一逻辑结果时，我们采用如下的归结反驳证明方法。设F ={f1, f2,…, fn}是命题逻辑公式集合， g 是命题逻辑公式，为了证明从 F能推导出 g， 我们先把逻辑公式f1, f2,…, fn转换成子句或子句集，把g 的否定～g 也转换成子句或子句集， 然后把这些子句放在一起， 组成一个子句集，在此子句集上应用归结， 把所得到的归结式不断地加入到子句集中， 继续进行归结，当子句集中包含空子句时，则认为是已经从F推导出g. 这种归结反驳证明的核心思想是反证法， 空子句表示矛盾。在证明过程中用□表示。如果把要证的结论的否定加入到前提集合中能导出矛盾， 则证明了该结论。理论上可以证明