目次
I. Hello Coq!
- Coqとのはじめての対話 ( ムービー pdf )
- 人間はCoqに何を伝えたか？ ( ムービー pdf )
- Coqは人間に何を伝えたか？ ( ムービー pdf )
II. 論理式の証明
- 論理式はどのような形をしているか？( ムービー pdf )
- 論理式の部分式への分解とサブゴール( ムービー pdf )
- 構成のルールと演繹のルール ( ムービー pdf )
- 「正しい」ことと「証明を持つ」こと ( ムービー pdf )
- 命題論理の演繹ルール ( ムービー pdf )
- Coqの返す「証明の状態」と演繹ルール ( ムービー pdf )
- tactic (1) サブゴールの形と演繹ルールの選択 ( ムービー pdf )
- tactic (2) 仮説部の形と演繹ルールの選択 ( ムービー pdf )
- 「否定」について ( ムービー pdf )
Appendix 11/28マルレク紹介
- なぜ、開発は人間によって担われているのか？ ( ムービー pdf )
なぜ、開発は人間によって担われているのか？
論理式の証明 (6) — Coqの返す「証明の状態」と演繹ルール
論理式の証明 (5) — 命題論理の演繹ルール
論理式の証明 (4) — 「正しい」ことと「証明を持つ」こと
論理式の証明 (3) — 構成のルールと演繹のルール
論理式の証明 (2) — 論理式の部分式への分解とサブゴール
論理式の証明 (1) — 論理式はどのような形をしているか？
Hello Coq! (3) — Coqは人間に何を伝えたか？
Hello Coq! (2) — 人間はCoqに何を伝えたか？
Hello Coq! (1) — Coqとのはじめての対話