摘要
在几何定理机器证明的各种方法中，吴氏方法获得了显著的成功．如预先把有关代数簇分解为不可约簇，则吴氏方法可成为完全方法．本文在吴法的基础上，以辗转伪除法为辅助工具，发展出一种不必预先分解代数簇的完全方法，并给出一些手算实例．
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.
出处
《系统科学与数学》
CSCD
北大核心
1995年第3期200-207,共8页
Journal of Systems Science and Mathematical Sciences
基金
国家自然科学基金
