例证法

书籍:现代科技综述大辞典上 更新时间:2018-09-11 01:55:40

出处:按学科分类—自然科学总论 北京出版社《现代科技综述大辞典上》第120页(2735字)

通过数值实例的检验证明几何定理的思想与方法,即用举例的方法证明数学定理。

它不仅是理论上的探讨,而且确实能用在计算机上或通过手算证明相当难的几何定理,人们还用它发现了一些新定理。

例证法是在吴文俊数学机械化理论与方法的影响之下,由中国数学家在80年代首先提出的。1986年,洪加威在加拿大多伦多举行的第27届国际电脑科学基础会议上,作了题为《能用举例的方法证明几何定理吗?》的学术报告,最早得出用举例的方法足以证明几何定理(即单点例证法)。

1989年张景中和杨路正式提出了另一种更有实用价值的例证法即数值并行法(也称多点例证法)。

其实这两种方法的基本思想,大体上都是在1984年产生的。这以后侯晓荣于1990年在天津计算数学会议上又报告了另一种例证法。

但是最实用的是数值并行法。这3种例证法都是分别基于以下3个定理。

定理1. 设f(x1,x2,…,xm)是x1,x2,…,xm的多项式,它关于xk的次数不大于nk,对应于k=1,2,…,m,取数组ak,l(=0,1,…,nk)使得l1≠l2时,有ak.l≠ak,l

,如果对任一组{l1,…,lm,0≤lk<nk},都有f(a1,l1,…,am,lm)=0.则f(x1,x2,…,xm)是恒为零的多项式。

定理2. 设f(x1,x2,…,xm)是x1,x2,…,xm的多项式,它关于xk的次数不大于nk,1≤k≤m,又设它的标准展式中非零系数的绝对值不大于L,不小于S>0,如果变元的一组值,…,满足

则有

定理3. 设f(x1,x2,…,xm)是x1,x2,…,xm的整系数多项式,它关于xk的次数不超过nk,又设p1,p2,…,pm是m个互不相同的素数,则当取时,只要f不恒为零,总有

着眼于多项式根的个数所得到的定理1,提供了可以证明的几何定理例证法即数值并行法;着眼于多项式根的界限的定理2,就提供了单点例证法;而着眼于多项式根的性质的定理3,则提供了侯晓荣例证法。

数值并行法可以证明代数恒等式,也可以证明能化成代数恒等式的几何命题。对于代数恒等式的证明,首先要估计f(x1,x2,…,xm)关于各个变元x1,x2,…,xm的次数的上界。

其次是确定用哪些数值代入检验,这时已估计好了xk的次数不超过nk,那就让xk这个变元取nk+1个不同值。

nk+1个不同的值ak,0,ak,1…,ak,nl组成有限集Ak,k=1,2,…,m。

从A1,A2,…Am中各取一个,便凑出一组(x1,x2,…xm)的值;一共可凑出(n1+1)(n2+1)…(nk+1)个数组来。这样的数组集称为格阵。

最后将这每组值都代入f(x1,x2,…,xm)加以检验。若每组值都使f=0,便证明f(.x1,x2,…,xm)恒等于零。

对于几何定理的证明步骤和思路如下:第1步,利用取坐标或三角函数,把问题表成代数形式:在一组代数等式条件下,问另一代数等式是否成立。第2步,设想利用假设条件消去结论等式中的约束变元,使结论转化为只含自由变元的代数方程,估计此代数方程关于各变元的次数以确定格阵规模(并不真的写出这个方程)。第3步,根据格阵规模取自由变元的若干组数组,检验命题对于这些具体数值是否成立。如果都成立,则表明第2步中的代数方程为恒等式,从而命题为真。

第2步中的消去约束变元得到一个只含自由变元的代数方程,是总能办到的,这可由吴-Ritt整序原理保证。

单点例证法的思想,是对于一个数学命题,可以通过给出一个数值例子,使该命题成立的充要条件是该命题对该特例成立。在计算检验这个具体例子的时候,需要进行加、减、乘、除、开方等等,一定会有误差。如果最后的等式判断语句中,等号两边之差非常接近零,那么我们可根据一些裂缝定理,说明如果一个数学等式判断语句两边的差小到一定程度之后,就说明绝对等于零。在证明代数恒等式时,对于一元代数恒等式的证明则需要举一个足够大的数值例子;而对于一个多元代数恒等式的证明,这个数值例子要涉及很大的变元数值。如按定理2,有,这表明运算涉及的有效数字之长正比于。而作一次乘法,运算工作量正比于有效数字长度的平方,即。显然当变元数目稍多时,将涉及很大的数值计算,这在计算机上难以实现。

但它所引出的观念的确是美妙而吸引人的,也引起了国际数学界同仁的很大兴趣。

很有研究前景的数值并行法用于机器证明,还有许多变化与发展:(1)单点例证法与数值并行法可以结合使用,对某些变元用单点法,另一些变元用数值并行法。(2)数值并行法与吴-Ritt除法可以结合使用,先消去一些变元,再对剩下的约束变元用并行法。这样可对不同的问题寻找组合优化的证法。

(3)既然吴-Ritt除法可以把“条件等式”问题化为“自由变元恒等式”问题,那么,任一种检验代数恒等式的数值方法都可以和吴-Ritt除法结合起来形成几何定理机械化证明的数值算法。这已超出了例证法的范围,但仍可以用数值并行法。(4)数值并行法还可以用来证明几何不等式这一机器证明中的难点,但这有待于进一步研究。

【参考文献】:

1 吴文俊.中国科学,1977,6:507

2 洪加威.中国科学(A辑),1986,3:234~242

3 洪加威.中国科学(A辑),1986,3:225~233

4 邓光克.科学通报,1988,24:1851

5 张景中、杨路,数学认识与实践,1989,1:34~43

6 Zang J,Yang L,Deng M.Theoretical Computer Science,1990,74:253

7 张景中.自然杂志,1991,1:55~62

(安徽机电学院王庚副教授撰;胡炳生审)

分享到: