Hilbert 机械化定理表明,Pascal 几何中构造型交点定理可以机器证明。1982年,吴文俊教授给出了机械化定理的构造性证法。本文指出,通过添加若干新的构造类型,有更广泛的一类平面几何定理,其机器证明可以按照同样的构造性证法实现,我们称这类定理为构造型几何定理。作者适当调整吴文俊算法的步骤,在 HP1000小型计算机上建立了构造型几何定理的机器证明系统,效率大大提高,从而成功地证明了许多不平凡的几何定理,并且独立发现了相当深入的结果。

In this paper,we point out that Hilbert's Mechanization Theorem may be extended to allconstructible theorems which can be mechanically proved in the same way by adjoining somenew constructive types.Using the Theorem-Prover built by the authors in rearranging thesteps of Wu's algorithm,many non-trivial theorems have been proved and some new resultshave also been discovered independently.