なぜ、開発は人間によって担われているのか？ （pdf）
参考資料
MaruLabo Hands on はじめてのCoq
Coqのインストール
平原ゼミ Coq スタートアップセミナー を利用ください
Hands on のソース
Github https://github.com/maruyama097/coq-tutorial
Hello Coq!
Hello Coq! (1) -- Coqとのはじめての対話 (pdf)
Hello Coq! (2) -- 人間はCoqに何を伝えたか？ (pdf)
Hello Coq! (3) -- Coqは人間に何を伝えたか？ (pdf)
論理式の証明
論理式はどのような形をしているか？( pdf )
論理式の部分式への分解とサブゴール ( pdf )
構成のルールと演繹のルール ( ムービー pdf )
「正しい」ことと「証明を持つ」こと ( pdf )
命題論理の演繹ルール ( pdf )
Coqの返す「証明の状態」と演繹ルール ( pdf )
tactic (1) サブゴールの形と演繹ルールの選択 ( pdf )
tactic (2) 仮説部の形と演繹ルールの選択 ( pdf )
「否定」について ( pdf )
