Mass production of Theorems of Elementary Geometry and its Application

在前期的研究中，我们得到了初等几何定理的批量生产的计算机程序。程序中使用了根岑逻辑演算系统LK的几条推理规则。为了得出有用的定理，我们需要许多几何公理。在初中数学教材中，几何公理约有20条。但也有许多命题间接地用来证明几何问题。本研究的目的是找出这些命题，并将它们作为几何公理。首先，我们在课堂上的几何问题的讨论和解答中寻找它们。其次，我们在旧的教科书中寻找它们，它们对几何证明的描述是精确的。我们得到了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.