自動定理証明におけるインターフェースの研究

本研究の目的は、計算機に人間の行なう数学的思考の一部を補佐・代行させた場合における人間と計算機との間のインターフェースを工夫し、その対話の円滑化をはかることである。そのために一般的な考察を行い、さらに具体的な数学理論について実験的に感触を得るために、圏論のための証明検証系と図式によるインターフェースを試作した。まず数学の証明における図や式の役割について考察した。その結果、式の長所として、論理的厳密性が挙げられ、一方短所として、直観性に乏しいことが挙げられる。逆に図は、直観性にまさるが、しばしば意味が曖昧になるという問題が指摘される。また、使用法にもよるが、厳密に書くと冗長になりがちな式に比較して、極めて簡潔な表現が図によって可能になることがある。このような観点から、証明の方針や概略を考える際には図などによる直観を利用し、最終的に厳密な証明を書き下すには式を用いるのがいいと考えられる。この使い分けに沿って圏論の証明支援システムを試作した。このシステムを用いると、点・線・矢印などの描画により圏論の定理や証明方針を記述できるので、ユーザは自己の直観に基づいて証明の基本方針を立てることが可能である。システムは、描画内容や手順から定理の内容を推測し、厳密な式に置き換えて証明を検証する。簡単な実験を行った結果、この図によるインターフェースは圏論の証明支援をおこなう上で大変有望と思われる。一方、このようなインターフェースがあっても、システムの検証能力が弱いと証明作業は煩わしいものとなり、インターフェースの効率が著しく減ずるので、自動証明能力の強化が重要な課題として浮かび上がって来た。

本研究の目的は、計算機に人間の行なう数学的思考の一部を補佐・代行させた場合における人間と計算機との間のインターフェースを工夫し、その対話の円滑化をはかることである。そのために一般的な考察を行い、さらに具体的な数学理論について実験的に感触を得るために、圏論のための証明検証系と図式によるインターフェースを試作した。まず数学の証明における図や式の役割について考察した。その結果、式の長所として、論理的厳密性が挙げられ、一方短所として、直観性に乏しいことが挙げられる。逆に図は、直観性にまさるが、しばしば意味が曖昧になるという問題が指摘される。また、使用法にもよるが、厳密に書くと冗長になりがちな式に比較して、極めて簡潔な表現が図によって可能になることがある。このような観点から、証明の方針や概略を考える際には図などによる直観を利用し、最終的に厳密な証明を書き下すには式を用いるのがいいと考えられる。この使い分けに沿って圏論の証明支援システムを試作した。このシステムを用いると、点・線・矢印などの描画により圏論の定理や証明方針を記述できるので、ユーザは自己の直観に基づいて証明の基本方針を立てることが可能である。システムは、描画内容や手順から定理の内容を推測し、厳密な式に置き換えて証明を検証する。簡単な実験を行った結果、この図によるインターフェースは圏論の証明支援をおこなう上で大変有望と思われる。一方、このようなインターフェースがあっても、システムの検証能力が弱いと証明作業は煩わしいものとなり、インターフェースの効率が著しく減ずるので、自動証明能力の強化が重要な課題として浮かび上がって来た。