応用情報数理学特論

注意:
2020年度の第1ターム終了日は6月17日です。
Moodle上の理由で、6月3日以降
第1タームで終了する全ての講義が
 「過去の講義」
として扱われます。

小テストを受ける際、課題を提出する際など、気を付けて下さい。

この講義では定理証明支援系 LEAN の使い方を学びます。

下のURIから、ブラウザ上で動作する
 LEAN Web Editor
を利用できます。
https://leanprover.github.io/live/latest/

LEAN Web Editor を使いながら
講義資料をみると
理解しやすくなると思います。

文献
 Logic and Proof Release 0.1
 J. Avigad, R.Y. Lewis, F.v. Doorn
を参考にします。下のURIからダウンロードできます。
https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf

第1回  講義資料 (5月11日 3限)

第2回  講義資料 (5月11日 4限)

第3回  講義資料 (5月18日 3限)

第4回  講義資料 (5月18日 4限)

第5回  講義資料 (5月25日 3限)

第6回  講義資料 (5月25日 4限)

第7回  講義資料 (6月 1日 3限)

第8回  講義資料 (6月 1日 4限)

第9回  講義資料 (6月 8日 3限)

第10回 講義資料 (6月 8日 4限)

第11回 講義資料 (6月15日 3限)

第12回 講義資料 (6月15日 4限)