Theorem Proving
때때로 정리증명과 증명검증 (proof verification) 사이에 차이가 있다. 그 차이는 처리과정에서의 자동화의 정도에 관한 것이다. 사람이 아주 자세한 단계별 증명을 하고, 컴퓨터는 각 단계를 체크만 한다면 proof verification 라고 부른다. 그와는 반대로 사람이 증명할 정리를 단순히 서술만 하고, 컴퓨터가 모든 필요한 보조정리 (lemmas) 를 제안하고 전체 증명을 한다면 정리증명이 되는 것이다. 실제로는 "관심있는" 정리를 완전히 자동으로 증명할 수 있는 범용 시스템은 없으며, 대부분의 정리증명은 자동화의 정도가 다양한 여러 가지 방법으로 이루어진다. 따라서 그 두가지 방법의 차이는 줄어들고 그 연속체 (continuum) 두 개를 모두 정리증명 이라고 한다.
또다른 차이가 정리증명과 다른 테크닉 사이에 있을 수 있다. 즉 공리에서 출발하여 추론규칙 (Inference Rule) 을 사용해서 새로운 추론 단계를 만드는 전통적인 증명을 구성하는 과정이 있다면 그것은 정리증명일 것이다. 다른 테크닉들은 많은 가능한 문장들을 맹목적으로 열거하는 것과 같은 model checking 을 포함한다 (비록 model checkers 를 실제로 구현할 때는 더 영리해야 하고 단순히 맹목적인 것으로 환원하기는 않지만). 추론규칙으로서 model checking 을 사용하는 합성 (hybrid) 정리증명 시스템이 있다. 또한 특별한 정리를 증명하기 위해 작성된 프로그램이 있는데 만일 그 프로그램이 어떤 결과와 함께 종료된다면 그 정리는 참이라는 (보통은 비형식적인) 증명을 하는 것이다. 이것의 좋은 예로써 four color theorem 의 기계의 도움을 받는 증명 (machine-aided proof) 이며, 그것이 수작업에 의한 체크가 근본적으로 불가능한 최초의 수학적 증명이냐 아니냐 하는 논쟁이 있었다. 또다른 예는 게임 Connect 4 에서 처음 플레이어가 이긴다는 것을 증명하는 것이다.
자동정리증명의 상업적인 용도는 주로 통합회로 (integrated circuit) 설계 와 검증에 대개 집중되어 있다. Pentium FDIV bug 이후에 현대 마이크로프로세서의 복잡한 Floating Point Units 은 초정밀조사 (extra scrutiny) 로 설계되었다. AMD, Intel 등의 회사에서 만든 최신 프로세서에서, 자동정리증명은 분리된 다른 작동이 정확한지를 검증하기 위해 사용되어 왔다. .................. (Wikipedia : Automated theorem proving)
5 세대 컴퓨터 (Fifth Generation Computer) 프로젝트에서 만들어진 자동 정리증명기 MGTP
term :
정리증명 (Theorem Proving) 도출법 (Resolution) 증명 (Proof) 공리 (Axiom) 논리학 (Logic) 수학 (Mathematics) 인공지능 (Artificial Intelligence)
site :
Wikipedia : Automated theorem proving
AI Topics : Automated Theorem Proving
paper :
정리증명 : 유석인 : 정리 증명을 위해 이용되는 두 개의 시스템, 즉 비교흡수 부정 (resolution refutation) 시스템과 규칙에 기초한 연역 (rule-based deduction) 시스템에 대해 고찰한다 ........
video :
컴퓨터과학이 여는 세계 - 프로그램은 논리증명 : SNU : 이광근 : 2016/03/07 ... 동영상 82개