《归结演绎推理》PPT课件

《《归结演绎推理》PPT课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、1第4章自动推理2第4章自动推理4.1引言4.2自然演绎推理4.3归结演绎推理-134.3归结演绎推理-14归结证明过程是一种反驳程序，即：不是证明一个公式是有效的(valid)，而是证明公式之非是不可满足的(dissatisfiable)。这完全是为了方便，并且不失一般性。埃尔布朗(Herbrand)(也称海明伦)提出的埃尔布朗论域和埃尔布朗定理为自动定理证明奠定了理论基础。鲁宾逊(Robinson)原理使定理证明的机械化变为现实。4.3归结演绎推理-15若欲证明前提条件P可推导出结论Q，即证明永真，该问题的证明等价

2、于证明永假，即是不可满足的。4.3归结演绎推理-16由于谓词逻辑是命题逻辑的推广，命题逻辑中的基本等价式和推理规则在谓词逻辑仍可沿用。但由于谓词逻辑中引入了变量及量词，须再增加一些与变量、量词有关的一些定理和规则，现一并归纳于下:4.3.1Skolem标准型7双重否定律(doublenegationlaw):┓(┓P(x))≡P(x)德·摩根定律(Mogenlaw):┓(P(x)∨Q(x))≡┓P(x)∧┓Q(x)┓(P(x)∧Q(x))≡┓P(x)∨┓Q(x)1、谓词演算的基本等价式8逆否律(inverse-nega

3、tionlaw):P(x)→Q(x)≡┓Q(x)→┓P(x)分配律(assignmentlaw):P(x)∧(Q(x)∨R(x))≡(P(x)∧Q(x))∨(P(x)∧R(x))P(x)∨(Q(x)∧R(x))≡(P(x)∨Q(x))∧(P(x)∨R(x))1、谓词演算的基本等价式9结合律(associationlaw):（P(x)∧Q(x))∧R(x)≡P(x)∧(Q(x)∧R(x))（P(x)∨Q(x))∨R(x)≡P(x)∨(Q(x)∨R(x))蕴含等价式(implicationlaw):P(x)→Q(x)≡┓P

4、(x)∨Q(x)1、谓词演算的基本等价式10易名规则(renamelaw):xP(x)∨xQ(x)≡xP(x)∨yQ(y)量词转换律(quantifiertransformlaw):┓xP(x)≡x┓P(x)┓xP(x)≡x┓P(x)1、谓词演算的基本等价式11量词分配律(quantifierassignmentlaw):x(P(x)∨Q(x))≡xP(x)∨xQ(x)x(P(x)∧Q(x))≡xP(x)∧xQ(x)x(P→Q(x))≡P→xQ(x)x(P→Q(x))≡P→xQ(x)

5、1、谓词演算的基本等价式12量词交换律(quantifiercommutativelaw):xy(P(x,y))≡yx(P(x,y))xy(P(x,y))≡yx(P(x,y))xy(P(x,y))yx(P(x,y))xy(P(x,y))yx(P(x,y))1、谓词演算的基本等价式13量词辖域变换等价式:xP(x)∨Q≡x(P(x)∨Q)xP(x)∧Q≡x(P(x)∨Q)xP(x)∧Q≡x(P(x)∨Q)xP(x)∧Q≡x(P(x)∨Q)Q中不含变量1、谓词演算的基本等

6、价式14全称量词消去规则:xP(x)≡P(y)全称量词引入规则:P(y)≡xP(x)存在量词消去规则:xQ(x)≡Q(c)(c为常量)存在量词引人规则:Q(c)≡xQ(x)2、量词消去及引入规则15有限域量词消去规则:设有限个体域为Dd1，d2，……dnxP(x)≡P(d1)∧P(d2)，……∧P(dn)xQ(x)≡Q(d1)∨Q(d2)，……∨Q(dn)2、量词消去及引入规则163、谓词逻辑中的范式同一个命题或谓词公式可以用不同的命题或谓词公式形式来表达，这些公式形式之间是相互等值的。为了把这些公式规范

7、化，下面讨论公式范式问题。所谓范式就是公式的标准形式，公式往往可以转换为和它等价的范式，以便对它们做一般性的处理。方法是：对给定公式中的某子公式用与它“等价”的一个公式来代替，并且重复该过程直到得出所需要的形式为止。下面给出一些定义。17范式中的一些定义:定义4.1文字(literal)是原子或原子之非。定义4.2公式G，当且仅当G有形式G1∧…∧Gn(n>=1)其中每个Gi都是文字的析取式。则G称为合取范式(conjunctivenormalform)3、谓词逻辑中的范式18定义4.3公式G称为析取范式(disjun

8、ctivenormalform)，逻辑公式的标准化(或规范化)，它是合取子句的析取.当且仅当G有形式G1∨…∨Gn(n>=1)其中每个Gi都是文字的合取式。例如:在命题逻辑中，若P、Q、R是原子，则P、Q、R、┓P、┓Q、┓R都是文字。(P∨┓Q∨R)∧(┓P∨Q)是合取范式。(┓P∧Q)∨(P∧┓Q∧┓R)是析取范式。3、谓词逻