Rosetta Code

Category:Coq: Difference between revisions

Category Discussion

Category:Coq (view source)

Revision as of 18:52, 15 March 2014

28 bytes added ,  10 years ago
m
Added link to official site
m (narrow cat)
m (Added link to official site)
 
Line 1:
{{language|Coq
{{language|Coq}}In computer science, Coq is a proof assistant application. 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 [[wp:Theorem_prover|theorem prover]] but includes automatic theorem proving tactics and various decision procedures.▼
|site=http://coq.inria.fr
}}
▲{{language|Coq}}In computer science, Coq is a proof assistant application. 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 [[wp:Theorem_prover|theorem prover]] but includes automatic theorem proving tactics and various decision procedures.
 
==Citations==
Retrieved from "https://rosettacode.org/wiki/Special:MobileDiff/59961"