《离散数学命题演算系统.ppt》由会员分享，可在线阅读，更多相关《离散数学命题演算系统.ppt（30页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、离散数学命题演算系统现在学习的是第1页，共30页目录数理逻辑集合论图论抽象代数现在学习的是第2页，共30页数理逻辑命题演算命题与联结词重言式范式命题演算形式系统谓词演算个体、谓词和量词谓词演算永真式谓词公式的前束范式一阶谓词演算形式系统现在学习的是第3页，共30页上次我们讲到几种命题公式重言式、矛盾式、可满足式逻辑等价、逻辑蕴含重言式的代入原理命题公式的替换原理析（合）取范式、主析（合）取范式联结词的（极小）功能完备集现在学习的是第4页，共30页命题演算：形式系统重言式反应了人类逻辑思维的基本规律排中律AAt矛盾律 AAf假言推理A(AB)B归谬推理(AB)BA穷举推理(AB)(AC)(BC)
2、C真值计算、以代入原理、替换原理进行推演难以反应人类思维推理过程，需要建立严密的符号推理体系现在学习的是第5页，共30页命题演算：形式系统形式系统是一个符号体系系统中的概念由符号表示推理过程即符号变换的过程以若干最基本的重言式作为基础，称作公理（axioms）系统内符号变换的依据是若干确保由重言式导出重言式的规则，称作推理规则（rules of inference）公理和推理规则确保系统内由正确的前提总能得到正确的推理结果现在学习的是第6页，共30页命题演算：证明与演绎证明(proof)公式序列A1,A2,Am称作Am的一个证明，如果Ai(1im)或者是公理，或者由Aj1,Ajk(j1,jki
3、)用推理规则推得。当这样的证明存在时，称Am为系统的定理(theorem)，记作*Am（*是形式系统的名称），或者简记为Am现在学习的是第7页，共30页命题演算：证明与演绎演绎(deduction)设为一公式集合。公式序列A1,A2,Am称作Am的以为前提的演绎，如果Ai(1im)或者是中的公式，或者是公理，或者由Aj1,Ajk(j1,jki)用推理规则推得。当有这样的演绎时，Am称作的演绎结果，记作*Am（*是形式系统的名称），或者简记为Am称和的成员为Am的前提(hypothesis)证明是演绎在为空集时的特例现在学习的是第8页，共30页命题演算：形式系统PC命题演算形式系统PC(Prop
4、osition Calculus)PC的符号系统命题变元：p,q,r,s,p1,q1,r1,s1,命题常元：t,f联结词：,（注意是完备集）括号：(,)命题公式命题变元和命题常元是公式如果A,B是公式，则(A)，(AB)均为公式（结合优先级和括号省略约定同前）只有有限次使用上面两条规则得到的符号串才是命题公式现在学习的是第9页，共30页命题演算：形式系统PCPC的公理（A,B,C表示任意公式）A1:A(BA)A2:(A(BC)(AB)(AC)A3:(AB)(BA)PC的推理规则（A,B表示任意公式）A,AB/B（分离规则）现在学习的是第10页，共30页命题演算：形式系统PCPC的合理性(sou
5、ndness)如果公式A是系统PC的定理，则A是重言式（如果PCA，则A）如果A是公式集合的演绎结果，那么A是的逻辑结果（如果PCA，则A）PC合理性的证明PC中的公理A1,A2,A3都是重言式；PC的分离规则是“保真”的，就是如果A真，AB真，总有B真。这样，由公理和规则导出的所有定理都是重言式由、公理和规则导出的公式，在中的公式都为真时也为真现在学习的是第11页，共30页命题演算：形式系统PCPC的一致性(consistency)没有公式A，使得PCA和PCA同时成立由PC的合理性容易证明PC的完备性(completeness)如果公式A是重言式，则A一定是PC中的定理（如果A，则PCA）
6、如果公式A是公式集合的逻辑结果，则A一定是的演绎结果（如果A，则PCA）证明很难，略。现在学习的是第12页，共30页命题演算：形式系统PC证明定理：PCAA1(A(AA)A)(A(AA)(AA)：公理A22 A(AA)A)：公理A13(A(AA)(AA)：对1,2使用分离规则4 A(AA)：公理A15 AA：对3,4使用分离规则现在学习的是第13页，共30页命题演算：形式系统PC证明：A,B(AC)BC1 A：前提2 B(AC)：前提3 A(BA)：公理A14 BA：对1,3用分离规则5(B(AC)(BA)(BC)：公理A26(BA)(BC)：对2,5用分离规则7 BC：对4,6用分离规则现在
7、学习的是第14页，共30页命题演算：形式系统PC演绎定理对任意公式集合和公式A,B，AB当且仅当AB当=时，AB当且仅当AB，或AB归谬定理对任何公式集合和公式A,B，若AB，AB，那么A穷举定理对任何公式集合和公式A,B，若AB，AB，那么B现在学习的是第15页，共30页命题演算：形式系统PC证明：AAA(AA)：公理A1，由演绎定理证明了：A,AAA(AA)：公理A1，由演绎定理证明了：A,AA，也就是A,AA上面两个前提，用归谬定理得到AA再用演绎定理，有AA现在学习的是第16页，共30页命题演算：形式系统PC证明：(AC)(BC)(AB)C)根据演绎定理，只需要证明AC,BC,ABC因
8、为AC,BC,AB,AC是显然的AC,BC,AB,AC是易证的根据穷举定理AC,BC,ABC得证现在学习的是第17页，共30页命题演算：定理判定问题一个形式系统本质上说是一个符号串的集合形式系统的定义就是符号串集合的构造性定义符号体系规定了符号串可能包含的字符（或字符的合法组合模式，词）如PC中的命题变元、常元和公式的定义公理规定了几个集合中的符号串（或者这种符号串的模式）如PC中的公理，实质是公理模式推理规则规定了从集合中已知符号串转换生成集合中其它符号串的方法如PC中的分离规则现在学习的是第18页，共30页命题演算：定理判定问题形式系统中的定理本质上就是在集合中的符号串定理的证明过程就是符
9、号串的构造过程这个过程需要在有限步内结束定理判定问题给定一个符号串，判定是否形式系统中的定理能否单靠形式系统本身的公理和推理规则在有限步骤内判定定理和非定理？现在学习的是第19页，共30页命题演算：定理判定问题例子：一个简单的形式系统MIU符号系统：M,I,U组成的串初始串：MI公理：MI规则1：如果串的最后一个符号是I，则可以加上一个U如果xI是定理，那么xIU也是定理规则2：如果串符合Mx，则可以再加上x而生成Mxx，x代表任何一个由M,I,U组成的串如果Mx是定理，那么Mxx也是定理现在学习的是第20页，共30页命题演算：定理判定问题一个简单的形式系统MIU规则3：如果串中出现连续3个I
10、，则可以用U代替III得到新串如果xIIIy是定理，那么xUy也是定理规则4：如果串中出现UU，则可以将UU删去得到新串如果xUUy是定理，那么xy也是定理判定问题：MU是否系统中的串？MU是否定理？现在学习的是第21页，共30页命题演算：定理判定问题一个简单的形式系统MIU由公理和推理规则，我们容易构造定理树MIMIUMII12MIUIUMIUIUIUIU22MIIUMIIUIIU12MIIIIMIIIIUMIIIIIIIIMUIMIU1233MU?2现在学习的是第22页，共30页命题演算：定理判定问题一个简单的形式系统MIU用构造系统中所有定理的方法并不能保证在有限的步骤内能够判定定理到底
11、MU是不是定理？我们需要利用同构机制求助于系统之外的自然数运算定律现在学习的是第23页，共30页命题演算：定理判定问题MIU的一种同构M对应3，I对应1，U对应0自然数31在集合中规则1：如果集合中有数以1结尾，则添一个0也是集合中的数规则2：如果集合中有数以3开始，则把3后面的数再重复一次添在末尾也是集合中的数规则3：如果集合中有数包含111，则把111替换成0也是集合中的数规则4：如果集合中有数包含00，则去掉00的数也是集合中的数问：30是不是集合中的数？现在学习的是第24页，共30页命题演算：定理判定问题MIU的一种同构通过分析数的构造规则，我们发现集合中的数都不可能被3整除31不能被
12、3整除规则14都不能从不能被3整除的数生成能被3整除的数30可以被3整除，所以30不属于这个集合结论：MU不是MIU系统中的定理现在学习的是第25页，共30页命题演算：定理判定问题形式系统PC定理判定问题一个符合PC符号体系定义的命题公式，是否是PC中的定理？同样，用PC系统中公理和分离规则不能保证能在有限步骤判定一个命题公式是否定理但是，PC有一个非常重要的同构：真值函数运算系统只需要用真值表判定命题公式对应的真值函数是否重言式，即可判定是否PC中的定理，真值表的运算是有限步骤可以完成的。（注意：真值表并不是PC中的成分）现在学习的是第26页，共30页下次我们讲谓词演算个体、谓词和量词谓词公
13、式永真式一阶谓词演算形式系统FC自然推理系统ND现在学习的是第27页，共30页数理逻辑教学进程第1课：概论和课程介绍（07.02.27）第2课：命题和联结词（07.03.01）第3课：重言式和范式（07.03.06）第4课：命题演算系统（07.03.13）第5课：谓词演算和永真式（07.03.15）第6课：谓词演算形式系统（四）现在学习的是第28页，共30页关于课程教材O158/75计算机科学中的离散结构王元元,张桂芸编著，机械工业出版社 2004O158/60离散数学导论王元元,张桂芸编著，科学出版社 2002O158/36离散数学王元元,李尚奋编著，科学出版社 1994现在学习的是第29页，共30页END特殊符号表,PC,现在学习的是第30页，共30页