コ‐キュー【CoQ】
読み方:こきゅー
Coq
COQ
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/08/30 05:21 UTC 版)
COQ, Coq, coq
- 1 COQとは
- 2 COQの概要
Coq
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2024/09/19 23:42 UTC 版)
Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。
- 1 Coqとは
- 2 Coqの概要
Coq
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2019/11/13 06:25 UTC 版)
フランスで開発された証明支援システムで、仕様記述から実行可能なプログラムを自動生成できる(生成するソースコードはOCamlまたはHaskell)。仕様記述や証明の記述に使われる言語は Calculus of Inductive Constructions (CIC) と呼ばれている。
※この「Coq」の解説は、「自動推論」の解説の一部です。
「Coq」を含む「自動推論」の記事については、「自動推論」の概要を参照ください。
- coqのページへのリンク