求证:菱形对角线互相垂直

hbghlyj

几何定理的机器证明, 自1945年出现了第一台电子计算机之后更是激起人们的关注.1948年, 波兰人Tarski解决实闭域初等几何定理可以机械化的证明 (见A.塔尔斯基, J.C.C.麦克铿, 初等代数和几何的判定法.北京:科学出版社, 1959, 陆钟万译) 用的是数理逻辑法, 虽然也给出实现这些证明的建议, 但离实现非常遥远, 并非切实可行.

1959年, 王浩设计一种方法, 用计算机证明了罗素的《数学原理》中几百条定理, 仅用9分钟, 引起轰动, 一时机器证明前景似乎非常乐观.当时人们猜测再过十年计算机将证明发现新定理.然而实践上人们碰到困难, 1976年美国做了大量实验, 塔尔斯基的初等几何, 用计算机证明一些近于同义反复的“儿戏”式的“定理”, 例如“若P₁, P₂, P₃, P₄, P₅五个点之中, P₁, P₂, P₃和P₁, P₂, P₄和P₁, P₂, P₅各在一条直线上, 则P₃, P₄, P₅也在一条直线上”. (见Kister, K.IEEE Trans on Computers C-25 (1976) , 328-334) .于是人们又走向悲观的一面, 有些专家估计:靠机器再过100年, 也未必能证明出多少有意义的新定理.

如前所述初等几何和初等代数的判定问题早在50年代就为塔尔斯基 (A.Tarski) 所解决, 但其复杂度远远超越了现代计算机的能力范围.总之, 几何定理由计算机自动地证明, 于20世纪五十年代由 Herbert Gelernter 开始研究. 在自动推理领域先驱性的工作, 是由数学机械化思想的倡导者吴文俊院士于70年代作出的, 这就是著名的几何定理机器证明的吴方法, 是第一个可以证明非平凡定理的系统的机器证明方法.

吴方法主要分两步.第一步是引进坐标.然后把需证定理中的已知条件与结论部分都用坐标间的代数关系来表示.我们所考虑的初等几何定理局限于这些代数关系都是多项式等式关系的范围.

例如, 有若干个点A_i (x_i, y_i) , 用 \[\left(x_1-x_2\right)\left(y_3-y_4\right)-\left(x_3-x_4\right)\left(y_1-y_2\right)=0\] 表示A₁A₂平行 (或重合) 于A₃A₄; \[\left(x_1-x_2\right)\left(y_1-y_2\right)+\left(x_3-x_4\right)\left(y_3-y_4\right)=0\] 表示A₁A₂垂直于A₃A₄; \[\left(x_1-x_2\right)^2+\left(y_1-y_2\right)^2-r^2=0\] 表示A₁A₂长度为$r$

第二步是消元.通过代表假设的多项式关系把代表结论多项式中的坐标逐个消去, 如果消元的结果为零, 即表明定理正确, 否则再作进一步检查.这一步完全是代数的, 即用多项式的消元法来验证.这一步完全可以通过计算机来完成.

例1 求证:菱形对角线互相垂直

如图1, 将A放在原点, 则B的坐标为 (u₁, 0) , 表明B是任意给定的 (u₁为参数) , 由菱形定义, AB=BC, 故C仅有一个任意参数u₂, 而D点, 两个坐标都是未知的, 即D (x₂, x₁) , 由AD//BC, 类似 (1) 的方法得$x_1(u_2-u_1)-x_2x_1=0$, 又由 (3) 的方法AB=AD得$u_1^2-(x_2^2+x_1^2)=0$,
将这两个方程整理并三角型化 (即第一方程仅有一个未知量x₂, 第二方程有两个未知量x₁, x₂)
用Mathematica软件的语句, 将已知条件方程左边的多项式记为:

$$f_1=-x_2+\left(u_2-u_1\right) ; f_2=-\left(x_1^2+x_2^2\right)+u_1^2$$ 求证:AC⊥BD, 由类似 (3) 的方法, 它的方程左边多项式为: $$g_1=x_1^2+u_2\left(x_2-u_1\right)$$ 现在做逐次除法, 即g₁除以f₂ (以x₁为未知量) 得余式.用r2=PolynomialRemainder[g1,f2,x1]得 $$u_1^2-u_1 u_2+u_2 x_2-x_2^2$$ 即 $g_1=c_2f_2+r_2$（$c_2$ 为非0的商）再用 $r_2$ 除以 $f_1$（以 $x_2$ 为未知量）它的余式用r1＝PolynamialRemainder[r2,f1,x2]得$r_1=0$. 又$g_1=-f_1+(x_2-u_1)f_2+r_1$.

由于r₁≡0, 从f₁=0, f₂=0推出g₁=0, 定理被证明.

一般的初等几何定理的假设条件表示为多元多项式方程组 ($k=r+s$维仿射空间中代数族) \[\begin{cases}p_1(u_1\cdots,u_r,x_1,\cdots,x_s)=0\\p_2(u_1,\cdots,u_r,x_1,\cdots,x_s)=0\\\cdots\cdots\\p_s(u_1,\cdots,u_r,x_1,\cdots,x_s)=0\end{cases}\qquad(4)\]

其中u₁, …, u_r是独立的参变量, x₁, …, x_s不是独立的变量.

定理的结论表示为$g(u_1,\cdots,u_r,x_1,\cdots,x_s)=0.$

将 (4) 化为三角形方程组 \[\begin{cases}f_1(u_1,\cdots,u_r,x_1)=0\\f_2(u_1,\cdots,u_r,x_1,x_2)=0\\\cdots\cdots\\f_s(u_1,\cdots,u_r,x_1,\cdots,x_s)=0\end{cases}\qquad(5)\]

剩下的问题是用计算机去求g与f_s两个多项式的除法所得的余式 (也是一个多项式) R_s, 再除以f_s-1, 再得余式R_s-1, 例如, 此过程可以用 Mathematica 软件中的命令

R_i=PolynomialRemainder[R_i+1, f_i, x_i]来实现, R_s+1=g, i=s, s-1, …, 1.

如此继续下去, 直到最后的余式R₁, 如果R₁=0, 则定理得证.