《归结原理不讲》PPT课件.ppt

《《归结原理不讲》PPT课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、人工智能原理第四讲归结原理周日贵华东交通大学信息工程学院1归结原理4.1引言4.2一阶逻辑4.3子句形4.4Herbrand定理4.5置换与合一4.6归结原理4.7归结法的完备性4.8归结策略24.1引言自动定理证明历史四色定理三类方法3自动定理证明AutomatedTheoremProving(ATP)定理机器证明(MechanicalTheoremProving)为什么？定理证明是一种智能行为；体现了人类的逻辑推理能力；推理用计算来实现Leibniz的梦想：Leibnizimaginedauniversalformalcalculuswhichcouldexpressre

2、asoninginanysubject,andanalgorithmicprocedurewhichcouldbeappliedtodecidetruthofstatementsinthiscalculus.41930年，Herbrand定理。半可判定问题。一阶逻辑的判定问题。在一阶逻辑中，有没有方法可以判断任何一个命题是否定理？(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。数理逻辑的基本问题。1936年，证明基本问题是不可解的。在一阶逻辑中，如果一个定理是正确的，则有一个机械的方法在有限步内证明它。一阶谓词逻辑有很强的表达能力，凡可计算的函数就可由一阶谓

3、词表达。5历史Newell，Shaw，Simon1956年，Thelogictheorymachine(逻辑理论机).数学定理证明程序(LogicTheorist)mimichumanreasoning《数学原理》第二章中的38个定理1963年，经过改进的LT程序在一部更大的电脑上，最终完成了第二章全部52条数学定理的证明。6王浩1958年，IBM704电脑，3-5分钟，证明了《数学原理》中有关命题演算的全部220条定理。1959年，8.4分钟，证明了《数学原理》中全部（350条以上）定理。罗素：“我真希望，在怀特海和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种

4、可能。”1983年获得首届自动定理证明里程碑奖。7四色定理1852年，一位21岁的大学生提出来的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。8四色定理1976年7月，美国的阿佩尔(K.Appel)等人合作解决了长达124年之久的难题--四色定理。他们用三台大型计算机，花去1200小时CPU时间，并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。《伊利诺斯数学杂志》第21卷刊载的检验表(460p)9三类方法基于归结的方法类人的方法(humansimulation)判定方法10基于归结的方法1960年，Gilmore在计算机

5、上实现了Herbrand算法。1960年，M.Davis和H.Putnam的改进：TautologyRule,One-literalRule,Pure-literalRule,SplittingRule。技巧而非本质：枚举基替换。1960年，D.Prawitz直接寻找替换，避免组合爆炸。思想深刻，效果不理想。1965年，J.A.Robinson提出归结原理One-literalRule的扩展。11效率的提高1965：Wos,G.A.Robinson,Curson,支持集归结；1967：Slagle，语义归结；1970：Loveland，Luckham，线性归结；1971：Bo

6、yer，锁归结；1978：刘叙华，锁语义归结；1979：王湘浩，刘叙华，广义归结；12类人的方法(humansimulation)1956年，Newell，Shaw，SimonThelogictheorymachine(逻辑理论机)1966年，MIT的L.M.Norton建造了ADEPT系统群论的定理证明系统；启发式；1972年，R.Boyer和J.Moore启发式策略和人机交互；质因子分解唯一定理，验证编译程序的正确性；1977年，Bledsoe：《Non-ResolutionTheoremProving》(非归结定理证明)13判定方法在较小的范围内找到一个有效的判定方法；

7、早期工作：A.Tarski的初等代数和初等几何的方法。王浩：命题逻辑的一个有效的判定方法。吴文俊：吴方法(1977)。14吴方法平面几何定理几何问题->代数问题1959年，Gelernter提出几何定理证明机(GeometryTheoremProvingMachine,GTM)反向推理；直线图形中大部分高中考试的问题；运行时间与高中学生做题时间差不多；获国际Herbrand自动推理杰出成就奖“吴的工作将几何定理证明从一个不太成功的领域变为最成功的领域之一。在很少的领域中，我们可以将定理机器证明归于一个人