Coq庵 - rfなブログ8/29 に、Coq庵 に行ってきました。 資料等はこちら。 行き道で祭りやってた。 一部道が通れなかったりして、少し迷うなど。 初めてのCoq 仕様記述言語 Prolog ACL2, HOL/Light 完全自動証明 自動で証明してくれるが、表現力がやや低い Isabelle/HOL, Coq, Agda 手動証明 表現力が非常に高い Coq の特徴 高階論理 表現力最強 自動証明機能 (tactic) 対話的に人間が証明を与えるが、部分的に自動証明を使うこともできる プログラムと連携 証明したものをそのまま実行できる OCaml, Haskell, Sheme に出力できる Coq の中身 関数型プログラム的 Vernacularコマンド (プログラムの文) Gallina式 (プログラムの式) 内部はラムダ式 論理学的 tactic 証明、証明を含む式 小文字で始まって . で終わる
