Fast Theorem-Proving and Wu's Method  

作　　者：李廉 王继民 

机构地区：[1]DepartmentofComputerScience,LanzhouUniversity,Lanzhou730000,P,R.China [2]DepartmentofComputerScience,Lan

出　　处：《Journal of Computer Science & Technology》1999年第5期481-486,共6页计算机科学技术学报（英文版）

摘　　要：In this paper, the possibility of fast algorithm is discussed for me-chanical theorem proving, where the degeneracy condition are considered in designingof these algorithms. It is found that all of the methods depend seriously on some prin-ciples appearing in Wu's Method. In other words, some principles in Wu's Methodare the instinctive properties in these new fast algorithms of theorem proving.In this paper, the possibility of fast algorithm is discussed for me-chanical theorem proving, where the degeneracy condition are considered in designingof these algorithms. It is found that all of the methods depend seriously on some prin-ciples appearing in Wu's Method. In other words, some principles in Wu's Methodare the instinctive properties in these new fast algorithms of theorem proving.

关 键 词：fast theorem proving Wu's Method degeneracy condition generic case approximate theorem-proving 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]