Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) – proces zdefiniowany w ramach automatycznego rozumowania, w którym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiejś teorii, często przy okazji generując jego dowód. Twierdzenia te należą zwykle do rachunku zdań lub rachunku predykatów pierwszego rzędu.
Dla komputera wygodniejsze jest zwykle wnioskowanie w tył, choć czasem stosuje się też wnioskowanie w przód.
Przykładem twierdzenia, które zostało dowiedzione dopiero przez ATP jest "Algebry Robbinsa są boolowskie".
Automatyczne dowodzenie twierdzeń rachunku zdań Chodzi o stwierdzenie czy dane twierdzenie jest tautologią, lub czy jest spełnialne. Oba przypadki są wzajemnie połączone: zaprzeczenie twierdzenia jest spełnialne wtedy i tylko wtedy, gdy twierdzenie to nie jest tautologią.
Twierdzenia rachunku zdań zawsze są rozstrzygalne – choćby metodą brute force, która polega na sprawdzeniu 2n kombinacji wartości prawda-fałsz dla n zmiennych zdaniowych występujących w twierdzeniu.