Coq
WIP
概要
関数型言語Gallinaで証明項を書く
CoqのプログラムはOCaml, Haskel, Schemeでextract可能
対話的に証明する
Coqにおける論理
デフォルトは直観主義論理(直観論理の完全な体系であるシークエント計算LJベース)
直観主義論理: 古典論理の制限(排中律や二重否定除去が公理として許容されない)
Coqの組み込み論理は非常に小さく、帰納的定義(Inductive)、全称記号(forall)、ならば(->)だけ
それ以外の論理演算子（かつ、または、否定、存在量化子、等号など）はこれら組み込みのものから定義できる
例: 存在量化子
code: existence(Ocaml)
Inductive ex (X:Type) (P : X->Prop) : Prop :=
ex_intro : forall (witness:X), P witness -> ex X P.
古典論理を使う場合は Require Import Classical.
タクティックと論理
自然演繹体系の論理規則との対応
https://gyazo.com/76f455c92e1add120e082bcaca090e88
参考
CoqはCoqとしての論理計算／証明のシステムを持っていて、それは（典型的な）自然演繹に近いところもあれば、（典型的な）シーケント計算に似てるところもあるけれど、どちらかに一致しているわけではありません
公理のライブラリまとめ
Coqで使われる言語
Gallina（ガリーナ）: 仕様記述言語
OCamlライクな関数型言語
式（項、term）の構文: pCic（ピーシック？ predicative Calculus of Inductive Constructions）
Vernacular（バーナキュラー）: 処理系に命令を与えるコマンド言語
タクティックを定義するLtacコマンドも専用の記法がある
証明方法
対話的証明
手順
証明する論理式(ゴール)を入力
ユーザーが証明のスクリプトを記述、サブゴールが返される
サブゴールがなくなれば証明完成
tactics
公式ドキュメントよりも分かりやすい
自動定理証明
auto、eauto、iauto、jautoタクティックなど
入門資料