几何定理可读证明的自动生成

用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题，自１９９２年以来有了突破性进展．对于一大类欧氏几何命题──构造性几何命题，已有了相当有效的算法．基于此算法所编制的程序，已证明了５００多条非平凡的几何命题．对其中大多数命题，机器自动生成的证明是简明而易于理解的．本文是对这一领域近三年来取得的进展的综述．包括了在非欧几何可读证明方面的最新成果．

基于前推法的几何信息搜索系统

我们提出并实现了几何信息搜索系统（ＧＩＳＳ），它可用于找出所给几何图形的＂所有＂性质．记ＧＰ为一给定的几何谓词之集，ＬＭ为涉及ＧＰ中谓词的某些几何引理之集．若ＬＭ中的引理不引入新的几何元素，则用ＧＩＳＳ能找出所有能由ＬＭ中引理推出的几何性质．由于适当选择谓词和引理，合理组织数据和优化推理过程，对平面欧氏几何成功地实现了ＧＩＳＳ．它可以用于发现非平凡的几何性质，也可以作为其它几何定理机器证明系统的辅助工具使证明更为优美、简短和传统化．文末给出了几个例子和对１６１个几何问题运行的统计数据．

任意升列的维数

不可约代数簇的维数是Ritt-吴构造性代数几何理论中的一个关键概念。本文将证明任意升列的维数确有几何意义,并证明任意升列维数的概念可以用于提高Ritt-吴分解算法的效率并可用来将一任意代数簇分解为齐维代数簇。 1 任意升列的维数设k为一特征为零的域,k[y_1,…,y_n]或[y]为变量)y_1…y_n的多项式环。若不特别说明,本文中所有多项式都在k[y]中。一多项式P可以写为P=a_ry_c^r+…+a_0,其中a_i为y_1…,y_(c-1)的多项式。我们称P的类为c,记为class(P)=c;a_r称为P的初式。