归结演绎推理

* (3)变量标准化：重新命名变元名，使不同量词约束的变元有不同的名字 (4)消去存在量词 存在量词不出现在全称量词的辖域内，此时只要用一个新的个体常量替换该存在量词的约束变元可消去存在量词 存在量词位于一个或多个全称量词的辖域内，如： 4.3.2 子句型 * 4.3.2 子句型 (5)将公式化为前束形: 把全称量词移到公式左边，并使每个量词的辖域包含这个量词后面的整个部分，所得的公式称为前束形. (6)把母式化为合取范式: 利用等价关系 ，把公式化为Skolem标准形。Skolem标准形的一般形式是 * (7)消去全称量词与合取词∧ 。 如P∧Q可表示为子句集: P Q (8)更改变量名，有时称为变量分离标准化。对变元更名，使不同子句中的变元不同名 4.3.2 子句型 * 例4.2 将合式公式化为子句形。 例题 * 解：(1)消去蕴涵符号： 这可以利用等价式： 得到： ?x[(~P(x)?[?y[~P(y) ?P(f(x,y))]?~?y[~Q(x,y) ?P(y)]]] (2)减少否定符号的辖域，把“ ”移到紧 靠谓词的位置上： 这可以利用下述等价式： 例题 * 得到： ?x[(~P(x)?[?y[~P(y) ?P(f(x,y))]??y[Q(x,y) ?~P(y)]]] (3)变量标准化：重新命名变元名，使不同量词约束的变元有不同的名字： ?x[~P(x)?[?y[~P(y)?P(f(x,y))]??w[Q(x,w) ?~P(w)]]] (4)消去存在量词： ?x[~P(x)?[?y[~P(y)?P(f(x,y))]?[Q(x,g(x)) ?~P(g(x))]]] 例题 * (5)化为前束形： ?x ?y[~P(x)?[ [~P(y)?P(f(x,y))]?[Q(x,g(x)) ?~P(g(x))]]] (6)把母式化为合取范式： ?x ?y[~P(x)? ~P(y)?P(f(x,y))]?[~P(x)? Q(x,g(x))] ? [~P(x)? ~P(g(x))] (7)消去全称量词和合取连接词： [~P(x)? ~P(y)?P(f(x,y))] [~P(x)? Q(x,g(x))] [~P(x)? ~P(g(x))] 例题 * (8)更改变量名，有时称为变量分离标准化。于是有： 必须指出: 一个子句内的文字可以含有变量，但这些变量总是被理解为全称量词量化了的变量。 例题 * 什么是子句?什么是子句集?请写出求谓词公式子句集的步骤. P144,习题4.4 作业 埃尔布朗定理 补充内容 * Thanks For Your Attention 下 课 中国矿大-中科院 智能信息处理联合实验室 * 中国矿大-中科院 智能信息处理联合实验室 * * 第4章 自动推理 * 第4章 自动推理 4.1 引言 4.2 自然演绎推理 4.3 归结演绎推理-1 * 4.3 归结演绎推理-1 * 归结证明过程是一种反驳程序，即：不是证明一个公式是有效的(valid)，而是证明公式之非是不可满足的(dissatisfiable)。这完全是为了方便，并且不失一般性。 埃尔布朗(Herbrand)(也称海明伦)提出的埃尔布朗论域和埃尔布朗定理为自动定理证明奠定了理论基础。鲁宾逊(Robinson)原理使定理证明的机械化变为现实。 4.3 归结演绎推理-1 * 若欲证明前提条件P可推导出结论Q，即证明 永真，该问题的证明等价于证明 永假，即 是不可满足的。 4.3 归结演绎推理-1 * 由于谓词逻辑是命题逻辑的推广，命题逻辑中的基本等价式和推理规则在谓词逻辑仍可沿用。但由于谓词逻辑中引入了变量及量词，须再增加一些与变量、量词有关的一些定理和规则，现一并归纳于下: 4.3.1 Skolem标准型 * 双重否定律(double negation law): ┓(┓P(x)) ≡P(x) 德·摩根定律(Mogen law): ┓(P(x)∨Q(x))≡ ┓P(x)∧ ┓Q(x) ┓(P(x)∧Q(x)) ≡ ┓P(x)∨ ┓Q(x