L'oeuf ou la poule | Un assistant de vérification de preuves nommé Coq
858
post-template-default,single,single-post,postid-858,single-format-standard,ajax_fade,page_not_loaded,,qode-title-hidden,qode_grid_1300,footer_responsive_adv,qode-content-sidebar-responsive,qode-theme-ver-10.1.2,wpb-js-composer js-comp-ver-5.1,vc_responsive

Un assistant de vérification de preuves nommé Coq

Depuis longtemps, on utilise les mathématiques pour vérifier les programmes informatiques. Il s’avère que l’informatique peut rendre la pareille aux mathématiques : pour vérifier de manière automatique une preuve mathématique, il existe des logiciels appelés assistant de preuve. La chronique Mathématiques de Nadia Lafrenière, Stéphanie Schanck et Élise Vandomme du 11 décembre 2017 nous en apprend plus sur Coq, un de ces logiciels.

No Comments

Post A Comment