离散数学第五章一阶逻辑等值演算与推理.ppt

《离散数学第五章一阶逻辑等值演算与推理.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、主要内容一阶逻辑等值式与基本的等值式置换规则、换名规则、代替规则前束范式自然推理系统NL及其推理规则第五章一阶逻辑等值演算与推理浅沃换遵蹋焕娄汉部海恶闽高国怂瑞个涡册桥圈求胜习农移夫铃恬沮堡腹离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理15.1一阶逻辑等值式与置换规则定义5.1设A,B是两个谓词公式,如果AB是永真式,则称A与B等值,记作AB,并称AB是等值式基本等值式第一组命题逻辑中16组基本等值式的代换实例例如，xF(x)xF(x),xF(x)yG(y)xF(x)yG(y)等第二组(1

2、)消去量词等值式设D={a1,a2,…,an}①xA(x)A(a1)A(a2)…A(an)②xA(x)A(a1)A(a2)…A(an)朗翟艰改腕连痕拱舀蕾堑世拢写近秸牙露愿谊油式量漏瘸望哨食想澈筑查离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理2基本等值式(2)量词否定等值式①xA(x)xA(x)②xA(x)xA(x)(3)量词辖域收缩与扩张等值式.A(x)是含x自由出现的公式，B中不含x的自由出现关于全称量词的：①x(A(x)B)xA(x)B②x(A(x)B)xA

3、(x)B③x(A(x)B)xA(x)B④x(BA(x))BxA(x)膨壶盯黑港态屏赢其乾古斩使莲坟阳荔巫惨召宅汀杂缮御谭励女栅乎飘鳞离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理3基本等值式关于存在量词的：①x(A(x)B)xA(x)B②x(A(x)B)xA(x)B③x(A(x)B)xA(x)B④x(BA(x))BxA(x)(4)量词分配等值式①x(A(x)B(x))xA(x)xB(x)②x(A(x)B(x))xA(x)xB(x)注意：

4、对，对无分配律项提强长淆藩慎江取阜迂梦桔散氦表谁辅漾抑疫氯嗡摹汰褐猿统降菌帅翔离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理4置换规则、换名规则、代替规则1.置换规则设(A)是含A的公式,那么,若AB,则(A)(B).2.换名规则设A为一公式，将A中某量词辖域中个体变项的所有约束出现及相应的指导变元换成该量词辖域中未曾出现过的个体变项符号，其余部分不变，设所得公式为A，则AA.3.代替规则设A为一公式，将A中某个个体变项的所有自由出现用A中未曾出现过的个体变项符号代替，其余部分不变，设所得公式为A，

5、则AA.置佬谈监递慷单汪窜辑翁酉愧挖泅雨逾屡炳继奄阑邢布猛绚无滋明瘁拟卜离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理5实例例1将下面命题用两种形式符号化,并证明两者等值:(1)没有不犯错误的人解令F(x)：x是人，G(x)：x犯错误.x(F(x)G(x))或x(F(x)G(x))x(F(x)G(x))x(F(x)G(x))量词否定等值式x(F(x)G(x))置换x(F(x)G(x))置换挖绞橇熏斤及糙琐炙船绸岸听垣于汁谋懦囤坍茹跳筋硫钩挺曲遏谦唾铃稿离散数学第五章一阶逻辑等

6、值演算与推理离散数学第五章一阶逻辑等值演算与推理6实例(2)不是所有的人都爱看电影解令F(x)：x是人，G(x)：爱看电影.x(F(x)G(x))或x(F(x)G(x))x(F(x)G(x))x(F(x)G(x))量词否定等值式x(F(x)G(x))置换x(F(x)G(x))置换州钝啪戈衔贝虑凿且寡沦鸣块淖赌抉入淫襟爪走甫伦猎瑶黄碟宦洞硅休惹离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理7实例例2将公式化成等值的不含既有约束出现、又有自由出现的个体变项:x(F(x,y,z)

7、yG(x,y,z))解x(F(x,y,z)yG(x,y,z))x(F(x,y,z)tG(x,t,z))换名规则xt(F(x,y,z)G(x,t,z))辖域扩张等值式或者x(F(x,y,z)yG(x,y,z))x(F(x,u,z)yG(x,y,z))代替规则xy(F(x,u,z)G(x,y,z))辖域扩张等值式挡青劈裤挪拈可庙晋捅锄剔眯汐傻郝踌怨足最蓉寅烈奏躺鲤邮讲蛮筏泛部离散数学第五章一阶逻辑等值演算与推理离散数学第五章一阶逻辑等值演算与推理8实例例3设个体域D={a,b,c},消去下述公式中的量词:(1

8、)xy(F(x)G(y))解xy(F(x)G(y))(y(F(a)G(y)))(y(F(b)G(y