研究の背景と目的

Next: 研究の内容 Up: 「図式を用いたユーザインタフェースを持つ圏論証明支援システム」に関する成果概要 Previous: 「図式を用いたユーザインタフェースを持つ圏論証明支援システム」に関する成果概要

研究の背景と目的

我々は図式による証明支援系のインターフェイスを設計している。圏論等の代数では証明をわかりやすくするため可換図がよく用いられる。この仕組みを形式的証明にも用いようと我々は考えた。

例えば、

という論理式は図 --1 のように表示したほうが人間にとってわかりやすい。

図 --1: 図式の例

また、

の証明を図 --2 のように、可換図を用いて表す事もある。

図 --2: 図式による証明の例

このように、圏論において図式はよく利用されるので、形式的な証明支援システムにも、採り入れる事は自然だと考えた。また、形式的な証明では、冗長な長い式の出現によって、証明の見通しが悪くなったりするので、それをユーザにとってわかりやすく表示する事は重要である。図式の利用はこの問題点にもある解を与えるのではないかと考えた。

そこで、本研究では図式をユーザインタフェイスとした圏論のための証明支援システムを作成する事を目的とした。

www-admin@icot.or.jp