Assistant De Preuve

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.

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


Voir aussi

Informatique théorique
Théorie du calcul
Calculabilité Décidabilité et indécidabilité • Ensemble récursif • Problème de l'arrêt • Récursivement énumérable
Modèle de calcul Automate fini • Automate cellulaire • Machine de Turing • Thèse de Church
Modes de calcul Concurrence • Parallèlisme • Théorie de l'ordonnancement
Mesure et échelle de complexité Réduction polynomiale • Problème NP-complet
Logique, syntaxe et sémantique
Logique mathématique Assistant de preuve • Calcul des prédicats • Correspondance de Curry-Howard • Fonction récursive • Lambda-calcul • Théorème d'incomplétude de Gödel • Théorie des types
Grammaire formelle et systèmes de réécriture Compilation • Expression rationnelle • Grammaire formelle • Langage rationnel • Théorie des langages
Sémantique Sémantique des langages de programmation • Sémantique dénotationnelle • Sémantique axiomatique • Sémantique opérationnelle
Spécifier, vérifier et concevoir des programmes Interprétation abstraite • Méthodes formelles • Model checking
Algorithmique, complexité et mathématiques discrètes
Algorithmique Algorithme génétique • Algorithme glouton • Algorithme probabiliste • Complexité algorithmique • Diviser pour régner • Heuristique • Programmation dynamique
Problèmes et algorithmes numériques Algorithme du simplexe • Géométrie algorithmique • Algorithme d'Euclide • Test de primalité
Problèmes et algorithmes non-numériques Algorithmes de la théorie des graphes • Arbre (informatique) • Liste (informatique) • Table de hachage • Tas (informatique)
Théorie des graphes Coloration de graphe • Problèmes de cheminement
Recherche opérationnelle Optimisation • Optimisation combinatoire • Théorie de l'ordonnancement
Données et codage Codage • Codage de l'information • Compression de données • Cryptage • Cryptanalyse • Cryptographie • Théorie de l'information
  • Portail des mathématiques Portail des mathématiques
  • Portail de l’informatique Portail de l’informatique
  • Portail de la logique Portail de la logique
Ce document provient de « Assistant de preuve ».

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”