第11讲谓词逻辑推理

《第11讲谓词逻辑推理》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、一阶逻辑永真式(tautology)永真式:在各种赋值下取值均为真(逻辑有效式)命题逻辑永真式:在各种赋值下取值均为真(重言式)永假式:在各种赋值下取值均为假(矛盾式)命题逻辑永假式:在各种赋值下取值均为假(矛盾式)可满足式：非永假式1一阶逻辑等值式(来源)命题逻辑等值式的代换实例与变项命名有关的换名规则代替规则与量词有关的有限个体域量词消去量词否定量词辖域收缩与扩张量词分配相同量词的交换2前束范式设φ为一谓词公式，如果φ具有如下形式：Q1x1Q2x2...QnxnB其中Qi(1≤i≤n)为或

2、，B为不含量词的公式，则称φ为前束范式3前束范式存在定理定理：任意一个谓词公式，都存在着一个等值的前束范式。(注：利用换名规则或代替规则以及上述所提及的等值式可知，任意公式都有其前束范式(存在性)，但并不唯一.)4例1xA(x,y)yB(y)xA(x,y)zB(z)xz(A(x,y)B(z))xA(x,y)∨zB(z)xA(x,y)∨zB(z)xz(A(x,y)∨B(z))xz(A(x,y)B(z))5一阶逻辑推理规则(定义)推出：AB读作：

3、A推出B含义：A为真时,B也为真AB当且仅当AB是永真式例如：xF(x)xF(x)F6一阶逻辑推理规则(来源)命题逻辑推理规则的代换实例基本等值式生成的推理规则其他的一阶逻辑推理规则xA(x)∨xB(x)x(A(x)∨B(x))x(A(x)∧B(x))xA(x)∧xB(x)x(A(x)→B(x))xA(x)→xB(x)x(A(x)→B(x))xA(x)→xB(x)7一阶逻辑推理规则(举例)命题逻辑推理规则的代换实例例如:假言推理规则:(A→B)∧AB代

4、入A=F(a),B=G(a),得到(F(a)→G(a))∧F(a)G(a)8一阶逻辑推理规则(举例、续)基本等值式生成的推理规则即由AB可得AB和BA例如:量词分配等值式:x(A(x)∧B(x))xA(x)∧xB(x)可得x(A(x)∧B(x))xA(x)∧xB(x)xA(x)∧xB(x)x(A(x)∧B(x))9一阶逻辑的常用推理规则前提引入、结论引入、置换规则假言推理、附加、化简、拒取式、假言三段论、析取三段论、构造性两难、合取引入US、UG、ES、EG104条

5、新的推理规则全称量词指定规则(US)全称量词引入规则(UG)存在量词指定规则(ES)存在量词引入规则(EG)11US规则(universalinstantiation)表示为xA(x)xA(x)————或————A(y)A(c)注意1:x,y是自由变项；c是个体常项注意2:在A中x不在y和y的辖域内自由出现注意3:被消去量词的辖域是整个公式例如(1)x(F(x)→G(x))前提引入(2)F(a)→G(a)(1)US12示例1设解释I为：个体域为全体整数集合，F(x,y)表示x>y(1

6、)xyF(x,y)前提引入(2)yF(y,y)(1)US此例错误的原因是违反注意213示例2(1)xF(x)→G(y)前提引入(2)F(y)→G(y)(1)US设解释I为：个体域为全体自然数集合，F(x)表示x是偶数，G(x)x是奇数此例错误的原因是违反注意314UG规则(universalgeneralization)表示为A(x)————xA(x)注意1:x是自由变项,且不在前提的任何公式中自由出现注意2:量词加在整个公式前面例如(1)F(x)→G(x)前提引入(2)x(F(x)

7、→G(x))(1)UG15示例3(1)F(x)→G(x)前提引入(2)F(x)前提引入(3)G(x)(1)(2)假言推理(4)xG(x)(3)UG设解释I为：个体域为全体整数集合，F(x)表示x是偶数，G(x)表示x可被2整除此例错误的原因是违反注意1，即在前提中x表示的是偶数，在推出的结论中仍用x则x表示全体整数，就变成x是偶数推出全体整数x能被2整除16示例4(1)F(x)→G(x)前提引入(2)F(x)→xG(x)(3)UG设解释I为：个体域为全体自然数集合，F(x)表示x是偶数，G(x

8、)x可被2整除此例违反注意2，正确推理为x（F(x)→G(x)）17ES规则(existentialinstantiation)表示为xA(x)————A(c)注意1:c是特定的满足A的个体常项且不在A(x)中出现注意2:被消去量词的辖域是整个公式注意3:A(x)中没有其他自由出现的变元例如(1)x(F(x)∧G(x))前提引入(2)F(a)∧G(a)(1)ES18示例5设解释I为：个体域为全体整数集合，F(x,y)表示x>y(1)xyF(x,y)前提引入(2)yF(