2023年度情報科学発展演習テーマ

担当：木下佳樹 yoshiki@kanagawa-u.ac.jp

概要

離散数学IIで扱った自然演繹の証明を，Agdaという言語によって書き表す演習を行います．

Agda処理系はAgdaで記された証明が間違っていないことを検証してくれます．

それだけでなく，Agda処理系が，使うべき証明規則を教えてくれます．

例 ((P ∧ Q) ⇒ R) ⇒ (P ⇒ (Q ⇒ R)) の証明

自然演繹による証明木：