Démonstration automatique de théorèmes

L'objectif de la démonstration automatique de théorèmes est de générer automatiquement des preuves dans un langage formel à partir d'une conjecture (théorème cible) et d'une base de connaissances de faits établis. Cette technologie a des applications significatives dans la vérification et la synthèse de systèmes logiciels et matériels, entre autres domaines.