离散数学第四章谓词演算的推理理论-假设推理系统.ppt
《离散数学第四章谓词演算的推理理论-假设推理系统.ppt》由会员分享,可在线阅读,更多相关《离散数学第四章谓词演算的推理理论-假设推理系统.ppt(20页珍藏版)》请在三一办公上搜索。
1、第四章 谓词演算的推理理论,4.1 谓词演算的永真推理系统 4.2谓词演算的假设推理系统 4.2.1 假设推理系统的组成及证明方法 4.2.2 推理过程的推导过程4.3谓词演算的归结推理系统,一、假设推理系统的组成,(附加前提证明法)如果,AB,则(AB),也可表示为:如果A1,A2,An,AB,则A1,A2,An(AB)。依次类推可得定理:(A1(A2(An(AB),(2)存在推理定理,如果有 A1,An,xP(x),P(e)Q,其中Q中不含有自由的e,且在推理过程中不对假设中的自由变元和额外假设中的自由变元实施全规则和存在规则,则有:A1,A2,An,xP(x)Q,去“存在量词”,二、假设
2、推理过程的证明方法,(1)把待证公式的前件作为假设一一列出,假设中的全称量词可用全称量词消去规则消去,存在量词可引入额外假设删除,并在式子后注明它为额外假设。,二、假设推理过程的证明方法,(2)按永真的证明方法进行证明,但此时不能对假设实施代入。(3)待证公式的后件中若有全称量词,可用全0规则引入,存在量词可由公理21引入。,全称量词消去规则,规则成立的条件:(1)t是任意个体变项或常项。,例 考察xyF(x,y)全称量词消去能不能得到下式:y F(y,y),存在量词消去规则,规则成立的条件:(1)c是使A(c)为真的特定的个体常元。(2)xA(x)是闭式。,例 考察yF(x,y)存在量词消去
3、能不能得到下式:F(x,c),全称量词引入规则,规则成立的条件:(1)A(t)在任何解释I及I中对t的任何赋值下均为真。(2)x不在A(t)中约束出现。,存在量词引入规则,规则成立的条件:(1)c是特定的个体常元。(2)x不在A(c)中出现。,第四章 谓词演算的推理理论,4.1 谓词演算的永真推理系统 4.2谓词演算的假设推理系统 4.2.1 假设推理系统的组成及证明方法 4.2.2 推理过程的推导过程4.3谓词演算的归结推理系统,例 求证苏格拉底三段论,凡人要死,苏格拉底是人,所以苏格拉底要死。,解:P(e):e是人 D(e):e要死a:苏格拉底(1)x(P(x)D(x)假设(2)P(a)假
4、设(3)P(a)D(a)全称量词消去规则(4)D(a)(2)(3)分离由存在推理定理得:x(P(x)Q(x),P(a)Q(a)由假设推理定理得:x(P(x)D(x)(P(a)D(a),例 下面推理是否正确?,设前提为xyF(x,y),(1)xyF(x,y)前提引入(2)y F(y,y)全称量词消去解 推理并不正确。如果给定解释I:个体域为实数集,F(x,y):xy。则 xyF(x,y)意为“对于每个实数x,均存在着比之更小的实数y”,这是一个真命题。而yF(y,y)意为“存在着比自己小的实数”,是假命题。之所以出现这样的错误,是因为yF(x,y)中有1个自由变元x,而y F(y,y)中无自由变
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 离散数学 第四 谓词演算 推理 理论 假设 系统
链接地址:https://www.31ppt.com/p-6010502.html