定理の証明を
コンピュータで
チェックする
2023年度情報科学発展演習テーマ
担当:木下佳樹 yoshiki@kanagawa-u.ac.jp
概要
概要
離散数学IIで扱った自然演繹の証明を,Agdaという言語によって書き表す演習を行います.
Agda処理系はAgdaで記された証明が間違っていないことを検証してくれます.
それだけでなく,Agda処理系が,使うべき証明規則を教えてくれます.
例 ((P ∧ Q) ⇒ R) ⇒ (P ⇒ (Q ⇒ R)) の証明
例 ((P ∧ Q) ⇒ R) ⇒ (P ⇒ (Q ⇒ R)) の証明
自然演繹による証明木:
Agda言語による表現:
curry : ((P ∧ Q) ⇒ R) ⇒ (P ⇒ (Q ⇒ R))
curry = ⇒導入 (λ p∧q⇒r →
⇒導入 (λ p →
⇒導入 (λ q →
⇒除去 p∧q⇒r
(∧導入 p q))))