Assistant de preuve

Assistant de preuve

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.

Sommaire

Conception

Beaucoup de projet ont été lancé pour formaliser les mathématiques. En 1966, Nicolaas de Bruijn lance le projet Automath, et d’autres projets ont été lancés après celui-ci. Les projets les plus avancé sont : le projet Mizar en Pologne, en Grande-Bretagne et aux États-Unis le projet HOL-Isabelle et, en France, le projet Coq[1].

Le but de ces projets est mettre à la disposition du mathématicien des outils informatiques pour l’aider à élaborer une version formelle du résultat auquel il s’intéresse. Le logiciel stocke aussi les résultats démontrés auparavant.

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).

Succès

Selon une étude publiée dans le magazine Pour la science[1], sur la liste des «100 théorèmes mathématiques les plus importants[2]», une liste composée par Nathan Kahn, mathématicien du Steven Institute of Technology, dans le New Jersey, 85 des 100 théorèmes ont été formalisés.

Avec les assistants de preuve actuels, le travail de formalisation est rendu fastidieux par un langage complexe[1].

Utilisation

Les assistants de preuve sont utiles pour la démonstration des problèmes très complexes, et aident à produire une démonstration formelle. Le célèbre problème des quatre couleurs a été résolu en utilisant un assistant de preuve. Avec l’utilisation de cet outil, des erreurs aurait été évitées, comme l’explosion de la fusée Ariane[1].

Les assistants de preuve sont utilisés pour démontrer le bon fonctionnement des circuits des microprocesseurs. En effet, Intel les a utilisés pour s’assurer du bon fonctionnement de son Pentium 4, cependant en 1994, Thomas Nicely, de l’Universitéde Lynchburg (États-Unis), a pu trouver un dysfonctionnement dans l’unité de calcul en virgule flottante du Pentium: il s’est rendu compte que certaines opérations du processeur renvoyaient une valeur erronée par excè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 bugués. Un assistant de preuve bugué 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.

Théorème à vendre

En 2010, des universitaires à l'University of Edinburgh offrent aux gens la possibilité d’acheter des théorèmes trouvés par des assistants de preuve. Le nouveau théorème sera appelé au nom de l’acheteur[3].

Théorèmes prouvés avec des assistants de preuve

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

Voir aussi

Références

  1. ↑ a, b, c et d Jean-Paul Delahaye, « Du rêve à la réalité des preuves », dans Pour la Science, avril 2011, p. 90-95 
  2. ↑ (en) the «top 100» of mathematical theorems, 2011
  3. ↑ (en) Herald Gazette article on buying your own theorem, Herald Gazette Scotland, Novembre 2010

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Assistant de preuve de Wikipédia en français (auteurs)

Игры ⚽ Поможем решить контрольную работу

Regardez d'autres dictionnaires:

  • Assistant De Preuve — 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… …   Wikipédia en Français

  • Coq (assistant de preuve) — Coq (logiciel) Coq est un assistant de preuve développé à l INRIA, à l École polytechnique et à l Université de Paris XI (et antérieurement à l École normale supérieure de Lyon) dans le cadre du projet TypiCal. Caractéristiques du logiciel Coq… …   Wikipédia en Français

  • Preuve — Une preuve est un fait ou un raisonnement propre à établir solidement la vérité. Il existe deux types de preuves épistémologiquement considérées comme valides : Les preuves basées sur la déduction qui ont un caractère absolu ou certain pour… …   Wikipédia en Français

  • Assistant — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Le mot assistant peut désigner: Un ecclésiastiques qui, dans les messes solennelles, assiste le célébrant à l autel. Les personnes présentes en un lieu.… …   Wikipédia en Français

  • Preuve (mathématiques) — Démonstration En mathématiques, une démonstration permet d établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de propositions initiales, en s appuyant sur un ensemble de règles de déduction. La… …   Wikipédia en Français

  • Démonstrateur interactif de théorèmes — Assistant de preuve 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 …   Wikipédia en Français

  • Methode formelle (informatique) — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… …   Wikipédia en Français

  • Méthode formelle — (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels… …   Wikipédia en Français

  • Méthode formelle (informatique) — Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin …   Wikipédia en Français

  • Méthodes formelles — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”