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.

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

Un problème plus simple, mais lié au problème des démonstrateurs automatiques de preuve, est celui de vérificateur de preuve, qui vérifie si la preuve d'un théorème est valide. Pour cela, il est généralement requis que chaque étape puisse être vérifiée par une fonction récursive ou un programme, et ainsi le problème est toujours décidable.

Les assistants de preuve nécessitent un humain pour donner le chemin amenant à la solution au système. En fonction du degré d'automatisation, l'assistant de preuve peut se réduire à un vérificateur de preuve, où l'utilisateur fourni la preuve de manière formelle, ou bien l'assistant de preuve peut réaliser des étapes importantes de manière automatique. Les assistants de preuve sont utilisés pour une variétés de tâches, mais les démonstrateurs automatiques de théorème ont prouvé des théorèmes intéressants difficiles à établir, certains ayant échappé aux mathématiciens pendant longtemps. Cependant ces succès sont sporadiques et le travail sur des problèmes compliqués nécessite un utilisateur compétent.

Il y a des systèmes de preuves de théorème hybrides qui utilisent le model checking pour les règles de déduction. Il y a également des programmes qui sont écrits pour prouver un théorème particulier, avec une preuve (usuellement informelle) qui est que si le programme termine, le théorème est vrai.

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