La demostración automática de teoremas (de siglas ATP, por el término en inglés: ) que también puede ser denominada Deducción automatizada, es actualmente el subcampo más desarrollado del razonamiento automático, y se encarga de la demostración de teoremas matemáticos mediante programas de ordenador.