一类初等几何定理的机械化证明

《一类初等几何定理的机械化证明》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、DOI:10.13885/j.issn.0455-2059.1997.03.008兰州大学学报(自然科学版),1997,33(3):31～36JOURNALOFLANZHOUUNIVERSITY(NaturalSciences)一类初等几何定理的机械化证明谭红艳吴尽昭(兰州大学计算机科学系,730000兰州)(北京大学数学系,100871北京)摘要对一类初等几何定理,通过根理想的分解,给出了一种机械化方法,利用这种方法,可恰好同时获得所有的不可约特征列.因而一类几何定理是一般真确的当且仅当其终结多项式对这些不可约特征列的余式为零.关键词根理想不可约特征列余式几何定理的一般真确性中图

2、法分类号TP3010前言几何定理证明的机械化思想,可追溯到十七世纪的笛卡儿时代,解析几何的出现,使得几何的问题可以用代数的方法来处理.这样就避免了欧几里德那种几何证法所需的高度技巧.但是,既使几何定理的证明完全化成代数问题,仍还有一些难以克服的困难.例如,代表几何关系的那些代数关系往往是杂乱无章的,而且计算量极大.由于计算机的出现,繁杂的计算基本上已不成问题,最关键的问题就是如何处理那些代数关系.[1]1960年,Gelernter等,基于欧几里德的传统证法,最先研究了几何定理的机械化证法,[2,3]但也只能证明一些极其平凡的定理.此外,早在1950年,Tarski与Seidenb

3、erg等人也给出了完整地进行几何定理机器证明的代数方法,指明了几何数域为实闭域的几何定理机器证明的可能性.但这些方法远不是切实可行的,根本无法证明非平凡的几何定理.直至1977年,吴文俊发明了一种方法(吴方法),这种方法十分有效,大量往往需要高度技巧和智能才能证明的所谓等式型的几何定理,用此方法能够很容易地得到证明.从而避免了Tarski方法效率过低这一问题.其基本思想是:首先,将几何定理的证明化为纯代数问题;其次,将定理的假设部分的代数关系式按一定的顺序加以整理和运算,判定定理的终结部分是可从已整理过的代数关系[4,5]式中推出;最后,编制程序在计算机上实施.在假设部分的代数关系

4、式的整理与运算过程[6]中,每次加入一个新的代数关系式时,这个过程必须重新进行.本文对一类几何定理给出了一种机械化方法,应用这种方法,可同时一次获得最后所需要的全部不可约特征列,而不需重复地进行整序.第二节是预备知识,罗列了一些下节需要用到的基本概念和结论;第三节是本文的中心部分,对于一类满足某一条件(当然,这一条件是否满足是可判定的)的几何定理,利用根理想的分解,给出了判定这种几何定理是否一般真确的算法;最后,简单地讨论了多项式组的特征列及非退化条件的选取.收稿日期:1995-06-17.谭红艳,25岁,女,硕士生.32兰州大学学报(自然科学版)第33卷1预备知识假设读者熟悉交换

5、代数及吴方法中的基本概念和结论.例如,多项式,环,域,理想,素理想,根理想,维数以及零点,母点,类,序,升列,初式,特征列,不可约特征列与一般真确的几何定理等概念以及有关结果.对此,读者可参阅文献[5,7].下面仅列出几个我们需要直接使用的结论.设R是UFD,并且有一机械化方法分解R中的元素.又设K是R的商域,K的特征为零,K[x1,…,xn]是域K上的以x1,…,xn为变元的多项式环.定理1.1有一机械化方法可在有限步内将K[x1,…,xn]中的多项式进行因式分解.定理1.2设T是K上的代数元,则有一机械化方法在有限步内可将K(T)上的以x为变元的多项式环K(T)[x]中的多项式

6、进行因式分解.假定变元x1,…,xn的序已确定,A1,…,Ak∈K[x1,…,xn]是一个升列.I1,…,Ik分别是A1,…,Ak的初式,对任意的多项式g∈K[x1,…,x7],首先令g对Ak关于Ak的主变元作伪除法,获得余式Rk-1,这样一直作下去,最后,R1对A1关于A1的主变元作伪除法,余式为R0.显然,存在非负整数s1,…,sk与多项式Q1,…,Qk∈K[x1,…,xn],使得sskI11…Ikkg=Q1A1+…+QAk+R0,并且Aj的主变元在R0中的次数小于它在Aj中的次数(j=1,…,k).我们记余式R0为prem(g,Ak,…,A1).定理1.3(整序原理)令΢={

7、h1,…,hm}是K[x1,-,xn]中的一个有限非空多项式集,I是΢生成的K[x1,…,xn]中的理想.则有一机械化方法可在有限步内获得一升列C,使得或者C仅由一个K∩I中的多项式组成;或者C={A1,…,Ak}(k≥1),A1的类大于零,A1,…,Ak∈I,并且prem(hi,Ak,…,A1)=0,(i=1,…,m).其实,上述升列C的获取只需按一定的顺序重复地作伪除法,而且这一过程最后终止.详细证明请参考文献[7].2几何定理一般真确性的判定设(S)是个等式型的