Tangente Hors-série. N° 52. p. 34-36. Démonstration : l’ordinateur à la rescousse.
Auteur : Filliâtre Jean-Christophe
Résumé
Cet article présente le logiciel Coq développé par des chercheurs de l’Inria qui est un assistant de preuve, c’est-à-dire un logiciel permettant l’écriture et la vérification de preuves mathématiques.
Notes
Cet article est publié sous la rubrique « Actions ».
Il fait partie du dossier : Maths et informatique : regards croisés dans Tangente Hors-série n° 52 – L’informatique riche des maths.
Il est également paru dans Bibliothèque Tangente n° 52 – Mathématiques et informatique.
Données de publication
Éditeur Editions POLE Paris , 2014 Format A4, p. 34-36
ISSN 1294-9949
Public visé élève ou étudiant, enseignant, tout public Niveau 1re, 2de, licence, lycée, terminale Âge 15, 16, 17, 18, 19
Type article de périodique ou revue, vulgarisation, popularisation Langue français Support papier
Classification