>>> on cherche ici à prouver des petits bouts de code, de théorème afin de faciliter la preuve d'ensemble.
Ce travail de fourmi, utilisant le logiciel français COQ
A noter un numéro extrêmement intéressant des Notices de l'American Mathematical Society consacré en décembre dernier aux preuves par ordinateur :
Les articles sont tous bien foutus mais j'ai particulièrement apprécié celui intitulé "Formal Proof—Getting Started" qui évoque les divers logiciels de preuve.
"HOL Light" contre "Mizar" contre "ProofPower" contre "Isabelle" contre "Coq".
# Notices of the AMS
Posté par patrick_g (site web personnel) . En réponse au journal Le labo commun Inria-Microsoft. Évalué à 3.
Ce travail de fourmi, utilisant le logiciel français COQ
A noter un numéro extrêmement intéressant des Notices de l'American Mathematical Society consacré en décembre dernier aux preuves par ordinateur :
http://www.ams.org/notices/200811/index.html
Les articles sont tous bien foutus mais j'ai particulièrement apprécié celui intitulé "Formal Proof—Getting Started" qui évoque les divers logiciels de preuve.
"HOL Light" contre "Mizar" contre "ProofPower" contre "Isabelle" contre "Coq".
Et que le meilleur gagne !