Démonstration automatique de théorèmes

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