Coqによる初等幾何学の証明方法について

摘要

初等幾何学を指導する知的教育システムの研究は計算機の教育利用の分野ではポピュラーなテーマの一つであるが,実用的なシステムの開発に成功した例は少ない[1,2].本報告では比較的新しい計算機による初等幾何学定理証明法である面積法[6]のJani?icらによる証明支援系言語であるCoqによる実装[7]を紹介している.特に,Jani?icらの面積法の実装により自動証明できていない命題を考察している.本研究は,より多くの命題を自動証明可能にすること,そして,そのための面積法による初等幾何証明の基本命題を整理することを目標としている.ここでは自動証明できない具体的な命題を考察し,対策のために必要な基本的な補題を構築したので紹介する.