几何定理机器证明.pdfVIP

维普资讯 穗 自然科学进展—— 国家重点实验室通讯 第 1期 专题评述 ， ，一 几何定理机器证明 吴文俊 (二)， {中国科学院系统科学研究所 ，北京100080) 关键词：机器证明，数学机撼化 ，啊 一 、 几何定理证明——从Euclid，Descartes到Hilbert 定理证明是现代纯粹数学的主要活动形式，导源于古希腊，Euclid的 《几何原本》是其 代表著作．即使是平面欧氏几何，就有着无数美妙的定理，以下略举数例，以资说明． 例 1．Feuerbach定理(1822)．三角形的九点圆与其内切圆 D 以及傍切圆都相切． 例2．Morley定理 (1900)．三角形三个角的相邻三分角线相交成一个等边三角形． 例3．Thebault推测(1938)．设三角形ABC，L是过顶点 的一直线，则在与底边BC， 直线工，以及三角形外接圆相切的诸圆中，有两圆其 中心联线经过三角形的内心或傍心． 按照通常的Euclid模式，几何定理的证明，是依据公理系统，按逻辑规则演绎地进行的． 每一个别的定量，其证明只能适合于这一个别的定理．证明没有通用的思想指导，需要有高度 的聪明技巧与迂回曲折的推理才能获得．往往表面看来极为平凡的定理，其证 明却极其困 难．下面是一个著名的例子，所述定理在 19世纪时曾一度难倒了许多著名的几何学家． 例 4． 分角线定理．有两个内分角线相等的三角形必等腰． 顺便指出，以上这些定理在叙述上都有不够完全与模棱两可之处必须加以澄清．这在以 后将再加讨论． 在 1637年出现了Descartes的 《几何学》，1899年又出现 了Hilbert的 《几何基础》．这 两部经典著作为几何定理的证明提供 了不同于 Euclid模式的可能性 Decsartes开创 了可 用计算来证明几何定理的局面，而Hill~rt则指出了几何定理可以不是逐一证明，而是一类定 理可以用统一的同一方法一起证明．这一统一的方法，在引人适当的坐标后，也可仅仅用计算 来完成，而计算的过程，则可依事先确定的步骤，即今 日所称的算法，按步进行以迄于成．应该 指出的是，并没有先验的理由来保证这样的算法必然存在，算法的存在与否，其本身也需加以 证明．在这样的算法确实存在时，我们将称这类定理的证明是可以机械化的，或简单地说这一 类(定理)是可以机械化的．相应的算法则称为这类定理的一个机械化证明．至于算法存在这 一 事实，则称为一个机械化定理． Hilbert的思想，已发展成一个新的数学领域：数理逻辑．无数数理逻辑学家，曾致力于各 本文 1991年8月 】日收刊． 本文及所引述的MMC论著部分受刊国家 自然科学基金资助 维普资讯 自然科 进展—— 国家重点实验室通讯 1992年 种类型定理的机械化证明．其中最值得称道的成就之一，是Tarski所发现的一个定理，依据 我们所用的辞汇，这一定理可表述如下． Tarski机械化定理 (1950)． 通常的Euclid几何是可以机械化的． 随着计算机的出现，自然引起如何将一已由某一机械化定理已保证存在的算法，转化为程 序使之可在计算机 七实现的问题 这方面的一位先驱者是王浩，他在计算机上只用了数秒钟 的时间，将Whitchead·Russell数学原理一书中的350个以上的命题一举证明．至于Tarski 的机械化算法，则由于过于复杂，尽管后来有各种改进与简化，迄今仍未听说有何值得称道的 定理 曾获证明． 二 、几何定理机器证明的一个有效算法 在 1976至 1977年之交，作者发现了对某一类非平凡几何定理的机械化证明方法．为了说 明这一方法，先考虑一个特例，例如例 l中的Feuerbac