 |
||||||||||
 |
 |
 |
||||||||
 |
 |
 |
 |
 |
 |
 |
 |
 |
||
Preuves formelles, preuves calculatoires19/03/07 Si elle est complètement détaillée, une preuve se ramène à l'utilisation de règles logiques, dont la correction est précisément définie de manière syntaxique : c'est là une des caractéristiques du raisonnement mathématique. Réussir cette opération en pratique demande de faire appel à l'informatique, et plus précisément à sa branche dite des méthodes formelles.
Dans cet exposé, structuré en quatre chapitres, Benjamin Werner distingue tout d'abord les deux rôles de l'ordinateur, son rôle de vérificateur formel étant bien distinct de son rôle de calculateur.
À travers plusieurs exemples, il s'attache ensuite à montrer comment les systèmes de preuves modernes, comme Coq, permettent de s'attaquer à des preuves nécessitant des calculs importants, et de répondre à des interrogations quant à la validité de certains résultats spectaculaires. Il montre ainsi comment Coq sert à prouver qu'un grand nombre est premier, puis comment ce système a permis de valider la démonstration du théorème des quatre couleurs
Cet exposé de Benjamin Werner a été enregistré le 11 décembre 2006, à l'INRIA Rocquencourt.
La mise en forme en XML/SMIL a été réalisée par Pierre Jancène. Pour visionner ces documents, utiliser RealPlayer.
|
