Proof

 
수학에서 증명이라고 하는 것은 어떤 공리 (Axiom) 가 주어졌을 때 관심있는 어떤 문장이 반드시 참 이라고 하는 것을 보이는 것이다. 증명은 논리 (Logic) 를 사용하지만 어느정도의 애매모호함을 허용하는 자연어을 포함하기도 한다. 순수하게 형식적 증명을 고려한 증명이론 (proof theory) 의 맥락에서, 완전히 형식적인 시연 (demonstration) 이 아닐 경우를 "social proof" 라고 한다. 그 차이는 작금의 mathematical practice, quasi-empiricism in mathematics, 그리고 소위 folk mathematics (그 용어의 두가지 의미에서) 의 많은 검사를 하게했다. 수학철학 (philosophy of mathematics) 은 증명에서의 언어와 논리의 역할을 다루고, 그리고 하나의 언어로서의 수학을 다룬다.
 
형식주의 (formalism) 를 어떻게 보느냐에 상관없이, 참으로 증명되는 결과는 하나의 정리 (theorem) 이다 ; 완전한 형식증명에서 그것은 최종선 (final line) 이며, 공리 그 자체로부터 어떻게 완전한 증명이 이루어지는 지를 보여준다. 일단 하나의 정리가 증명되면 그것은 다른 문장을 증명하기 위한 기초로 사용될 수 있다. 소위 수학의 기본 (foundations of mathematics) 은 증명할 수도 없고, 할 필요도 없는 문장들이다. 이것들은 한때 수학철학의 주요한 연구였었다. 오늘날에는 실제적인, 즉 받아들여 질 수 있는 기술에 더 초점을 둔다.
 
흔한 증명 기술은 다음과 같다.

확률증명 (probabilistic proof) 은 하나의 예가 확률이론의 방법에 의해 존재한다는 것이 보여지는 증명을 의미하며 - 어떤 정리가 '아마도' 참일 것이다 라는 주장에 의한 것이 아니다. 후자의 추론 형식을 '가능성 주장 (plausibility argument)' 라고 부른다 ; Collatz conjecture 의 경우에서 처럼 참된 증명과는 거리가 멀다는 것이 명확하다. 확률증명은 존재 (existence) 정리를 보여주는 여러 방법중 하나로서, 구축에 의한 증명과는 다르다.

예를들면 "어떤 X 가 f(X) 를 만족한다" 를 증명하고자 한다면, existence or nonconstructive 증명은 f(X) 를 만족하는 X 가 존재한다 는 것을 증명할 것이지만, 그러한 X 가 어떻게 얻어지는 지를 말하지 않는다. 그러나 constructive 증명에서는 그렇게 할 것이다.

참이라고 생각되지만 아직 증명되지는 않은 문장을 추측 (conjecture) 라고 부른다.

때때로 어떤 문장이 주어진 공리 집합으로부터 아마도 증명될 수 없을 것이라는 것을 증명하는 것은 가능하다 ; continuum hypothesis 를 그 예로서 들 수 있다. 대부분의 공리 시스템에서, 증명될 수도 없고 반증될 수도 없는 문장들이 존재한다. 괴델의 불완전성 정리 (Incompleteness Theorem) 를 참고하라.  .... (Wikipedia : Mathmatical proof)

..... 이 기술은 다음과 같은 하나의 법칙에 의존한다.

(1) 의 특별한 경우는 다음과 같다.

이것은 추론이나 정리 증명의 많은 컴퓨터 프로그램의 기초 (basis) 이다. ... (Richard Johnsonbaugh, 1999)

term :

증명 (Proof)    도출법 (Resolution)   정리증명 (Theorem Proving)   

paper :

증명 기법 : Peter Linz

증명 (Proof)   분해증명 (Resolution Proof) : Richard Johnsonbaugh