权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Mass production of Theorems of Elementary Geometry and its Application

初等几何定理的量产及其应用

基本信息

批准号：
12680184
负责人：
OKAZAKI Hiromitsu
金额：
$ 0.7万
依托单位：
Kumamoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2000
资助国家：
日本
起止时间：
2000 至 2001
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-12680184/
关键词：
elementary geometry proof problem inference rule automatic proof 初等幾何定理

项目摘要

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.

在我们以前的研究中，我们得到了元素几何定理的批量生产的计算机程序。程序中使用了Gentzen的逻辑演算系统LK的几条推理规则。为了产生有用的定理，我们需要许多几何公理。在初中数学教材中，大约出现了二十条几何公理。但许多其他命题也间接地被用来证明几何问题。这项研究的目的是找到这些命题，并将它们用作几何公理。首先，我们在课堂上对几何问题的对话和解答进行了探索。其次，我们在对几何证明描述精确的旧教科书中进行了检索。我们得到了50多条几何公理。利用这些公理，我们可以得到一些有用的初等几何定理。