Démonstration automatique de théorèmes

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

La démonstration automatique de théorèmes est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet sans l'aide de l'utilisateur.

Application en mathématiques[modifier | modifier le code]

Les démonstrateurs automatiques de théorème ont résolu des conjectures intéressantes difficiles à établir, certaines ayant échappé aux mathématiciens pendant longtemps. Cependant ces succès sont sporadiques et supposent une forme très particulière des théorèmes à démontrer.

Problèmes liés[modifier | modifier le code]

Un problème plus simple, lié aux démonstrateurs automatiques, est celui des vérificateurs de démonstration, qui s'assurent que les démonstrations qu'on leur soumet sont valides.

Les assistants de démonstration (ou assistants de preuve) nécessitent l'intervention d'un humain pour donner les étapes amenant à la solution. En fonction du degré d'automatisation, l'assistant de preuve peut se réduire à un vérificateur des démonstrations, que l'utilisateur lui fournit en tant qu'objets formels, ou bien à un créateur des étapes importantes de manière automatique.

Il y a aussi des systèmes hybrides de vérification de la véracité d'énoncés qui utilisent la vérification de modèles (en anglais model checking). Il y a également des programmes qui sont écrits spécifiquement pour démontrer un théorème donné.

Usage industriel[modifier | modifier le code]

Les démonstrateurs automatiques de preuve sont utilisés de manière commerciale principalement dans le design et la vérification de circuits intégrés. Depuis le problème du bug FDIV du processeur Pentium, la conception de l'unité de calcul flottante des microprocesseurs fait l'objet de soins accrus. En février 2011, AMD, Intel et d'autres font appel à des démonstrateurs automatiques de théorèmes pour vérifier que la division et d'autres opérations sont correctement implémentées dans leurs processeurs.

Techniques populaires[modifier | modifier le code]


(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Automated theorem proving » (voir la liste des auteurs).