Les révisions vous permettent de faire le suivi des différences entre les différentes versions de votre contenu, et de rétablir les versions plus anciennes.

Le logiciel Coq est un assistant à la preuve formelle développé à l'Inria. Il est fondé sur le Calcul des Constructions de Thierry Coquand, une théorie des types d'ordre supérieur, et exploite largement la correspondance de Curry-Howard.

Coq peut manipuler des énoncés du calcul et permet de faire une vérification mécaniques de ces énoncés. Il peut aussi aider à la recherche de preuves formelles d'énoncés mathématiques (par exemple, le théorème des quatre couleurs) ainsi que à la vérification formelle de programmes informatiques (par exemple, le compilateur CompCert C).

Tags: 
Disponible sur: 
Version: 
Logiciel en version stable (publié)
Langue: 
Créateur(s): 
Thierry Coquand
Société ou organisation: 
Inria

Autres suggestions...

Fracatux est un logiciel libre permettant de représenter des fractions sous forme de barres.

Le Frido contient des mathématiques du niveau de l’agrégation.

Pour s'entraîner aux additions, soustractions, multiplications et divisions en jouant.