Démonstration Automatique de Théorèmes (ATP)
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.