归结原理不.ppt

人工智能原理第 四 讲 归结原理 周日贵 华东交通大学信息工程学院 归结原理 4.1 引言 4.2 一阶逻辑 4.3 子句形 4.4 Herbrand定理 4.5 置换与合一 4.6 归结原理 4.7 归结法的完备性 4.8 归结策略 4.1 引言 自动定理证明 历史 四色定理 三类方法 自动定理证明 Automated Theorem Proving(ATP) 定理机器证明(Mechanical Theorem Proving) 为什么？ 定理证明是一种智能行为； 体现了人类的逻辑推理能力； 推理用计算来实现 Leibniz的梦想： Leibniz imagined a universal formal calculus which could express reasoning in any subject, and an algorithmic procedure which could be applied to decide truth of statements in this calculus. 1930年，Herbrand定理。 半可判定问题。 一阶逻辑的判定问题。 在一阶逻辑中，有没有方法可以判断任何一个命题是否定理？(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。 数理逻辑的基本问题。 1936年，证明基本问题是不可解的。 在一阶逻辑中，如果一个定理是正确的，则有一个机械的方法在有限步内证明它。 一阶谓词逻辑有很强的表达能力，凡可计算的函数就可由一阶谓词表达。 历史 Newell，Shaw，Simon 1956年，The logic theory machine(逻辑理论机). 数学定理证明程序(Logic Theorist) mimic human reasoning 《数学原理》第二章中的38个定理 1963年，经过改进的LT程序在一部更大的电脑上，最终完成了第二章全部52条数学定理的证明。 王浩 1958年，IBM704电脑，3-5分钟，证明了《数学原理》中有关命题演算的全部220条定理。 1959年，8.4分钟，证明了《数学原理》中全部（350条以上）定理。 罗素：“我真希望，在怀特海和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。” 1983年获得首届自动定理证明里程碑奖。 四色定理 1852年，一位21岁的大学生提出来的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。 四色定理 1976年7月，美国的阿佩尔(K.Appel)等人合作解决了长达124年之久的难题--四色定理。他们用三台大型计算机，花去1200小时CPU时间，并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。 《伊利诺斯数学杂志》第21卷刊载的检验表(460p) 三类方法 基于归结的方法 类人的方法(human simulation) 判定方法 基于归结的方法 1960年，Gilmore在计算机上实现了Herbrand算法。 1960年，M.Davis和H.Putnam的改进： Tautology Rule, One-literal Rule, Pure-literal Rule, Splitting Rule。 技巧而非本质：枚举基替换。 1960年，D.Prawitz 直接寻找替换，避免组合爆炸。 思想深刻，效果不理想。 1965年，J.A.Robinson提出归结原理 One-literal Rule的扩展。 类人的方法(human simulation) 1956年，Newell，Shaw，Simon The logic theory machine(逻辑理论机) 1966年，MIT的L.M.Norton建造了ADEPT系统 群论的定理证明系统； 启发式； 1972年，R.Boyer和J.Moore 启发式策略和人机交互； 质因子分解唯一定理，验证编译程序的正确性； 1977年，Bledsoe： 《Non-Resolution Theorem Proving》(非归结定理证明) 判定方法 在较小的范围内找到一个有效的判定方法； 早期工作： A.Tarski的初等代数和初等几何的方法。 王浩：命题逻辑的一个有效的判定方法。 吴文俊：吴方法(1977)。 吴方法 平面几何定理 几何问题-代数问题 1959年，Gelernter提出几何定理证明机(Geometry Theorem Proving Machine, GTM) 反向推理； 直线图形中大部分高中考试的问题； 运行时间与高中学生做题时间差不多； 获国际Herbrand自动推理