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

같이 보기 
 컴퓨터를 이용한 증명
 기호계산
 논리형 프로그래밍
 컴퓨터 과학

각주 

논리 프로그래밍
컴퓨터 과학 내 논리
인공지능
정형 기법