コ‐キュー【CoQ】
読み方：こきゅー
Coq
名前 コック
COQ
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/30 05:21 UTC 版)
COQ, 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が事実上の開発代表者である。
[続きの解説]
「Coq」の続きの解説一覧
- 1 Coqとは
- 2 Coqの概要
Coq
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/13 06:25 UTC 版)
フランスで開発された証明支援システムで、仕様記述から実行可能なプログラムを自動生成できる（生成するソースコードはOCamlまたはHaskell）。仕様記述や証明の記述に使われる言語は Calculus of Inductive Constructions (CIC) と呼ばれている。
※この「Coq」の解説は、「自動推論」の解説の一部です。
「Coq」を含む「自動推論」の記事については、「自動推論」の概要を参照ください。
ウィキペディア小見出し辞書の「CoQ」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。
- CoQのページへのリンク
