Démonstration automatique de théorèmes

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.

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.

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

• 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

• Des assistants de preuve comme le logiciel Coq