자동정리증명(自動定理證明, Automated theorem proving, ATP) 또는 자동 연역(Automated deduction)은 자동 추론 연구의 한 분야로, 수학적 정리들을 컴퓨터 프로그램을 통해 형식적으로 증명하는 것, 또는 그에 대한 연구를 가리킨다. 수학적 증명에 대한 자동화된 추론은 컴퓨터 과학 발전의 주요 원동력이었다.
