几何定理机器证明的WE完全方法  

WE COMPLETE ALGORITHM FOR AUTOMATED THEOREM PROVING

作　　者：张景中[1] 杨路[1] 侯晓荣[1] 

机构地区：[1]中国科学院成都计算机应用研究所

出　　处：《系统科学与数学》1995年第3期200-207,共8页Journal of Systems Science and Mathematical Sciences

基　　金：国家自然科学基金

摘　　要：在几何定理机器证明的各种方法中，吴氏方法获得了显著的成功．如预先把有关代数簇分解为不可约簇，则吴氏方法可成为完全方法．本文在吴法的基础上，以辗转伪除法为辅助工具，发展出一种不必预先分解代数簇的完全方法，并给出一些手算实例．In this paper, we propose an algorithm, which need not do decomposition of an algebraic set into the union of its irreducible varieties, to overcome the so-called 'reducibility difficulty' in automated theorem proving. Employing Wu's division and Euclid's algorithm, we call it WE algorithm.

关 键 词：机器证明 辗转伪除法 几何定量 WE完全法 

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