자동 정리 증명

자동 정리 증명의 목표는 추측(목표 정리)과 알려진 사실들의 지식 기반을 주어졌을 때, 형식 언어로 증명을 자동으로 생성하는 것입니다. 이 기술은 소프트웨어 및 하드웨어 시스템의 검증과 합성 등 다양한 분야에서 중요한 응용 프로그램을 가지고 있습니다.