Mass production of Theorems of Elementary Geometry and its Application

在前期的研究中，我们得到了大量生成元素几何定理的计算机程序。程序中使用了根岑逻辑演算系统LK的几个推理规则。为了得出有用的定理，我们需要许多几何公理。在初中数学教科书中，出现了大约二十个几何公理。但是许多其他的命题被间接地用来证明几何问题。本研究的目的是找出这些命题，并将它们作为几何公理。起初，我们在谈话和学校课堂上几何问题的解法中寻找它们。其次，我们在旧教科书中查找它们，这些教科书对几何证明的描述是精确的。我们得到了50多个几何公理。利用这些公理，我们可以得到一些有用的初等几何定理。

In our previous research, we got the computer program of the mass production of the theorems of the elementry geometry. The several inference rules, of Gentzen's logical calculus system LK were used in the program. To product the useful theorems, we need many geometrical axioms. In the mathematical textbooks of junior high school, about twenty geometrical axioms appear. But many other propositions used indirectly to prove the geometrical problems. The purpose of this research is to find those propositions and use them as the geometrical axioms. At first, we searched them in the talking and the solutions to the geometrical problems in the school lessons. Secondly, we searched them in the old textbooks whose descriptions of the geometrical proofs were precise. And we got over fifty geometrical axioms. Using these axioms, we can get the useful theorems of elementary geometry.