Coq (assistant de preuve)

Coq (assistant de preuve)

Coq (logiciel)

Coq est un assistant de preuve développé à l'INRIA, à l'École polytechnique et à l'Université de Paris XI (et antérieurement à l'École normale supérieure de Lyon) dans le cadre du projet TypiCal.

Caractéristiques du logiciel

Coq est fondé sur le calcul des constructions (introduit par Thierry Coquand, CoC abrégé en anglais, d'où un jeu de mots justifiant le nom du système), une théorie des types d'ordre supérieur, et son langage de spécification est donc une forme de lambda-calcul typé. Le calcul des constructions utilisé dans Coq comprend directement les constructions inductives, d'où son nom de calcul des constructions inductives (CIC).

Coq a été récemment doté de fonctionnalités d'automatisation croissantes. Citons notamment la tactique Omega qui décide l'arithmétique de Presburger.

Plus particulièrement, Coq permet :

  • de manipuler des assertions du calcul ;
  • de vérifier mécaniquement des preuves de ces assertions ;
  • d'aider à la recherche de preuves formelles ;
  • de synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications.

C'est un logiciel libre distribué selon les termes de la licence GNU LGPL.

Parmi les grands succès de Coq, on peut citer la démonstration complètement mécanisée du théorème des quatre couleurs par Georges Gonthier et Benjamin Werner.

On peut le comparer aux autres assistants de preuves tel que : Isabelle, HOL, Mizar, PVS.

Voir aussi

Liens externes


  • Portail des logiciels libres Portail des logiciels libres
  • Portail des mathématiques Portail des mathématiques
  • Portail de la logique Portail de la logique
Ce document provient de « Coq (logiciel) ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Coq (assistant de preuve) de Wikipédia en français (auteurs)

Игры ⚽ Нужно решить контрольную?

Regardez d'autres dictionnaires:

  • Assistant De Preuve — En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des… …   Wikipédia en Français

  • Assistant de preuve — En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des… …   Wikipédia en Français

  • Coq (Logiciel) — Coq est un assistant de preuve développé à l INRIA, à l École polytechnique et à l Université de Paris XI (et antérieurement à l École normale supérieure de Lyon) dans le cadre du projet TypiCal. Caractéristiques du logiciel Coq est fondé sur le… …   Wikipédia en Français

  • Coq (Homonymie) — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom.  Pour les articles homophones, voir Cock et Coque …   Wikipédia en Français

  • Coq (logiciel) — Pour les articles homonymes, voir Coq (homonymie). Coq (logiciel) …   Wikipédia en Français

  • Coq (homonymie) — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom.  Pour les articles homophones, voir Cock et Coque. Sur les autres projets Wikimedia  …   Wikipédia en Français

  • Démonstrateur interactif de théorèmes — Assistant de preuve En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques …   Wikipédia en Français

  • Methode formelle (informatique) — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… …   Wikipédia en Français

  • Méthode formelle — (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels… …   Wikipédia en Français

  • Méthode formelle (informatique) — Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”