1、,*,本资料仅供参考,不能作为科学依据。谢谢。本资料仅供参考,不能作为科学依据。感谢,数理逻辑,主讲,:,邱晓红,1/227,1,数理逻辑,介绍,数理逻辑是用数学方法研究形式逻辑科学。数学方法即符号方法,故数理逻辑又称符号逻辑。包含命题逻辑、谓词逻辑、证实论、模型论、递归函数、公理化集合论、归纳逻辑、模态逻辑、多值逻辑和时态逻辑等内容,与计算机有亲密关系。,2/227,2,各知识点关联图,3/227,3,第一部分:数理逻辑,第一章 命题逻辑,1.1,命题及其表示,1.2,逻辑联结词,1.3,命题公式与解释,1.4,真值表与等价公式,1.5,命题公式分类与蕴含式,1.6,其它逻辑联结词和最小功效
2、,完备联结词组,1.7,对偶与范式,1.8,推理理论,习 题 一,试验一 真值表程序计算,第,2,章 谓词逻辑,2.1,谓词基本概念,2.2,谓词公式与解释,2.3,变元约束,2.4谓词演算等价式与蕴含式,2.5谓词公式范式,2.6 谓词演算推理理论,习 题 二,试验二 命题逻辑简单推理系统,第3章 基于归结原理推理证实*,3.1谓词公式与子句集,3.2 海伯伦(HERBRAND)理论,3.3 归结原理(RESOLUTION METHOD),3.4 归结过程控制策略,习 题 三,试验三 归结原理程序实现,4/227,4,第一章:命题逻辑,主要内容:,命题及表示、联结词、命题公式与翻译、真值表与
3、等价公式、重言式与蕴涵式、其它联结词、对偶与范式、推理理论。,教学要求:,深刻了解和掌握命题逻辑中基本概念和基本方法。,重点:,命题逻辑中基本概念和基本推理方法,难点:,推理理论。,实践活动:,真值表程序计算,5/227,5,1.1,命题及其表示,定义,1.1.1,能够判断真假陈说句称为,命题,(,Proposition,)。命题判断结果称为命题,真值,,惯用,T,(True),(或,1,)表示,真,,,F,(False),(或,0,)表示,假,。真值为真命题称为,真命题,,真值为假命题称为,假命题,。,判定一个句子是否为命题要分为两步:一是判定是否为陈说句,二是能否判定真假,二者缺一不可。,
4、6/227,6,7/227,7,解,在上述十个句子中,(,2,)、(,9,)为祈使句,(,4,)为疑问句,(,5,)、(,6,)即使是陈说句,但(,5,)没有确定真值,其真假随,x,、,y,取值不一样而有改变,(,6,)是悖论,(Paradox),(即由真能推出假,由假也能推出真),因而(,2,)、(,4,)、(,5,)、(,6,)、(,9,)均不是命题。(,1,)、(,3,)、(,7,)、(,8,)、(,10,)都是命题,其中(,10,)即使现在无法判断真假,但伴随科技进步是能够判定真假。需要深入指出是,命题真假只要求它有就能够,而不要求马上给出。如例,1.1.1,(,8,),1+101=1
5、10,,它真假意义通常和上下文相关,看成为二进制加法时,它是真命题,不然为假命题,8/227,8,命题分类,命题标识符,依据命题结构形式,命题分为原子命题和复合命题。,定义,1.1.2,不能被分解为更简单陈说语句命题称为,原子命题,(Simple Proposition),。由两个或两个以上原子命题组合而成命题称为,复合命题,(Compound Proposition,),。,定义,1.1.3,表示原子命题符号称为,命题标识符,(Identifier),。,命题标识符依据表示命题情况,分为,命题常元,和,命题变元,。,9/227,9,1.2,逻辑联结词,一个复合命题,不论其组成多么复杂,普通都
6、能够分析出组成该命题原子命题。下面介绍,5,种惯用,逻辑联结词,(Logical Connectives),,分别是“非”(,否定联结词,)、“与”(,合取联结词,)、“或”(,析取联结词,)、“若,则,”,(,条件联结词,)、“,当且仅当,”,(,双条件联结词,),经过这些联结词能够把多个原子命题复合成一个复合命题。,10/227,10,1.2.1否定联结词,11/227,11,1.2.2,合取联结词,12/227,12,1.2.3,析取联结词,13/227,13,1.2.4,条件联结词,14/227,14,1.2.5,双条件联结词,15/227,15,1.2.6字位运算与布尔检索,16/2
7、27,16,17/227,17,1.3,命题公式与解释,上一节介绍了,5,种惯用逻辑联结词,利用这些逻辑联结词可将详细命题表示成符号化形式。对于较为复杂命题,需要由这,5,种逻辑联结词经过各种相互组合以得到其符号化形式,那么怎样组合形式才是正确、符合逻辑表示形式呢?,18/227,18,1.3.1,命题公式,19/227,19,1.3.2命题符号化,20/227,20,命题符号化范例,21/227,21,1.4,真值表与等价公式,22/227,22,真值表,23/227,23,真值表,范例,24/227,24,25/227,25,1.4.2,等价公式,26/227,26,27/227,27,1
8、.4.2.1,真值表法,28/227,28,12组惯用等价公式,29/227,29,1.4.2.2,等值演算法,30/227,30,31/227,31,32/227,32,33/227,33,34/227,34,35/227,35,36/227,36,1.5,命题公式分类与蕴含式,37/227,37,38/227,38,39/227,39,1.5.3,蕴含式,40/227,40,41/227,41,1.5.3.1,真值表法,42/227,42,1.5.3.2,等值演算法,43/227,43,1.5.3.3,分析法,44/227,44,1.6,其它逻辑联结词和最小功效完备联结词组,45/227,
9、45,46/227,46,1.6.1.2,与非联结词,(Nand)(),47/227,47,1.6.1.3,或非联结词,(Nor),(),48/227,48,49/227,49,1.6.2,最小功效完备联结词组,50/227,50,1.6.3,联结词逻辑电路表示,51/227,51,52/227,52,53/227,53,1.7,对偶与范式,54/227,54,1.7.1.2,对偶原理,(Duality Principle),55/227,55,56/227,56,1.7.2,命题公式范式,57/227,57,58/227,58,1.7.2.2,析取范式与合取范式,59/227,59,求公式范
10、式步骤,60/227,60,61/227,61,1.7.2.3,范式应用,62/227,62,1.7.3,命题公式主析取范式和主合取范式,63/227,63,64/227,64,65/227,65,66/227,66,67/227,67,(,2,)等值演算法,68/227,68,69/227,69,70/227,70,71/227,71,72/227,72,73/227,73,(,2,)等值演算法,74/227,74,75/227,75,1.7.3.3,主析取范式和主合取范式关系,76/227,76,77/227,77,78/227,78,1.7.3.4,主范式应用,79/227,79,(2)
11、,命题公式类型判定,80/227,80,81/227,81,(,3,)处理实际问题,82/227,82,1.8,推理理论,83/227,83,84/227,84,1.8.1,直接证法,85/227,85,86/227,86,87/227,87,88/227,88,89/227,89,1.8.2,间接证法,90/227,90,1.8.2.2,归谬法,91/227,91,习题课,92/227,92,93/227,93,提醒:,94/227,94,提醒,:,95/227,95,提醒,:,96/227,96,97/227,97,解,98/227,98,99/227,99,答案:,100/227,100
12、,101/227,101,102/227,102,103/227,103,解答,104/227,104,105/227,105,106/227,106,107/227,107,108/227,108,109/227,109,110/227,110,解,111/227,111,112/227,112,113/227,113,114/227,114,证实,115/227,115,116/227,116,试验一 真值表程序计算,117/227,117,118/227,118,第二章:谓词逻辑,主要内容:,谓词概念与表示、命题函数与量词、谓词公式与翻译、变量约束、谓词演算等价式与蕴涵式、前束范式、谓词
13、演算推理理论。,教学要求:,深刻了解和掌握谓词逻辑基本概念和基本推理方法。,重点:,谓词逻辑中基本概念和基本推理方法,难点:,谓词演算推理理论,。,实践活动:,命题逻辑简单推理系统,119/227,119,120/227,120,2.1,谓词基本概念,121/227,121,122/227,122,123/227,123,124/227,124,2.1.2,量词,125/227,125,126/227,126,2.2,谓词公式与解释,127/227,127,2.2.2,谓词公式解释,128/227,128,129/227,129,2.3,变元约束,130/227,130,131/227,131
14、,132/227,132,2.3.2,换名规则,133/227,133,134/227,134,2.3.3,代替规则,135/227,135,2.4,谓词演算等价式与蕴含式,136/227,136,137/227,137,138/227,138,2.4.2,谓词公式分类,139/227,139,140/227,140,141/227,141,142/227,142,2.4.3,谓词演算等价式,143/227,143,2.4.3.1,量词消去,144/227,144,145/227,145,2.4.3.2,量词与“”之间关系,146/227,146,2.4.3.3,量词作用域扩张与收缩,147/
15、227,147,148/227,148,2.4.3.4,量词与命题联结词之间一些等价式,149/227,149,2.4.4,谓词演算蕴含式,150/227,150,151/227,151,152/227,152,2.5,谓词公式范式,153/227,153,154/227,154,155/227,155,156/227,156,157/227,157,2.5.2,斯柯林范式,158/227,158,2.6,谓词演算推理理论,159/227,159,2.6.1,规则(全称指定规则)(,Universal Specification,),160/227,160,2.6.2,(全称推广规则)(,Un
16、iversal Generalization,),161/227,161,2.6.3,(存在指定规则)(,Existential Specification,),162/227,162,2.6.4,(存在推广规则)(,Existential Generalization,),163/227,163,164/227,164,165/227,165,166/227,166,167/227,167,习题课,168/227,168,169/227,169,解,170/227,170,171/227,171,解,172/227,172,173/227,173,174/227,174,175/227,17
17、5,176/227,176,177/227,177,178/227,178,179/227,179,解,180/227,180,181/227,181,证实,:,182/227,182,试验二 命题逻辑简单推理系统,183/227,183,184/227,184,185/227,185,186/227,186,187/227,187,第三章:,基于归结原理推理证实,主要内容:,谓词公式与子句集概念,斯柯林,(Skolem),标准范式及其求取过程,海伯伦(,Herbrand,)理论,H,域及其解释,置换与合一,命题和谓词归结原理,归结过程控制策略。,教学要求:,深刻了解和掌握归结原理基本概念和基
18、本归结过程。,重点:,归结原理基本概念和基本归结方法,难点:,归结原理实现方法,。,实践活动:,归结原理程序实现,188/227,188,第,3,章 基于归结原理推理证实*,189/227,189,3.1,谓词公式与子句集,190/227,190,3.1.1.2,斯柯林,(Skolem),标准范式,191/227,191,192/227,192,193/227,193,194/227,194,3.1.2,子句与子句集,195/227,195,3.1.3,不可满足意义下一致性,196/227,196,3.1.4,P,P1,P2,Pn,子句集,197/227,197,3.2,海伯伦(,Herbra
19、nd,)理论,198/227,198,199/227,199,3.2.2,原子集,200/227,200,3.2.3,H,域上解释,201/227,201,202/227,202,3.3,归结原理,(Resolution Method),203/227,203,3.3.1.2,置换合成,204/227,204,3.3.1.3,置换结合律,205/227,205,3.3.1.5,最普通合一置换求取算法,206/227,206,3.3.2,命题逻辑中归结原理,207/227,207,3.3.2.2,归结推理过程,208/227,208,3.3.3,一阶谓词逻辑中归结原理,209/227,209,2
20、10/227,210,211/227,211,212/227,212,3.3.4,归结原理完备性,213/227,213,3.3.5,利用归结原理进行定理证实,214/227,214,215/227,215,3.3.6,应用归结原理进行问题求解,216/227,216,217/227,217,218/227,218,219/227,219,3.4,归结过程控制策略,220/227,220,(2),控制策略分类,221/227,221,3.4.2,归结控制策略及其应用举例,222/227,222,223/227,223,224/227,224,225/227,225,试验三 归结原理程序实现,226/227,226,227/227,227,
©2010-2025 宁波自信网络信息技术有限公司 版权所有
客服电话:4008-655-100 投诉/维权电话:4009-655-100