《高级数理逻辑》PPT课件.ppt

-,1,高级数理逻辑,-,2,主要内容,预备知识 形式系统 命题逻辑形式系统 一阶谓词逻辑形式系统 归结原理,-,3,1. 预备知识,1.1 基本概念 1.2 数理逻辑的发展过程 1.3 数理逻辑学科的发展 1.4 数理逻辑与其他科学 1.5 课程学习内容 1.6 主要掌握内容,-,4,1.1 基本概念,逻辑 探索、阐述和确立有效推理原则的学科，最早由古希腊学者亚里士多德创建。 数理逻辑 用数学的方法研究关于推理、证明等问题的学科就叫做数理逻辑，又称为符号逻辑。,-,5,1.1 基本概念,数理逻辑的研究内容 对世界的描述：认为逻辑是描述世界的最基本单元。如逻辑原子主义和逻辑实证主义等观点认为，每个逻辑原子是对世界的描述。而推理过程描述了世界的变化过程。这种观点是罗素所主张的哲学观点，他认为世界上的一切都可以用逻辑原子来描述。从而世界没有必要讨论意识与物质关系的问题。 对思维的描述：认为逻辑是对人类思维过程的描述，主要研究推理过程。,-,6,1.1 基本概念,数理逻辑的研究内容 （1）命题逻辑系统 命题是指具有具体意义的又能判断它是真还是假的句子。 研究关于命题如何通过一些逻辑连接词构成更复杂的命题以及逻辑推理的方法。 把命题看作运算的对象，如同代数中的数字、字母或代数式，而把逻辑连接词看作运算符号，就象代数中的“加、减、乘、除”那样，那么由简单命题组成复和命题的过程，就可以当作逻辑运算的过程，也就是命题的演算。,-,7,1.1 基本概念,（2）一阶谓词逻辑系统 谓词演算也叫做命题涵项演算。在谓词演算里，把命题的内部结构分析成具有主词和谓词的逻辑形式，由命题涵项、逻辑连接词和量词构成命题，然后研究这样的命题之间的逻辑推理关系。 Bird(鸵鸟) Bird(鸟)-fly(鸟) Fly(鸵鸟),-,8,1.1 基本概念,命题涵项 指除了含有常项以外还含有变项的逻辑公式。常项是指一些确定的对象或者确定的属性和关系；变项是指一定范围内的任何一个，这个范围叫做变项的变域。命题涵项和命题演算不同，它无所谓真和假。如果以一定的对象概念代替变项，那么命题涵项就成为真的或假的命题了。 命题涵项加上全称量词或者存在量词，那么它就成为全称命题或者特称命题。,-,9,1.1 基本概念,逻辑推理的过程 前提（真/假的命题）结论（真/假的命题） 命题 具有真假值的句子 演绎推理 前提的真蕴涵结论的真，即前提和结论之间的推导是正确的。 归纳推理 前提的真并不蕴涵结论的真。,-,10,1.1 基本概念,高级数理逻辑 研究各种数理逻辑系统的构成和性质的科学。高级数理逻辑综合了数理逻辑、形式化方法和计算逻辑中的主要内容。 主要研究内容 命题逻辑系统形式化描述 一阶谓词逻辑系统形式化描述 形式化系统的语义结构 自动推理方法 模态逻辑、时态逻辑 非单调逻辑系统,-,11,1.1 基本概念,形式语言 人工构造的符号语言，以取代自然语言。 对象语言 被讨论的语言。 元语言 讨论对象语言时的语言。,-,12,1.1 基本概念,语义 涉及符号和符号表达式的涵义。 语法 涉及符号表达式的形式结构，不考虑任何对语言的解释。 两者既有区别又有联系。,-,13,1.2 数理逻辑的发展过程,逻辑学数理逻辑形式逻辑计算逻辑 第一阶段：逻辑学思想的提出 亚里士多德提出建立探索人类推理、思维原则的学科，从而有了逻辑的概念。,-,14,1.2 数理逻辑的发展过程,第二阶段：数理逻辑思想的提出 莱布尼茨提出创造一种“通用的科学语言”，可以把推理过程象数学一样利用公式来进行计算，从而得出正确的结论。,-,15,1.2 数理逻辑的发展过程,第三阶段：数理逻辑的诞生 1847年，英国数学家布尔发表了逻辑的数学分析，建立了“布尔代数”，并创造一套符号系统，利用符号来表示逻辑中的各种概念。布尔建立了一系列的运算法则，利用代数的方法研究逻辑问题，初步奠定了数理逻辑的基础。,-,16,1.2 数理逻辑的发展过程,第四阶段：发展为独立的学科 十九世纪末二十世纪初，数理逻辑有了比较大的发展，1884年，德国数学家弗雷格出版了数论的基础和符号论，在书中引入量词的符号，使得数理逻辑的符号系统更加完备。对建立这门学科做出贡献的，还有美国人皮尔斯，他也在著作中引入了逻辑符号。从而使现代数理逻辑最基本的理论基础逐步形成，成为一门独立的学科。,-,17,1.2 数理逻辑的发展过程,第五阶段：公理集合论促进了数理逻辑形式系统的产生 英国唯心主义哲学家、逻辑学家、数学家罗素在集合论的研究过程中，于1903年提出了著名的罗素悖论（数学史上的第三次危机）。罗素悖论动摇了集合论的基础，促使人们去研究数学中的矛盾性。从而提出了公理集合论。公理集合论的产生和发展，促进了形式系统的产生。,-,18,1.2 数理逻辑的发展过程,第六阶段：形式推理自动化的产生 1965年Robinson提出了归结原理（Principle of Resolution），归结原理提出了基于形式描述的，利用计算机的推理方法。从而使机器定理证明和计算机辅助软件工程得到长足的发展。,-,19,1.3 数理逻辑学科的发展,从数理逻辑学中衍生出来的学科很多 如：递归论、可计算理论、模型论、机器证明、知识工程、布尔代数等。 这些理论都是以数理逻辑学为基础的。针对数理逻辑本身，由于这些学科的需求产生了很多不同种类的逻辑系统。,-,20,1.3 数理逻辑学科的发展,数理逻辑的种类 经典逻辑传统的命题逻辑、一阶谓词逻辑等。认为世界是黑白的，对于一个命题非真既假。 模态逻辑认为世界上任何事情的真假是与时间有着密切的关系的。 多值逻辑认为世界上的对与错是没有绝对的，命题的真假是可以是多个甚至连续值的。 非单调逻辑讨论如何将人类的常识加入到逻辑系统中去。经典逻辑是单调逻辑，既事实越多，已有的结论不会消失；而单调逻辑中，可能随着事实的增加原有的结论被否定。,-,21,1.3 数理逻辑学科的发展,数理逻辑的不同种类，基本上都是从经典的逻辑系统中扩展而来的。这种扩展通常有语法扩展和语义扩展。 语法扩展：在经典逻辑系统中，扩充一些符号，从而衍生出新的逻辑系统。如模态逻辑，二阶谓词逻辑等。 语义扩展：对逻辑系统中语义的范围等进行扩展，如模糊逻辑等。,-,22,1.4 数理逻辑与其他科学,数理逻辑与计算机科学 数理逻辑首先是计算机科学的基础 可计算理论与数理逻辑 软件工程与数理逻辑 人工智能与数理逻辑 定理机器证明,-,23,1.4 数理逻辑与其他科学,可计算理论与数理逻辑 1903年罗素悖论的提出给数学界带来极大的震动，数学的基础受到了动摇。正是在这种背景下，英国数学家图灵在数理逻辑大本营的剑桥大学提出：能否有这样一台机器，通过某种一般的机械步骤，能在原则上一个接一个地解决所有的数学问题。这一装置只是一种理想的计算模型，或者说是一种理想中的计算机。 “图灵机”不是一种具体的机器，而是一种思想模型。它导致了数理逻辑的发展，产生了新的学科“可计算理论”：对于一个数学问题，能否有图灵机解是可计算理论研究的主要问题。,-,24,1.4 数理逻辑与其他科学,罗素悖论 一天，萨维尔村理发师挂出一块招牌：“村里所有不自己理发的男人都由我给他们理发，我也只给这些人理发。”于是有人问他：“您的头发由谁理呢?”理发师顿时哑口无言。 因为，如果他给自己理发，那么他就属于自己给自己理发的那类人。但是，招牌上说明他不给这类人理发，因此他不能自己理。如果由另外一个人给他理发，他就是不给自己理发的人，而招牌上明明说他要给所有不自己理发的男人理发。因此，他应该自己理。由此可见，不管怎样的推论，理发师所说的话总是自相矛盾的。,-,25,1.4 数理逻辑与其他科学,1874年，德国数学家康托尔创立了集合论，很快渗透到大部分数学分支，成为它们的基础。到19世纪末，全部数学几乎都建立在集合论的基础之上。 此时，集合论中接连出现了一些自相矛盾的结果，特别是1902年罗素提出的理发师故事反映的悖论。它极为简单、明确、通俗。因此，数学的基础被动摇了，这就是所谓的第三次“数学危机”。,-,26,1.4 数理逻辑与其他科学,软件工程与数理逻辑 20世纪80年代曼纳（Manna），提出利用时态逻辑来描述程序结构。从而将数理逻辑与程学设计与计算机辅助软件工程（CASE）结合在一起。从而掀起了学术界对时态逻辑、模态逻辑等逻辑系统的研究热潮。我们国家软件所得唐秩松教授在这个方面的研究工作处于世界领先地位。,-,27,1.4 数理逻辑与其他科学,将程序的执行过程抽象成多个逻辑公式，通过逻辑公式之间的推理来得到结论。 可解决的软件工程问题 自动化程序设计：给出所目标程序的逻辑表达式，由这个逻辑表达式，产生所需要的程序。 程序验证：将现有的程序，描述成逻辑表达式，通过对逻辑表达式的推理，证明程序的正确性。,-,28,1.4 数理逻辑与其他科学,结论,模块1,模块2,模块3,结论,逻辑公式1,逻辑公式2,逻辑公式3,-,29,1.4 数理逻辑与其他科学,人工智能与数理逻辑 人工智能中需要将人类的知识进行抽象、表示、利用。从而使计算机具有人类的智力水平。利用知识进行推理必然要涉及的推理的科学数理逻辑，因此数理逻辑在人工智能中有非常重要的作用。 例如：常识推理 鸟会飞 鸵鸟是鸟 鸵鸟会飞,-,30,1.4 数理逻辑与其他科学,定理机器证明 对于给定的公理系统定理集合是固定的。那么怎样利用计算机技术将人类从复杂的定理证明过程中解脱出来是人们长期考虑的问题。定理机器证明正是解决这个问题。 例如：给出前提，证明结论的过程。 前提：P1, P1, P1, ., Pn . 求证：结论A成立。 归结原理中讲述怎样建立这样的证明推理系统。,-,31,1.4 数理逻辑与其他科学,数理逻辑与数学 数理逻辑近年来发展特别迅速，主要原因是这门学科对于数学其它分支如集合论、数论、代数、拓扑学等的发展有重大的影响，特别是对新近形成的计算机科学的发展起了推动作用。反过来，其他学科的发展也推动了数理逻辑的发展。对于代数而言，每一种逻辑会对应一种不同的逻辑系统。逻辑促进了代数学的发展，而代数学反过来促进逻辑学的发展。,-,32,1.5 课程学习内容,形式系统概述 命题演算逻辑系统 一阶谓词演算逻辑系统 归结原理 逻辑程序设计,-,33,1.6 主要掌握内容,逻辑系统的形式化描述方法 逻辑系统的两种语义结构（Taski语义和Kripke语义） 形式系统的基本性质 命题逻辑形式系统 一阶谓词逻辑形式系统 归结原理,-,34,参考书籍,面向计算机科学的数理逻辑学陆钟万 科学出版社 计算机科学中的逻辑学 王元元 元数学 莫绍揆,-,35,主要内容,预备知识 形式系统 命题逻辑形式系统 一阶谓词逻辑形式系统 归结原理,-,36,2. 形式系统,2.1 基本概念 2.2 形式系统定义 2.3 形式系统特性,-,37,2.1 基本概念,背景 20世纪初，由于罗素悖论，导致了公理集合论的出现。从而导致了利用公理系统来研究数学的方法。 公理系统的分类 具体公理系统 抽象公理系统 形式系统,-,38,2.1 基本概念,具体公理系统 指有明确具体含义的公理系统。由于公理方法的出现，人们开始利用公理系统描述学科理论。 例如欧氏几何公理系统： 公理1：过直线外一点只有一条直线与已知直线平行。 公理2：两点唯一确定一条直线。 公理3：两条直线如果相交，只有一个交点。 推理规则：采用三段论 同样其他的系统也可以采用同样的方式来描述。,-,39,2.1 基本概念,抽象公理系统 用符号来描述公理系统，从而公理系统再没有确定的物理含义。 例如：欧氏集合中的公理3可以表示为,-,40,2.1 基本概念,形式系统 抽象公理系统从具体公理系统中来，脱离了具体公理系统。但是其推理规则一直沿用三段论一个直觉上成立的规则。形式系统克服这个问题，将抽象公理系统中的规则抽象成笛卡儿乘积的子集。 形式系统的发展过程 具体公理系统抽象公理系统形式系统,-,41,2.1 基本概念,形式系统的特点 形式系统由抽象的符号构成，与实际系统没有任何关系。对于形式系统中的公理，通常没有任何实际意义。 形式系统是对自然科学中理论体系的高度抽象与概括。形式系统可以描述多个实际系统。对于一个形式系统，可以描述一个现实存在的系统。可以增加、更改和删除公理，来描述不同的实际系统。,-,42,2.2 形式系统定义,形式系统的组成 语言部分和推理部分 语言部分用来描述，形式系统中的符号和语言的产生规则等； 推理部分用来描述，由已知的推理规则以及定理等。,-,43,2.2 形式系统定义,形式系统由, TERM, FORMULA, AXIOM, RULE等5个部分构成，其中称为符号表，TERM为项集；FORUMULA为公式集；AIXIOM为公理集；RULE为推理规则集。其中： （1）符号表为非空集合，其元素称为符号。 （2）设*为上全体字符串的组合构成的集合。项集TERM为*的子集，其元素称为项；项集TERM有子集VARIABLE称为变量集合，其元素称为变量。 （3）设*为上全体字符串的组合构成的集合。公式集FORMULA为*的子集，其元素称为公式；公式集有子集ATOM，其元素称为原子公式。,-,44,2.2 形式系统定义,（4）公理集AXIOM是公式集FROMULA的子集，其元素称为公理。 （5）推理规则集RULE是公式集FORMULA上的n元关系集合，即 RULE= 其元素称为形式系统的推理规则。 由定义可知，符号表、项集TERM、公式集FORMULA是形式系统的语言部分；而公理集AXIOM、推理规则集RULE为推理部分。,-,45,2.2 形式系统定义,定理 公式A称为形式系统FS的定理，记为FSA如果存在一个有穷公式序列： 使得 或者为形式系统FS的公理，或者为 由推理规则r得到；则称A为形式系统FS的定理。上面的序列被称为公式A的证明序列。,-,46,2.2 形式系统定义,演绎结果 设为形式系统FS的一个公式的集合，A为一个公式，称A为公式集合的演绎结果，记为FSA；如果存在一个有穷序列： 使得 或者为形式系统FS的公理，或者为公式集合中的元素，或者为 由推理规则r得到；则称A为形式系统FS的定理。上面的序列被称为公式A的演绎。 其中，公式集合又被称为前提。,-,47,2.3 形式系统特性,符号表 为非空、可数集合（有穷、无穷都可以）。 项集TERM、公式集FORMULA、公理集AXIOM和推理规则集RULE是递归集合，即必须存在一个算法能够判定给定符号串是否属于集合（可判定的）。 形式系统中的项是用来描述研究的对象。而公式是用来描述这些研究对象的性质的。这个语言被称为对象语言。定义公式和项产生方法的规则称为词法。 用来描述形式系统中各个部分性质的语言称为元语言。用于研究形式系统的元语言又被称为元数学。,-,48,主要内容,预备知识 形式系统 命题逻辑形式系统 一阶谓词逻辑形式系统 归结原理,-,49,3. 命题逻辑形式系统,3.1 命题逻辑与命题演算 3.2 命题逻辑形式系统 3.3 命题形式演算 3.4 命题逻辑语义 3.5 逻辑推论 3.6 公式化简 3.7 元理论与元语言 3.8 命题逻辑元理论,-,50,3.1 命题逻辑与命题演算,Leibniz提出逻辑推理变成符号演算不久，英国数学家BOOL提出了布尔代数。布尔代数把逻辑命题与逻辑推理归结为代数计算。 命题演算是研究关于命题如何通过一些逻辑连接词构成更复杂的命题以及逻辑推理的方法。 把命题看作运算对象，如同代数中的数字、字母或代数式，而把逻辑连接词看作运算符号，就象代数中的“加、减、乘、除”，则由简单命题组成复和命题的过程，即是逻辑运算的过程，也就是命题演算。,-,51,3.1 命题逻辑与命题演算,命题（Proposition） 可以判断真假的陈述句。不涉及任何联结词的命题称为原子命题。 联结词 为联结词，用于联结一个或者多个命题。其中： 如果A成立则B成立； 如果A成立则B成立，并且如果B成立则A成立； A B，或者A成立或者B成立； A B，A成立并且B成立。,-,52,3.1 命题逻辑与命题演算,非（ ）,A,A,1,0,1,0,-,53,3.1 命题逻辑与命题演算,与（并且 ）,A,A B,0,0,0,0,B,0,1,1,1,0,1,0,1,-,54,3.1 命题逻辑与命题演算,或（或者 ）,A,A B,0,0,1,0,B,0,1,1,1,0,1,1,1,-,55,3.1 命题逻辑与命题演算,蕴涵（如果，则； ）,A,A B,0,1,1,0,B,0,1,1,1,0,1,0,1,-,56,3.1 命题逻辑与命题演算,等价（当且仅当或者其充分必要条件， ）,A,A B,0,1,0,0,B,0,1,1,1,0,1,0,1,-,57,3.1 命题逻辑与命题演算,真值表 命题的真假称为命题的真值，用0表示假；用1表示真。 命题变元 以真值为值域的变量称为命题变元。,-,58,(AVB)-C,-,59,3.1 命题逻辑与命题演算,赋值映射 命题变元集合到0,1上的函数。 如果公式A对任意的赋值映射，取值为真，则称A为永真式； 如果公式A对于所有赋值映射为假，称为A为矛盾式。 对于任意赋值映射，公式A的真值等于公式B的真值，则A与B等价。,-,60,命题逻辑系统的特点,（1）从语义角度研究逻辑命题之间真值变化规律。对于任意公式可以给出其所有的真值可能性。 （2）存在永真式，例如： 等。 （3）永真式通过三段论推理方法得到的公式，仍然为永真式。 基于这样的事实，提出一个问题“是否有永真式的最小集合？”。答案是肯定的。公理方法的出现，使人们开始用公理方法研究逻辑系统。于是产生了命题逻辑形式系统。,-,61,3.2 命题逻辑形式系统（FSPC）,FSPC定义 包括语言和推理两个部分。 PC最著名的形式化系统可能源于Whitehead和Russell 的数学原理(Principia Mathematica)。,-,62,3.2 命题逻辑形式系统（FSPC）,语言部分 （1）符号集：（, ）, , , p1 ,p2 ,p3. ，其中 , , , , 为联接词；（，）为技术符号，即括号；p1 ,p2 ,p3为命题变量（命题变元或者命题符号）。 （2）项集：为空集。 （3）公式集合：公式集合有以下递归定义。 p1 ,p2 ,p3（命题变元）为公式，称为原子公式。 如果A、B为公式，那么 ， 为公式。 除此之外没有公式。 语言部分定义了FSPC的公式（语言）产生规则。,-,63,3.2 命题逻辑形式系统,推理部分 （1）公理：FSPC包含下列三个公理模式。 A1 A2 A3 A-A,-,64,-,65,3.2 命题逻辑形式系统,推理规则集合：只有一条推理规则，称为分离规则，即：,-,66,公式结构,公式产生序列 对于一个*上的字符串A是公式的充分必要条件是存在一个公式序列 其中 为（1）到（3）中的一种： （1）为原子公式 （2）存在 ，使得 （3）存在 ，使得,-,67,公式生成过程举例 （1）首先p、q、r为公式（原子公式） p, q, r, p, q, r, p q, q r, r p, p ( q r), （2）（ ）、 、 为公式； （3） 为公式,公式结构,-,68,树能够更清晰地给出公式的生成过程,公式结构,-,69,公式结构特点,（1）括号是在公式中，是成对出现，左右括号数量相同。 （2）在自然逻辑中，公式有否定式、合取式、析取式、蕴涵式、等值式等不同类型的概念。 （3）由于公式采用递归定义的方法来定义，因此，对上的任意字符串能够判断是否为公式。 （4）形式系统的联结词只有两个，因为在命题逻辑的语义上，其他联结词可以有这两个联结词表示。 （5）由于公式是采用递归定义方式来定义的，因此，对于公式的性质通常采用递归证明方法来证明。,-,70,公式结构特点,例如 设R是一个有关公式的性质，如果要证明R对于所有公式有效则通过下面的证明步骤： （1）对于 ，则 （2） 且 ，则 （3） 是公式，如果 且 ，则 由以上三条，可知R对于FSPC上的所有公式成立。,-,71,3.3 命题形式演算,基本概念 演绎结果与定理：设A为FSPC上一公式，集合 为FSPC上一公式集合。称A为 的演绎结果，记为 ，如果存在一个公式序列： 使得 或者为形式系统FSPC的公理，或者为公式集合中的元素，或者为 由推理规则r得到；则称A为FSPC的演绎结果。当 时，称A为定理FSPC上的定理。称 为A的证明序列。,-,72,3.3 命题形式演算,基本概念 逻辑等价：公式A和B分别为两个公式，如果A,B满足BA，且AB同时成立，则称公式A和B为逻辑等价公式，记为AB。即A,B互为演绎结果。 例如： | ， | ， |,-,73,3.3 命题形式演算,基本概念 对偶：设A为FSPC上由联结词 , , 和原子公式构成的公式。在A中交换 和 ，以及原子公式和它的否定公式，得到公式 ，则称 为A的对偶。,-,74,形式演算举例,求证： 为FSPC的定理 证明（1） A2 （2） A3 （3） A1 （4） （1）（2） （5） （3）（4）,-,75,形式演算举例,已知 求证A成立 证明: A,-,76,主要的形式演算方法,形式演算方法多种多样，通常有以下方法： （1）公理代入原理 设A(P)为含有变元P的公理（定理同样适用），如果将公式A中的变元P替换为命题变元B，则A(B)仍为公理（定理）；（公理填充） A-(B-A);A-(A-A)-A);C-(B-C),-,77,主要的形式演算方法,（2）等价替换原理 设命题公式A含有子公式C（C为命题公式），如果CD，那么将A中子公式C替换为命题公式D（不一定全部），所得公式B满足AB。 A-(A-A)-(A-A)=A-(B-B)-(A-A) A-A=B-B,-,78,主要的形式演算方法,（3）对偶原理 设A为FSPC上的公式， 为其对偶，则A （4）形式演算规则 在FSPC之上，利用分离规则扩展的推理规则。例如：AA（自反规则）；如果A，则 A，其中 为一个公式集合（引入规则）等。这样扩充后的系统被称为自然推理系统。,-,79,主要的形式演算方法,（5）联结词运算规则 针对联结词的运算规律。例如：交换律、结合律、莫根定律等。 对于（1）是对于任何证明序列所必须的。其他的定律都可以由分离规则产生。,-,80,不同类型的证明方法,在命题演算时，主要是证明以下问题： （1）命题 （2）命题 （3）命题 （4）命题 （5）命题 （6）命题,-,81,不同类型的证明方法,针对这些要证明的问题，通常的证明方法： 1）命题 自反规则： 证明 ，只需证明 0 中， 0 销去 如果 则 （分离规则）,-,82,不同类型的证明方法,销去（反证法） 如果 ， ， 则 包含 销去 如果 ，则,-,83,不同类型的证明方法,2）命题 （同上） 3）命题 如果 ， 则 ） 4）命题,-,84,不同类型的证明方法,5）命题 如果或者 或者 B 则 6）命题 如果 并且 B 则 ,-,85,例题,证明： （1） ， 包含 （2） ， 包含 （3） （反证规则）,-,86,形式演算性质,紧致性：设 为FSPC上的公式集合，A为FSPC的公式。如果 ，则存在 的有限子集 0 使得 0 传递性：设 和 1为FSPC上的公式集合，A为FSPC的公式。如果 1 ， 1 ；则 成立。 A1An=A这是从 1推导A一个证明序列。 任取Ai属于证明序列中的，存在一个证明序列。 Bi1.Bim=Ai其中Bj，i1=j=im。或者 中元素，或者公理或者是有前边公式由分离规则得到的。 把所有的Ai证明序列都放在一起替代Ai则构成了A的一个证明序列，这个证明序列是从中对于A的一个推导过程。,-,87,实例1,求证： 证明：（1） （2） A1 （3） （1）（2） （4） A3 （5） （3）（4） （6） A3 （7） （5）（6） （8）,-,88,实例2,已知：A(BC), B, 求证:AC 证明： A(BC), B,A，证明C A(BC) 1 B 2 A 3 BC 4（1，3） C 5（2，4）,-,89,结论,公理推演系统模式单一，易于机械化，而推理过程复杂。 自然推演系统，模式复杂，相对证明过程简单。,-,90,3.4 命题逻辑语义,基本概念 1. 什么是形式系统的语义 形式系统与具体的系统无关 能够用形式系统来描述现实系统 把从形式系统解释成“ ”现实系统的过程称为语义 语义有多种类型：指称语义，克里普克语义，操作语义和公理语义等。,-,91,3.4 命题逻辑语义,基本概念 2语义构成 （指称语义） 语义主要有两部分： 结构：（有两个主要部分构成） *确定研究对象集合，论域或个体域 *把形式系统中的变量到论域中的一组规则映射规则 域值：指一组给公式赋值的规则 根据这项规则将 Atomic Value中,-,92,3.4 命题逻辑语义,语义结构 由于没有变量，所以只有第二部分赋值，值域为0,1 赋值规则： T(A)= 当T（A）0时，T(A)=1。 当T（A）1时，T(A)=0。,-,93,3.4 命题逻辑语义, 当T(A)=T(B)=1时，T( )=1，其他情况T( )=0。 当T(A)1或者T（B）1情况下，T（ ）1，其他情况T（ ）0。,-,94,3.4 命题逻辑语义, 当T(A)=0时候，T（ ）=1；当T(B)=1时，T（ ）=1。其他情况下T（ ）=0。 ,-,95,3.4 命题逻辑语义,语义的特殊公式 （1）公式A为永真式，重言式tautologies，如果对一切赋值 ， A-A （2）A为永假式，矛盾式contradictions，如果对一切赋值 ， AA,-,96,3.4 命题逻辑语义,语义的特殊公式 （3）A，B为逻辑等价的，如果对于一切赋值 ， ，记做AB(A|B) T(A)=T(B),对于任意T （4）可满足的，公式A为可满足的，如果至少存在一个赋值 ，,-,97,3.4 命题逻辑语义,真值计算 有了赋值映射，我们可以计算任意公式的真值。通常真值计算的方法有：真值表计算方法和二叉树计算方法等。 1）真值表 真值表是计算真值的简单工具。利用这个工具可以计算任意公式的真值。,-,98,3.4 命题逻辑语义,实例 公式 的真值表如下：,-,99,3.4 命题逻辑语义,2）利用二叉树，可视化地计算公式的真值。例如：计算下面公式的真值，并给出它是否是重言式