| 平成８年度 委託研究ソフトウェアの 最終成果報告書 |
形式的な定理証明を行うシステムにとっても、ユーザインターフェースが重要であるとの認識が高まっている。 圏論においては、自然言語や論理式で書いた(非形式的な)証明の理解を容易にするために、可換図というものが広く用いられている。当然、形式的な定理証明においても可換図を用いたいというのは、自然な要求である。実際、数学の機械化を推進する上での主要な障害の一つは、形式的な証明を理解する際の難しさであるから、書いてある内容について直観的な理解を得るための助けが受けられるということの価値は大きい。 我々は、圏論の証明支援システムのために、可換図を中心としたユーザ・インターフェースを開発している。
www-admin@icot.or.jp