Bibliothèque Tangente. N° 52. Démonstration : l’ordinateur à la rescousse. p. 76-79.
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 : Informatique pour les mathématiques de l’ouvrage Bibliothèque Tangente n° 52 – Mathématiques et informatique.
Il est également paru dans Tangente Hors-série n° 52 – L’informatique riche des maths.
Données de publication
Éditeur Editions POLE Paris , 2014 Collection Bibliothèque Tangente Num. 52 Format 17 cm x 24 cm, p. 76-79
ISBN 2-84884-151-6 EAN 9782848841519 ISSN 2263-4908
Public visé élève ou étudiant, enseignant, tout public Niveau 1re, 2de, licence, lycée, terminale Âge 15, 16, 17, 18, 19
Type chapitre d’un ouvrage, vulgarisation, popularisation Langue français Support papier
Classification