逻辑学与程序设计(1)

逻辑学与程序设计 1 2012年2月22xianyubo 逻辑学与计算科学的关系本课程开设目的本课程的主要内容考核和学习方法 一导论 现代计算机的产生和数理逻辑的发展 人工智能中的逻辑学自动定理证明与逻辑程序设计语言逻辑学在程序设计中的应用 逻辑学与计算科学的关系 现代逻辑创始于19世纪末叶和20世纪早期 其发展动力主要来自于数学中的公理化运动数理逻辑的发展和计算机的产生密切有关数理逻辑是计算理论的基础 而计算理论又是计算机科学的核心基础数理逻辑学家的工作对于通用计算机的产生是决定性的 许多计算机科学的先驱者既是数学家 又是逻辑学家 现代计算机的产生和数理逻辑的发展 阿兰 麦席森 图灵AlanMathisonTuring 6月23日生于英国伦敦 是英国著名的数学家和逻辑学家 被称为计算机科学之父 人工智能之父 是计算机逻辑的奠基者 提出了 图灵机 和 图灵测试 等重要概念 人们为纪念其在计算机领域的卓越贡献而设立 图灵奖 1936年5月 图灵写出了表述他的最重要的数学成果的论文 论可计算数及其在判定问题中的应用 该文于1937年在 伦敦数学会文集 第42期上发表后 立即引起广泛的注意 1937年 阿兰 麦席森 图灵发表的另一篇文章 可计算性与 可定义性 则拓广了丘奇 Church 提出的 丘奇论点 形成 丘奇 图灵论点 对计算理论的严格化 对计算机科学的形成和发展都具有奠基性的意义 现代计算机的产生和数理逻辑的发展 约翰 冯 诺依曼 JohnVonNeumann 1903 1957 美藉匈牙利人在第二次世界大战前 他主要从事算子理论 集合论等方面的研究冯 诺依曼对人类的最大贡献是对计算机科学 计算机技术和数值分析的开拓性工作 EDVAC方案明确奠定了新机器由五个部分组成 包括 运算器 逻辑控制装置 存储器 输入和输出设备 并描述了这五部分的职能和相互关系 报告中 诺伊曼对EDVAC中的两大设计思想作了进一步的论证 为计算机的设计树立了一座里程碑 设计思想之一是二进制 逻辑代数的应用已成为设计电子计算机的重要手段 现代计算机的产生和数理逻辑的发展 Haskell是一种纯函数式编程语言 它的命名源自美国数学家HaskellBrooksCurry 他在数学逻辑方面上的工作使得函数式编程语言有了广泛的基础 现代计算机的产生和数理逻辑的发展 约翰 麦卡锡 JohnMcCarthy 1927年9月4日 2011年10月24日 生于美国马萨诸塞州波士顿 计算机科学家 他因在人工智能领域的贡献而在1971年获得图灵奖 实际上 正是他在1955年的达特矛斯会议上提出了 人工智能 这个概念 全名LIStProcessor 即链表处理语言 由约翰 麦卡锡在1960年左右创造的一种基于 演算的函数式编程语言 Lisp长久以来一直被视为伟大的编程语言之一 数理逻辑与程序设计 基于logic的人工智能 物理符号系统人工智能与LISP程序设计语言计算机科学和人工智能将至少是当前逻辑学发展的主要动力源泉哲学逻辑所研究的许多课题在理论计算机和人工智能中具有重要的应用价值 AI从认知心理学 社会科学以及决策科学中获得了许多资源 但逻辑 包括哲学逻辑 在AI中发挥了特别突出的作用 人工智能中的逻辑学 自动推理与逻辑程序设计语言 自动推理的理论和技术是专家系统 程序推导 程序正确性证明 智能机器人等研究领域的重要基础 自动推理早期的工作主要集中在机器定理证明 1930年Herbrand为定理证明建立了一种重要方法 他的方法奠定了机械定理证明的基础 机械定理证明的主要突破是1965年由J A Robinson做出的 他建立了所谓归结原理 使机械定理证明达到了应用阶段 自动推理早期的工作主要集中在机器定理证明自动定理证明是人工智能的最古老分支 其根源可以从纽维尔和西蒙的 逻辑理论家 NewellandSimon1963a 以及 通用问题求解器 NewellandSimon1963b 纽厄尔和赫伯特 西蒙便利用这个LT程序向数学定理发起了激动人心的冲击 电脑果然不孚众望 它一举证明了数学家罗素的数学名著 数学原理 第二章中的38个定理 洛克菲勒大学教授王浩在 自动定理证明 上获得了更大的成就 1959年 王浩用他首创的 王氏算法 在一台速度不高的IBM704电脑上再次向 数学原理 发起挑战 不到9分钟 王浩的机器把这本数学史上视为里程碑的著作中全部 350条以上 的定理 统统证明了一遍 1953年起 王浩开始计算机理论与机器证明的研究 因为一方面他敏锐地感觉到被认为过分讲究形式的精确 十分繁琐而无任何实际用处的数理逻辑可以在计算机领域发挥极好的作用 自动推理与逻辑程序设计语言 自动推理的基础 归结原理机械定理证明的主要突破是1965年由鲁宾逊 J A Robinson 做出的 他建立了所谓归结原理 使机械定理证明达到了应用阶段 归结法推理规则简单 而且在逻辑上是完备的 因而成为逻辑式程序设计语言Prolog的计算模型 Prolog 一词是 PROgrammationenLOGique 逻辑程序设计语言 的缩写 意思是实现一个用自然语言进行人机对话的软件工具 Prolog是自然语言与自动定理证明完美结合的产物Prolog语言 或者系统 是以一阶谓词逻辑的Horn子句集为语法 以Robinson的消解原理为工具 加上深度优先的控制策略而形成的人工智能通用程序设计语言 自动推理与逻辑程序设计语言 1972年法国科莫劳埃小组实现了第一个逻辑程序设计语言PROLOG 1974年以后R 科瓦尔斯基进一步阐明了PROLOG的理论基础 并系统地发展了逻辑程序设计的思想 对于传统的程序设计来说 算法的逻辑意义往往被程序复杂的控制成分所掩盖 使程序的正确性难以得到证明 而且通常的高级程序设计语言属于过程性语言 需要在程序执行前详细规定运行步骤 科瓦尔斯基对传统的算法或对用通常高级语言编写的程序提出了一个著名的分析公式 即算法 逻辑 控制 其基本思想是要从根本上改变程序设计的方法 用户只需要编写程序的逻辑部分 逻辑程序设计之名由此而来 而系统中的解释程序则实施控制部分的职能 自动推理与逻辑程序设计语言 这种将逻辑与控制分开的方法具有下列的优点 可以在控制部分设计之前不断改进逻辑程序 可以改进控制部分而无需变动逻辑程序本身 可以从程序说明中生成逻辑程序 加以验证和变换 而无需考虑其控制部分 只需在逻辑程序中规定目标和实现这些目标的现有条件 也就是只需告诉系统做什么 Whattodo 至于如何执行也就是说怎样做 Howtodo 则由系统的控制部分 即解释程序处理解决 自动推理与逻辑程序设计语言 数理逻辑对计算机科学的发展起着重要的作用 它是计算机科学工作者必须具备的基本理论 无论是研究算法 程序语言或者是程序本身 它都是必须具备的理论基础 随着人类大量思维过程机械化 计算化的日益发展 数理逻辑的应用也在发展 除了在计算机线路设计方面发挥着重要的作用外 它还是研究计算机软件的基础知识和重要工具 计算机科学是一门应用性强的科学 由于其研究的本质也是对形式逻辑系统的合理性 正确性进行探讨 所以在很多方面可以借鉴数理逻辑的思想 时序逻辑程序设计是一种新型的程序设计范式 程序的具体执行和性质的描述可以在同一逻辑框架内表示 适用于并发系统的建模 模拟和验证 逻辑学在程序设计中的应用 逻辑学与计算科学的关系本课程开设目的本课程的主要内容考核和学习方法 一导论 加深队逻辑学与计算科学关系的认识深入理解逻辑程序设计的数理逻辑基础掌握逻辑程序设计语言的基础知识掌握Prolog程序设计语言掌握Haskell程序设计语言 课程目的 课程目的 逻辑学与计算科学的关系本课程开设目的本课程的主要内容考核和学习方法 一导论 逻辑程序设计的数理逻辑基础 归结原理Prolog程序设计语言Haskell函数式程序设计语言 研究生 课程的主要内容 应用逻辑 logic ProgrammingandPrologLogicProgrammingwithPrologHaskell程序设计语言 教学参考书 逻辑学与计算科学的关系本课程开设目的本课程的主要内容考核和学习方法 一导论 理论基础学习程序设计实践 学习方法 平时成绩 40 期末考试 60 考核方法 Username xianyubo Password sysulogic 课件资料 二逻辑程序设计的数理逻辑基础 命题逻辑 命题 能判断真假的陈述句 命题的真值 命题的判断结果 它只有两种可能 真或假 分别用1和0来表示 真值为1的命题称为真命题 真值为0的命题称为假命题 判断一个句子是否为命题 首先判断它是否陈述句 如果是陈述句 再判断它是否具有唯一的真值 一 命题 proposition 命题用小写字母p q r pi qi ri 表示 真值用1和0表示 称为命题的符号化 比如 p 4是素数 p的真值为0 q 北京是中国的首都 q的真值为1 r 2010年元旦是晴天 r的真值现在不知道 二 命题和真值符号化 一个命题若不能被分解成更简单的陈述句 则称为简单命题或原子命题 若一个命题是由几个简单陈述句通过联结词联结而成的 则称为复合命题 例如 以下命题都是复合命题 2或4是素数 如果2是素数 则3也是素数 2是素数当且仅当3也是素数 关于基本联结词的说明 称为一个联结词集 由联结词集 中的一个联结词联结一个或两个原子命题组成的复合命题是最简单的复合命题 可以称它们为基本的复合命题 基本复合命题的真值见下表 命题公式概念 简单命题是真值唯一确定的命题逻辑中最基本的研究单位 所以也称简单命题为命题常项或命题常元 propositionconstant 称真值可以变化的陈述句为命题变项或命题变元 propositionvariable 也用p q r 表示命题变项 当p q r 表示命题变项时 它们就成了取值0或1的变项 因而命题变项已不是命题 这样一来 p q r 既可以表示命题常项 也可以表示命题变项 在使用中 需要由上下文确定它们表示的是常项还是变项 将命题变项用联结词和圆括号按一定的逻辑关系联结起来的符号串称为合式公式或命题公式 命题公式 wff 1 单个命题变项是合式公式 并称为原子命题公式 2 若A是合式公式 则 A 也是合式公式 3 若A B是合式公式 则 A B A B A B A B 也是合式公式 4 只有有限次地应用 1 3 形式的符号串才是合式公式 合式公式也称为命题公式或命题形式 并简称为公式 设A为合式公式 B为A中一部分 若B也是合式公式 则称B为A的子公式 合式公式 WellFormedFormula 命题公式的解释 在命题公式中 由于有命题符号的出现 因而真值是不确定的 当将公式中出现的全部命题符号都解释成具体的命题之后 公式就成了真值确定的命题了 p q r若p 2是素数 q 3是偶数 r 是无理数 则p与r被解释成真命题 q被解释成假命题 此时公式 p q r被解释成 若2是素数或3是偶数 则 是无理数 真命题 r被解释为 是有理数 则 p q r被解释成 若2是素数或3是偶数 则 是有理数 假命题 将命题变项p解释成真命题 相当于指定p的真值为1 解释成假命题 相当于指定p的真值为0 定义 命题赋值或解释 设p1 p2 pn是出现在公式A中的全部命题变项 给p1 p2 pn各指定一个真值 称为对A的一个赋值或解释 若指定的一组值使A的真值为1 则称这组值为A的成真赋值 若使A的真值为0 则称这组值为A的成假赋值 对含n个命题变项的公式A的赋值情况做如下规定 1 若A中出现的命题符号为p1 p2 pn 给定A的赋值 1 2 n是指p1 1 p2 2 pn n 2 若A中出现的命题符号为p q r 给定A的赋值 1 2 n是指p 1 q 2 最后一个字母赋值 n 上述 i取值为0或1 i 1 2 n 定义 重言式 永真式 可满足式 设A为任一命题公式 1 若A在它的各种赋值下取值均为真 则称A是重言式 tautology 或永真式 2 若A在它的各种赋值下取值均为假 则称A是矛盾式 contradiction 或永假式 3 若A不是矛盾式 则称A是可满足式 satisfactableformula A是可满足式的等价定义是 A至少存在一个成真赋值 等值式 两公式什么时候表达的逻辑相同呢 抽象地看 它们的真假取值完全相同时即具有相同的逻辑 设公式A B共同含有n个命题变项 可能对A或B有哑元 若A与B有相同的真值表 则说明在2n个赋值的每个赋值下 A与B的真值都相同 于是等价式A B为重言式 定义 设A B是两个命题公式 若A B构成的等价式A B为重言式 则称A与B是等值的 记为A B 注意 不要将 和 混淆 A或B中可能有哑元出现 p q p q r r r为左边公式中的哑元 用真值表可以验证两个公式是否等值 常用等值模式 1 双重否定律 A A 2 幂等律 A A A A A A3 交换律 A B B A A B B A4 结合律 A B C A B C A B C A B C 5 分配律 A B C A B A C 对 的分配律 A B C A B A C 对 的分配律 6 德摩根律 A B A B A B A B7 吸收律 A A B A A A B A 8 零律 A 1 1 A 0 09 同一律 A 0 A A 1 A10 互补律 A A 1A A 011 蕴含等值式 A B A B12 等价等值式 A B A B B A 39 LogicalEntailment 逻辑涵蕴 KB setofsentences 知识库 arbitrarysentenceKBentails writtenKB iffeverymodelofKBisalsoamodelof Alternatively KB iff KB isunsatisfiable 不可满足的 KB isvalid 永真的 范式 disjunctivenormalform任何一个命题形式A都可以等价为如下形式的析取范式 Qij如同p或 p的形式 证明 选取A的真值表中使A为真的的那些真值赋值 如 p q q p 中的p T q T和p F q F 然后写为 p q p q 范式 CNF conjunctivenormalform 任何一个命题形式A都可以等价为如下形式的合取范式 Qij如同p或 p的形式 证明 设 A的析取范式为B 如 p q p q 则A逻辑等价于 B 如 p q p q 逻辑等价于 p q p q 为A的合取范式 注意多次使用DeMorgan sLaw 42 ModelofaKB LetKBbeasetofsentencesAmodelmisamodelofKBiffitisamodelofallsentencesinKB thatis allsentencesinKBaretrueinmGivenavocabularyA B CandD howmanymodelsforA B Carethere forA B B 43 ModelofaA B C A B C有多少模型 A B C A B 有多少模型 命题逻辑中的归结原理 子句和子句形归结归结反演合理性和完备性归结反演的搜索策略 子句和子句形 1 子句和子句形 2 一般方法Eliminateimplicationsignsbyusingtheequivalentformusing Reducethescopesof signsbyusingDeMorgan slawandbyeliminatingdouble signsConverttoCNFbyusingtheassociativeanddistributivelaws 子句和子句形 归结 对任意三个文字p q和rp r q r p q或者 forC1 P C1 C2 P C2 P C1 P C2 C1 C2 归结式 R C1 C2 C1 C2 已知A1 A2 A3成立 证明B成立也就是证明A1 A2 A3 B是永真的使用反证法 等价于证明A1 A2 A3 B是永假式 首先将A1 A2 A3 B化成子句集 子句集是子句的合取 子句是只出现原子公式和 的合式公式 证明过程就是从A1 A2 A3 B出发 用归结推理规则寻找矛盾 最后证明A1 A2 A3 B是定理 命题逻辑的归结法 化成合取范式 P Q Q P 建立子句集 P Q Q PS P Q Q P 对S做归结 例 证明 P Q Q P ResolutionRefutations 1 定理证明的任务 由前提A1 A2 An推出结论B即证明 A1 A2 An B永真转化为证明 A1 A2 An B为永假式归结推理就是 从A1 A2 An B出发 使用归结推理规则来找出矛盾 最后证明定理A1 A2 An B的成立 ResolutionRefutations 2 归结方法是一种机械化的 可在计算机上加以实现的推理方法可认为是一种反向推理形式提供了一种自动定理证明的方法是Prolog和大多数自动定理证明的基础简单高效 ResolutionRefutations 3 一般过程 建立子句集S从子句集S出发 仅对S的子句间使用归结推理规则如果得出空子句 则结束 否则转下一步将所得归结式仍放入S中对新的子句集使用归结推理规则转 3 空子句不含有文字 它不能被任何解释满足 所以空子句是永假的 不可满足的归结过程出现空子句 说明出现互补子句对 说明S中有矛盾 因此S是不可满足的 ResolutionRefutations 4 例子 证明 P Q Q p首先建立子句集 P Q Q P P Q Q PS P Q Q P 对S作归结 1 P Q 2 Q 3 P 4 P 1 2 归结 5 3 4 归结 消解树证明 C的从S出发的消解树证明是指具有如下性质的有穷标签二叉树T T的根标示为C T的叶子标识为S中的元素 如果任意非叶子节点 的标识为 2 其直接后续 1 2分别标识为 0 1 那么 2是 0 1的消解式 公式S p r q s t 的消解树反驳 即从 的从S出发的消解树证明 例子 消解的可靠性 消解的完全性 消解的完全性 更抽象的表达 主要思想 根据情况cases分解S的可满足性 对应于 为真的情况 对应于 为真的情况 因此将S的可满足性化简为 少掉一个命题字母的 和 的问题 一直这样简化下去 生成一个以公式为节点的二叉树 每一层消去一个文字 该树的每一条路径都对应着一个指派 如果所有路径都已一个包含空子句的句子结束则S是不可以满足的 否则 要么存在一条无穷路径 要么存在一条路径是以空公式结束 例子 提高搜索的效率 限制搜索空间判断S的可满足性是NP完全问题一是通过终结无望路径上的搜索二是制定替代路径上的次序 加细消解或精炼消解 T 消解是指父子句均非重言式式的消解 是 在 消解下的闭包T消解的可靠性T消解的完全性 证明基本上同前 忽略重言式 T 消解 令A为一个指派 A 消解是指父子句之中至少有一个在A下为假的消解 如果所有的父子句在A下都为真 那么消解式也为真 而没有在A下失败的子句 就不能期望得到不可解性 是 在 消解下的闭包 这有称为语义消解 A 消解的完全性 对于任意的A和S 如果S UNSAT 则 A 消解 假设我们已经给所有的命题字母编