《高级数理逻辑》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）结合在一起。从而掀起了学术界对时态逻辑、模态逻辑等逻辑系统的研究热潮。我们国家软件所得唐秩松教授在这个方面的