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

Mechanical Demonstration for a Class of Elementary Geometric Theorems

作　　者：谭红艳[1,2] 吴尽昭[1,2] 

机构地区：[1]兰州大学计算机科学系 [2]北京大学数学系

出　　处：《兰州大学学报（自然科学版）》1997年第3期31-36,共6页Journal of Lanzhou University(Natural Sciences)

摘　　要：对一类初等几何定理，通过根理想的分解，给出了一种机械化方法，利用这种方法，可恰好同时获得所有的不可约特征列．因而一类几何定理是一般真确的当且仅当其终结多项式对这些不可约特征列的余式为零．By decomposing a radical ideal, a method can be given to obtain all the useful irreducible characteristic sets. Then, a geometric theorem is generally true if the remainders of the conclusion polynomial to these characteristic sets are zero.

关 键 词：机械化证明 初等几何 几何定理 机器证明 

分 类 号：O123[理学—数学]