Démonstration automatique de théorèmes

Un article de Wikipédia, l'encyclopédie libre.
Cet article est une ébauche concernant les mathématiques, la logique et l’informatique.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).

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.