Page d'accueil
encyclopedie-enligne.com en page d'accueil| Page d'accueil |
encyclopedie-enligne.com en page d'accueil |
|||||
| Liste Articles: [0-A] [A-C] [C-F] [F-J] [J-M] [M-P] [P-S] [S-Z] | Liste Catégories | Une page au hasard | Pages liées | ||||||
En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l'écriture et la vérification de preuves mathématiques, soit sur des
théorèmes au sens usuel des mathématiques, soit sur des assertions
relatives à l'exécution de programmes
informatiques.
L'écriture de preuves entièrement formelles est une activité extrêmement fastidieuse ; de nombreuses étapes qui seraient sautées, car considérées comme évidentes pour le lecteur familier des mathématiques, doivent être décortiquées dans les plus grands détails. Cependant, l'assistant de preuve peut fournir plus ou moins d'automatisation pour limiter le travail de l'utilisateur humain. Certains assistants de preuve, tels que PVS, possèdent des procédures de décision dans des domaines souvent utilisés et décidables (tels que l'arithmétique de Presburger); souvent, on leur ajoute des procédures de semi-décision (qui ne terminent pas forcément avec succès).
Une objection à l'usage d'assistants de preuve et que, de toute façon, la sécurité des preuves obtenues repose sur le bon fonctionnement de l'assistant. En effet, les assistants de preuves sont de gros logiciels complexes, dont on peut soupçonner qu'ils soient eux-même bogués. Un assistant de preuve bogué peut permettre de démontrer l'absurde. Certains assistants de preuve, comme Coq, produisent un terme de preuve dont la vérification peut être déléguée à une logiciel beaucoup plus simple qu'un assistant complet ; ainsi, Coq produit des termes du Calcul des Constructions ([inductives, à présent), un lambda-calcul typé d'ordre supérieur, dont on peut relativement facilement vérifier s'ils sont correctement typés. Coq, de plus, a lui-même été prouvé dans Coq, ce qui rend la confiance que l'on peut avoir dans ce logiciel un peu plus légitime.
