初等几何判定问题与机械化证明

机械化证明定理,目前值得注意的是Tarski关于初等几何与初等代数定理的机械证明法。他以及后来一些研究工作者的方法,大都基于Sturm定理的某种推广,这些方法仍极繁复,因之即使使用了计算机,实际上也是难以实现的。本文的目的,在于把定理限制在不牵涉到“之间”关系的情形,应用完全不同的原理给出初等几何定理的机械化证法。这种方法仅用手算即可给出不太简单的定理的证明。