(19) 図式を用いたユーザインタフェイスを持つ 圏論証明支援システム

平成８年度委託研究中間報告

１　研究テーマ、研究代表者：
　（１）研究テーマ
        図式を用いたユーザインタフェイスを持つ、圏論証明支援システムに
        関する研究
　（２）研究代表者（氏名、所属、役職）
        坂井公　筑波大学数学系  助教授　

２　記述項目：

　（１）研究進捗状況

ユーザインタフェイスに図式(可換図式)を用いた圏論の命題の証明支援システ
ムを作成する。図式は圏論においてよく使われているが、その役割は補助的な
ので、証明支援システムに使うためには形式化する必要がある。そこで、一般
に、圏論においてどのように図式が利用されているか調査し、図式の仕様を決
定した。そして、図式を用いた証明手段として「貼り付け」という手法を確立
し、試作システムを作成した。「貼り付け」によって、等式の証明を目で見て
わかりやすい形で行う事ができるようになった。しかし、一般の命題は論理記
号を含んでいるため、圏論の命題の証明支援システムにするためには、それら
を扱う必要がある。現在論理記号を含んだ図式、及び証明支援システムの仕様
を検討している。また、試作システムによって明らかになった問題点の修正を
行っている。

　（２）現在までの主な成果

仮定となる図式を、証明したい図式に「貼り付け」る事によって、証明を行う
システムを java で書いたものを作成した。「貼り付け」る場所が一意に定ま
る場合は、自動的に「貼り付け」が行われる。図式の変形が可能なので、複雑
になった図式をユーザが自由に変形し、見やすい形にする事ができる。

　（３）今後の研究概要

図式を用いた証明支援の核は、「貼り付け」であるが、これだけでは等式の証
明しかできないため、初等的な命題でさえ証明できない。そこで、簡単な論理
記号を扱えるようにシステムの拡張をする。

　（４）今年度目標成果ソフトウェアイメージ

圏論の教科書の最初の方に出て来るような例は、図式の描画、図式上でのボタ
ンのクリック、図式のドラッグによる「貼り付け」等によって、証明すること
のできるシステムを作成する。論理式を直接書いたり、見たりすることなく証
明を行う。