La démonstration automatique de théorèmes (ATP) est l'utilisation d'algorithmes et d'heuristiques par des logiciels pour effectuer la recherche de preuves et établir des théorèmes sans intervention humaine, en produisant des preuves ou des réfutations dans des logiques formelles.

Principe

Combiner des règles d'inférence correctes, le contrôle de recherche, des heuristiques et des optimisations (indexation de termes, unification, sélection de clauses, apprentissage) afin d'explorer efficacement l'espace des dérivations tout en conservant, autant que possible, des garanties de correction.

Démonstration

Un système ATP basé sur la résolution en logique du premier ordre réfute la négation d'une conjecture en saturant les clauses par résolution et unification et renvoie une dérivation de contradiction ; les solveurs SAT et SMT décident automatiquement des formules propositionnelles et des formules contraintes par des théories.

Mauvaise application

Se fier sans contrôle aux sorties d'un ATP sans objets de preuve, supposer la complétude dans des logiques indécidables ou déployer des solveurs sans tenir compte d'erreurs de modélisation peut conduire à une confiance injustifiée en l'exactitude.

Conséquence

L'ATP automatise le raisonnement routinier, met à l'échelle les tâches de vérification, fournit des preuves ou contre-modèles vérifiables par machine et complète les mathématiciens et ingénieurs en vérification par la découverte et la vérification automatiques.

Inversion

L'inversion est le développement de preuves manuelles ou la démonstration interactive où la guidance humaine, les tactiques et l'intuition sont centrales ; l'ATP contraste avec les preuves constructives purement humaines.

Limite

L'ATP s'applique lorsque la logique et l'encodage se prêtent à une recherche algorithmique (logique propositionnelle, fragments décidables, problèmes du premier ordre énumérables de manière effective) ; elle exclut la créativité mathématique informelle et la formation de conjectures non formalisées.

Tension sémantique

La tension apparaît entre l'ATP pleinement automatisé (qui vise autonomie et montée en charge) et les assistants de preuve interactifs/vérifiés (qui privilégient la guidance humaine et les objets de preuve formels).

Synthèse

L'ATP intègre moteurs d'inférence, procédures de recherche et heuristiques d'ingénierie pour établir ou réfuter mécaniquement des assertions formelles dans les limites algorithmiques et de modélisation, produisant des artefacts utilisables pour la vérification et le raisonnement.