机器证明法

我们知道，公理化体系的几何证明是手工的，一个难度较大的几何证明题，往往要经过冥思苦想，为找规律，有时还要添加辅助线，学习者常叫苦连天，而采用机器证明，让机器代替人的部分劳动，进行自动推理，速度快，说理简单明了，这是人们所期望的，更是学术界长期研究的课题，是现代人工智能发展的重要方向.

1977年，吴文俊在中国古算研究的基础上，分析从古希腊到笛卡儿思想的特点，创造出几何机器证明的现代化数学分支，这个数学新领域将数学证明问题归结为纯代数问题，经过几十年的发展，取得了许多丰硕成果，从而开辟了一条定理机器证明的代数化途径，计算机成为数学研究必不可少的工具的时代已经开始.

吴文俊在《几何定理机器证明的基本原理》中证明了这样的事实: 若一种几何的附属系数是一个数域，则假设和结论都可由多项式代数方程来表达的一类定理的证明都可以机械化. 这就是说，凡是假设和结论部分的代数关系式都可用多项式方程来表示的定理，就可用机械化证明. 这是“吴方法”的基本原理. 按照“吴方法”，机器证明可分三个步骤: ①把几何问题化为纯代数问题. 具体做法是，用解析几何方法建立坐标系并设未知量，将条件表示成所设未知量的多项式方程组G1，将求证表示成多项式方程组G2; ②代数结论机械化. 即用一定的算法判断G2是否可以由G1推出，这是机器证明的核心步骤; ③程序化操作. 依据②中所确定的步骤编程序，在计算机上实施，得出最后结论. 不过，按传统计算是相当麻烦的.

例 求证: 直角三角形斜边上的高是斜边两线段的比例中项

首先，建立直角坐标系，如图2.11所示.

其次，将已知条件代数化:

AD⊥BC，斜率互为负倒数:，x1u1-x2u2=0

图2.11

即 h1(u1，u2，x1，x2) =x1u1-x2u2=0

直线BC方程为=1，D点在BC所在直线上:

=1. 整理得 h2(u1，u2，x1，x2) =u1x2+u2x1-u1u2=0

求证|AD|2=|CD|·|BD|.这里，|AD|=，|CD|=|CD|·|BD|=

即 整理得:

g1(u1，u2，x1，x2)=［+(x2-u2)2］［(x1-u1)2+］-()2=0.于是有G2:g1(u1，u2，x1，x2)=0.即G1⇒G2.