一类构造性几何不等式的机器证明  

Automated Proving for a Class of Constructive Geometric Inequalities

作　　者：杨路[1] 夏时洪[2] 

机构地区：[1]广州大学软件研究所 [2]中国科学院计算技术研究所,北京100080

出　　处：《计算机学报》2003年第7期769-778,共10页Chinese Journal of Computers

基　　金：国家"九七三"重点基础研究发展规划项目 (NKBRSF G19980 3 0 60 2 );中国科学院知识创新工程基金资助

摘　　要：阐述了一个基于胞腔分解的不等式证明算法 .据此算法编制的Maple通用程序能有效地处理含有根式的不等式型定理 ,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效 .An automated inequality-proving algorithm is presented based on a mixed method including a so-called cell-decomposition. That is implemented by a Maple program named BOTTE-MA which can prove or disprove propositions in an extensive class of geometric and algebraic inequalities involving radicals. Most of the theorems in Geometric Inequalities written by Bottema et al., can be proven efficiently in this way.

关 键 词：构造性几何不等式 机器证明 自动证明 半代数系统 

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