特別専攻セミナーの様子

本研究室の特別専攻セミナーでは、命題論理学を学んでいます。面白そうだということで、私の担当ではない学生も来て、学んでいます。そのため、特別専攻の学生が4人もいます (@_@)。

特別専攻セミナーの様子

特別専攻の学生さんは、勉強が得意な学生さんたちなので、紙と鉛筆を使って熱心に勉強しています。行っているテーマは、論理学の中の証明木を使った証明です。

発端は関数型言語に興味のあるという大学院生です。関数型言語に興味があるのならば、ということで、カリー・ハワードの同型対応を説明し、coqなどについて学んでいます。その学びの一部を、特別専攻のセミナー生に伝授しています。

カリー・ハワードの同型対応は、一言で言ってしまえば「型＝命題，プログラム＝証明」を提唱したもので、「型付けできたということは、証明できた」ということになります。その原理を用いているのが対話型の定理証明支援システムcoqです。これらの中で、論理学の自然演繹は基本になりますので、この部分も学びました。そして、その学びを特別専攻のセミナー生に伝授しています。