Isabelle
によるシーケント計算
定理証明支援ツール Isabelle
上でシーケント計算の推論規則を表現し，それを使って証明をします．
自然演繹とはまた違ったパズルを楽しむことができます．
集合の帰納的定義を使って推論規則を表現する典型的な例です．シーケント計算は命題論理の範囲です．
※ カットの話はしません．
プログラム
- シーケント計算
- Isabelle 上での表現
- 証明例
- 演習問題
- チャレンジ問題
セミナー参加の前提条件
前提知識
- Isabelle の文書 tutorial.pdf の part I, II 程度の知識（Isabelle
チュートリアル第1~4回相当）
必要なもの