Démonstration Automatique de Théorèmes (ATP)

- Natural & Formal Sciences -
Mathematics & Logic Dictionary
Définition
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.