Автоматичне доведення (англ. Automated theorem proving) — доведення, реалізоване на програмному рівні. В основу покладено апарат математичної логіки. Використовуються ідеї теорії штучного інтелекту. Процес доведення базується на численні висловлень і логіці предикатів.
В силу нерозв'язності навіть достатньо простих теорій практичне застосування має лише напівавтоматичне людсько-машинне доведення. До того ж після повної автоматизації доведення називають вже обчисленням. Повністю автоматичною може бути лише перевірка доведення більш складних теорій (якщо його для цього підготувати).
В даний час автоматичне доведення теорем на виробництві застосовується в основному при розробці і верифікації інтегральних схем. Після того, як було виявлено помилку ділення в процесорах Pentium, складні модулі операцій з рухомою комою сучасних мікропроцесорів розробляються з особливою ретельністю. У нових процесорах AMD, Intel і інших фірм автоматичне доведення теорем використовується для перевірки того, що ділення і інші операції виконуються коректно.