Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.
influenced
Wikipage redirect
primaryTopic
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.
has abstract
Coq (gallo en francés) es un s ...... escrito en el lenguaje Ocaml.
@es
Coq (фр. coq — петух) — интера ...... ля исчисления — Тьерри Кокана.
@ru
Coq est un assistant de preuve ...... Languages Software 2013 Award.
@fr
Coq ist ein Programm zum maschinengestützten Beweisen mathematischer Aussagen.
@de
Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数 ...... 开了停机问题。同时，这也使得 Coq 语言本身并非图灵完全。
@zh
Coqは証明支援システムの一つ。Coqの核はプログラミング言 ...... いる。Hugo Herbelinが事実上の開発代表者である。
@ja
In computer science, Coq is an ...... Software System Award for Coq.
@en
genre
latest release date
2016-07-11
latest release version
license
operating system
programming language
status
thumbnail
Link from a Wikipage to an external page
Wikipage page ID
Wikipage revision ID
741,581,345
developer
The Coq development team
dialects
language
paradigm
turing-complete
subject
hypernym
comment
Coq (gallo en francés) es un s ...... del Cálculo de Construcciones.
@es
Coq (фр. coq — петух) — интера ...... ется для верификации программ.
@ru
Coq est un assistant de preuve ...... wiki dédié, baptisé Cocorico!.
@fr
Coq ist ein Programm zum maschinengestützten Beweisen mathematischer Aussagen.
@de
Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数 ...... Gérard Huet 共同提出了前述的构造演算）的姓氏。
@zh
Coqは証明支援システムの一つ。Coqの核はプログラミング言 ...... いる。Hugo Herbelinが事実上の開発代表者である。
@ja
In computer science, Coq is an ...... d various decision procedures.
@en
label
Coq (Software)
@de
Coq (logiciel)
@fr
Coq
@en
Coq
@es
Coq
@ja
Coq
@ru
Coq
@zh
wasDerivedFrom
depiction
isPrimaryTopicOf
name
Coq (software)
@en