自動定理證明 (自動定理證明, Automated theorem proving, ATP) 또는 自動 演繹 (Automated deduction)은 自動 推論 硏究의 한 分野로, 數學的 整理 들을 컴퓨터 프로그램 을 통해 形式的으로 證明하는 것, 또는 그에 對한 硏究를 가리킨다. 數學的 證明에 對한 自動化된 推論은 컴퓨터 科學 發展의 主要 原動力이었다.
