Démonstrateur interactif de théorèmes

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 se terminent pas forcément avec succès).

Une objection à l'usage d'assistants de preuve est 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êmes 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 à un 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 par son vérificateur de démonstrations, ce qui rend la confiance que l'on peut avoir dans ce logiciel un peu plus légitime.

Note sur la terminologie: L'utilisation de preuve à la place de démonstration est, en toute rigueur, un anglicisme, en tant que traduction directe du mot «proof», mais l'utilisation du mot «preuve» fait maintenant partie du langage des spécialistes et cet article se plie à cet usage. La difficulté est d'autant plus grande que le mot «demonstration» a un usage courant différent en anglais.

Assistants de preuve

• Coq
• Isabelle
• PhoX
• PVS

Voir aussi

• Logique mathématique
• Décidabilité et indécidabilité

• Portail des mathématiques
• Portail de l’informatique
• Portail de la logique