搜索
1学科介绍1.1数理逻辑介绍1.1.1什么是数理逻辑？逻辑是探索、阐述和确立有效推理原则的学科，最早由古希腊学者亚里士多德创建的。用数学的方法研究关于推理、证明等问题的学科就叫做数理逻辑。也叫做符号逻辑。数理逻辑的内容：1、命题逻辑系统2、一阶谓词逻辑系统命题演算是研究关于命题如何通过一些逻辑连接词构成更复杂的命题以及逻辑推理的方法。命题是指具有具体意义的又能判断它是真还是假的句子。如果我们把命题看作运算的对象，如同代数中的数字、字母或代数式，而把逻辑连接词看作运算符号，就象代数中的“加、减、乘、除”那样，那么由简单命题组成复和命题的过程，就可以当作逻辑运算的过程，也就是命题的演算。AA-BBA(BA)这样的逻辑运算也同代数运算一样具有一定的性质，满足一定的运算规律。例如满足交换律、结合律、分配律，同时也满足逻辑上的同一律、吸收律、双否定律、狄摩根定律、三段论定律等等。利用这些定律，我们可以进行逻辑推理，可以简化复和命题，可以推证两个复合命题是不是等价，也就是它们的真值表是不是完全相同等等。命题演算的一个具体模型就是逻辑代数。逻辑代数也叫做开关代数，它的基本运算是逻辑加、逻辑乘和逻辑费，也就是命题演算中的“或”、“与”、“非”，运算对象只有两个数0和1，相当于命题演算中的“真”和“假”。逻辑代数的运算特点如同电路分析中的开和关、高电位和低电位、导电和截至等现象完全一样，都只有两种不同的状态，因此，它在电路分析中得到广泛的应用。利用电子元件可以组成相当于逻辑加、逻辑成和逻辑非的门电路，就是逻辑元件。还能把简单的逻辑元件组成各种逻辑网络，这样任何复杂的逻辑关系都可以有逻辑元件经过适当的组合来实现，从而使电子元件具有逻辑判断的功能。因此，在自动控制方面有重要的应用。谓词演算也叫做命题涵项演算。在谓词演算里，把命题的内部结构分析成具有主词和谓词的逻辑形式，由命题涵项、逻辑连接词和量词构成命题，然后研究这样的命题之间的逻辑推理关系。Bird(老鹰)ABird(X)A--fly(X)BFly(鸵鸟)CP(X,y),P就是表示y=x.y=x+1命题涵项就是指除了含有常项以外还含有变项的逻辑公式。常项是指一些确定的对象或者确定的属性和关系；变项是指一定范围内的任何一个，这个范围叫做变项的变域。命题涵项和命题演算不同，它无所谓真和假。如果以一定的对象概念代替变项，那么命题涵项就成为真的或假的命题了。命题涵项加上全程量词或者存在量词，那么它就成为全称命题或者特称命题了。1.1.2什么是高级数理逻辑？高级数理逻辑是研究数理各种数理逻辑系统的构成和性质的科学。高级数理逻辑综合了数理逻辑、形式化方法和计算逻辑中的主要内容。主要内容包括：1、命题逻辑系统形式化描述2、一阶谓词逻辑系统形式化描述3、形式化系统的语义结构4、自动推理方法5、模态逻辑、时态逻辑6、非单调逻辑系统1.2数理逻辑发展1.2.1数理逻辑发展史逻辑学→数理逻辑→形式逻辑→计算逻辑1、逻辑思想的提出：亚里士多德提出建立探索人类推理、思维原则的学科，从而有了逻辑的概念。2、数理逻辑思想提出：莱布尼茨提出创造一种“通用的科学语言”，可以把推理过程象数学一样利用公式来进行计算，从而得出正确的结论。由于当时的社会条件，他的想法并没有实现。但是它的思想却是现代数理逻辑部分内容的萌芽，从这个意义上讲，莱布尼茨的思想可以说是数理逻辑的先驱。3、数理逻辑诞生：1847年，英国数学家布尔发表了《逻辑的数学分析》，建立了“布尔代数”，并创造一套符号系统，利用符号来表示逻辑中的各种概念。布尔建立了一系列的运算法则，利用代数的方法研究逻辑问题，初步奠定了数理逻辑的基础。4、发展成独立学科：十九世纪末二十世纪初，数理逻辑有了比较大的发展，1884年，德国数学家弗雷格出版了《数论的基础》和《符号论》，在书中引入量词的符号，使得数理逻辑的符号系统更加完备。对建立这门学科做出贡献的，还有美国人皮尔斯，他也在著作中引入了逻辑符号。从而使现代数理逻辑最基本的理论基础逐步形成，成为一门独立的学科。5、公理集合论促进了数理逻辑形式系统的产生：英国唯心主义哲学家、逻辑学家、数学家罗素在集合论的研究过程中，于1903年提出了著名的罗素悖论（数学史上的第三次危机）。罗素悖论动摇了集合论的基础，促使人们去研究数学中的矛盾性。从而提出了公里集合论。公里集合论的产生和发展，促进了形式系统的产生。德国数学家弗雷格《符号论》就是形式化系统的原型。公里集合论促进了其他学科的发展，如罗巴契夫斯基几何的产生等。6、形式推理自动化的产生：1965年Robinson提出了归结原理（PrincipleofResolution），归结原理提出了基于形式描述的，利用计算机的推理方法。从而使机器定理证明和计算机辅助软件工程得到长足的发展。A1,A2,A3,A4,An;7、1982RETE-－ruleengine1.2.2数理逻辑与其研究对象数理逻辑通常有两种研究对象或者称作用：1、对世界的描述：认为逻辑是描述世界的最基本单元。如逻辑原子主义和逻辑实证主义等观点认为，每个逻辑原子是对世界的描述。而推理过程描述了世界的变化过程。这种观点是罗素所主张的哲学观点，他认为世界上的一切都可以用逻辑原子来描述。从而世界没有必要讨论意识与物质关系的问题。2、对思维的描述：认为逻辑是对人类思维过程的描述，主要研究推理过程。在本课程中认为逻辑原子描述了对应的世界中的一个基本事物，而推理规则是人类思维的原则。逻辑原子可以指非现实世界，如把欧式几何作为一个研究对象。同时我们集中研究数理逻辑系统的构成及其性质。1.2.3数理逻辑的学科发展从数理逻辑学中衍生出来的学科有很多，如：递归论、可计算理论、模型论、机器证明、知识工程、布尔代数等。这些理论都是以数理逻辑学为基础的。针对数理逻辑本身，由于这些学科的需求产生了很多不同种类的逻辑系统。数理逻辑的不同种类，基本上都是从经典的逻辑系统中扩展而来的。这种扩展通常有语法扩展和语义扩展。语法扩展：在经典逻辑系统中，扩充一些符号，从而衍生出新的逻辑系统。如模态逻辑，二阶谓词逻辑等。语义扩展：对逻辑系统中语义的范围等进行扩展，如模糊逻辑等fuzzylogic。数理逻辑通常划分成以下不同种类的逻辑系统：1、经典逻辑：传统的命题逻辑、一阶谓词逻辑等。认为世界是黑白的，对于一个命题非真既假。2、模态逻辑：认为世界上任何事情的真假是与场合有着密切的关系的。3、多值逻辑：认为世界上的对与错是没有绝对的，命题的真假是可以是多个甚至连续值的。A=0.34、非单调逻辑：讨论如何将人类的常识加入到逻辑系统中去。经典逻辑是单调逻辑，既事实越多，已有的结论不会消失；而单调逻辑中，可能随着事实的增加原有的结论被否定。5、CBR－概率推理;LBN－MIT1.3数理逻辑与其他科学1.3.1数理逻辑与计算机科学数理逻辑首先是计算机科学的基础，反过来计算机科学的发展又促进了数理逻辑学的发展。我们从以下几个方面来阐述，数理逻辑与计算机科学之间的关系。1、可计算理论与数理逻辑图灵机的提出奠定了计算机的基础：1903年罗素悖论的提出给数学界带来极大的震动，数学的基础受到了动摇。正是在这种背景下，应该数学家图灵图灵在数理逻辑大本营的剑桥大学提出一个设想：能否有这样一台机器，通过某种一般的机械步骤，能在原则上一个接一个地解决所有的数学问题。1936年图灵发表一篇著名的论文《论数字计算在判决难题中的应用》。他提出了一种十分简单但运算能力极强的理想计算装置，用它来计算所有能想象得到的可计算函数。它由一个控制器和一根假设两端无界的工作带组成。工作带起着存储器的作用，它被划分为大小相同的方格，每一格上可书写一个给定字母表上的符号。控制器可以在带上左右移动，控制带有一个读写头，读写头可以读出控制器访问的格子上的符号，也能改写和抹去模块1模块2模块3结论逻辑公式1逻辑公式1逻辑公式3结论专家知识知识库这一符号。这一装置只是一种理想的计算模型，或者说是一种理想中的计算机。这就是电脑史上与“冯·诺依曼机器”齐名的“图灵机”。“图灵机”不是一种具体的机器，而是一种思想模型。它由三部分组成：一条带子，一读写头和一个控制装置，能计算出任何给定的计算，也能执行任何可能的任务。图灵的这一思想实际上奠定了现代计算机的基础。图灵机导致了数理逻辑的发展，产生了新的学科“可计算理论”：对于一个数学问题，能否有图灵机解是可计算理论研究的主要问题。2、软件工程与数理逻辑：20世纪80年代曼纳（Manna），提出利用时态逻辑来描述程序结构。从而将数理逻辑与程学设计与计算机辅助软件工程（CASE）结合在一起。从而掀起了学术界对时态逻辑、模态逻辑等逻辑系统的研究热潮。我们国家软件所得唐秩松教授在这个方面的研究工作处于世界领先地位。CASE=ROSE-UML=将程序的执行过程抽象成多个逻辑公式，通过逻辑公式之间的推理来得到结论。对于这种方法给软件工程解决以下问题：A、自动化程序设计：给出所目标程序的逻辑表达式，由这个逻辑表达式，产生所需要的程序。B、程序验证：将现有的程序，描述成逻辑表达式，通过对逻辑表达式的推理，证明程序的正确性。3、人工智能与数理逻辑：人工智能中需要将人类的知识进行抽象、表示、利用。从而使计算机具有人类的智力水平。利用知识进行推理必然要涉及的推理的科学－数理逻辑，因此数理逻辑在人工智能中有非常重要的作用。在人工智能中，利用数理逻辑的主要有：经典逻辑－知识工程非单调逻辑－常识推理（弥补了经典逻辑在描述世界时的不足之处）例如：利用知识推理的过程推理机例如：常识推理鸟会飞鸵鸟是鸟鸵鸟会飞4、定理机器证明：对于给定的公里系统定理集合和固定的。那么怎样利用计算机技术将人类从复杂的定理证明过程中，解脱出来是人们长期考虑的问题。定理机器证明正是解决这个问题。例如：给出前提，证明结论的过程。前提：P1,P1,P1,….,Pn.求证：结论A成立。归结原理中讲述怎样建立这样的证明推理系统。1.3.2数理逻辑与数学代数学对数理逻辑的促进作用：数理逻辑近年来发展特别迅速，主要原因是这门学科对于数学其它分支如集合论、数论、代数、拓扑学等的发展有重大的影响，特别是对新近形成的计算机科学的发展起了推动作用。反过来，其他学科的发展也推动了数理逻辑的发展。对于代数来说，每一种逻辑会对应一种不同的逻辑系统。逻辑促进了代数学的发展，而代数学反过来促进逻辑学的发展。经典逻辑多值逻辑布尔代数软代数（格论的一种）1.4课程介绍1.4.1本课程主要内容本课程主要讲述的内容：1、形式系统概述2、命题演算逻辑系统3、一阶谓词演算逻辑系统4、归结原理，逻辑程序设计5、模态逻辑系统学习本课程主要掌握以下内容：1、逻辑系统的形式化描述方法2、掌握逻辑系统的两种语义结构（Taski语义和Kripke语义）3、形式系统的基本性质4、命题逻辑与一阶谓词逻辑的形式系统5、归结原理6、模态逻辑系统1.4.2本课程参考资料《面向计算机科学的数理逻辑学》陆钟万《计算机科学中的逻辑学》王元元南京大学《元数学》莫绍揆1.5附件：相关人物介绍1.5.1弗雷格弗雷格，G.GottlobFrege(1848～1925)德国数学家、逻辑学家和哲学家。1869～1871年先后在耶拿大学、哥丁根大学学习，1873年获博士学位，1874年起在耶拿大学任教，直到1918年退休。他在数学和哲学的研究中做了许多开拓性的工作，对数理逻辑、数理哲学以及语言哲学的发展产生了重要的影响，被誉为现代数理逻辑和分析哲学的创始人或奠基者。他的主要著作有：《概念演算──一种按算术语言构成的纯思维的符号语言》(1879)、《算术的基础──对数概念的逻辑数学研究》(1884)、《算术的基本规律》（第1卷，1893；第2卷,1903）；重要的论文有：《函项和概念》(1891)、《论概念和对象》(1892)、《论意义和指称》(1892)。谓词理论弗雷格把数学中的函数引入哲学，提出新的谓词理论，解决了传统哲学中关于“共相”、“存在”等问题的长期争论。他以数学中的主目──函数与逻辑中的对象──概念作