Démonstration automatique de théorèmes
![](http://upload.wikimedia.org/wikipedia/commons/thumb/1/1f/Racine_carr%C3%A9e_bleue.svg/35px-Racine_carr%C3%A9e_bleue.svg.png)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/3/33/Consistency.png/45px-Consistency.png)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/0/02/Circle-icons-computer.svg/35px-Circle-icons-computer.svg.png)
Cet article est une ébauche concernant les mathématiques, la logique et l’informatique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
![Page d’aide sur l’homonymie](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a9/Logo_disambig.svg/20px-Logo_disambig.svg.png)
Pour les articles homonymes, voir DAT.
La démonstration automatique de théorèmes (DAT) 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
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 ; c'est le cas, par exemple, de la conjecture de Robbins (en), démontrée en 1996 par le logiciel EQP. Cependant, ces succès sont sporadiques et supposent une forme très particulière des théorèmes à démontrer ; par exemple dans le cas de la conjecture de Robbins, il s'agit d'un théorème équationnel, c'est-à-dire d'un théorème dont l'énoncé comporte essentiellement, des identités à démontrer.
Problèmes liés
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é.
Le problème qui consiste à évaluer la longueur minimum d'une preuve pour un certain énoncé dans un certain système de preuve, est étudié en complexité des preuves.
Usage industriel
Les démonstrateurs automatiques de théorèmes 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 [réf. nécessaire], 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
- Règle de résolution avec l'unification
- Lean theorem proving
- Model elimination
- Méthode des tableaux
- Superposition and term rewriting
- Model checking
- Raisonnement par récurrence
- Diagramme de décision binaire
- Algorithme DPLL
- Higher-order unification
Voir aussi
- Des assistants de preuve comme le logiciel Coq
Portail des mathématiques
Portail de la logique
Portail de l’informatique