어떤 명제,proposition가 참임을 명백하고 모호하지 않게(unequivocally) 입증하는(demonstrate) 엄밀한 수학적 주장(argument). 증명된 수학적 진술(statement)은 정리,theorem라고 한다. (MW)

Proof techniques

direct - 직접증명
indirect - see 간접증명,indirect_proof { 수학백과: 간접증명 - easy }
모순,contradiction을 이용 - see 귀류법,proof_by_contradiction
귀납,induction(귀납법)
- 수학적귀납법,mathematical_induction 사실 귀납은 아니지 않나? 명칭만 귀납? 귀납 유사? 아님 귀납 맞음?....
- 강한귀납? strong_induction strong.induction strong.induction
- 구조귀납? structural_induction structural.induction structural.induction { Structural_induction }
반례,counterexample를 하나 이상 들기?
모든 경우,case를 따지기? exhaustive case analysis
대우에 의한 증명 contrapositive method of proof - 대우,contraposition
...(이목록에있는것들은 not mutually exclusive. 예를 들어 귀류법은 간접증명과 rel. QQQ 증명방법을 체계적으로 categorize하여 정리한 목록같은거 ??)

일부 링크는 논리,logic에서 가져옴 i.e. mklink

증명된 명제,proposition 중 자주 사용되며 기본이 되는 것들을 정리,theorem라고 한다.

TBW:
문제,problem를 푸는(solve) 것(해,solution를 구하는 것)과
명제,proposition를 증명하는(prove) 것 (증명,proof을 작성하는 것)의 차이를 비교서술...

증명의 패턴,pattern이나 전략,strategy etc

chk 맞는지
{
명제,proposition가 참,true인지 거짓,false인지 알 수 없을 때 증명을 해서 알아낸다.
하지만 진리임에도(참이면서도) 증명되지 않는 수학적 명제가 존재한다.[1]
}

증명의 다른 표현: demonstration

proof란 수학의 명제,proposition가 참인지 거짓인지를 demonstrate하는 것?? chk

ALSOIN 정리,theorem
정리 증명 (Theorem Proving) (from 인공지능 원론, 유석인, 1988)
http://www.aistudy.co.kr/heuristic/theorem_yoo.htm

semantic_proof
https://everything2.com/title/semantic proof

[edit]

증명나무 ¶

// tmp, cleanup; from SNU이광근 컴여세 p177 and wpen

'논리적인 징검다리' (널리 쓰이는 용어는 아님)
분수,fraction 표기를 사용하며

분자: 알려진 사실
분모: 유도한 새로운 사실

ex. "A가 사실이고 B가 사실이면 (A 그리고 B)도 사실이다"는 이렇게 나타냄. $\frac{A\quad B}{A\wedge B}$

몇가지 징검다리들은 다음과 같다.

A and B가 사실이면 A도 사실이고 B도 사실이다. $\frac{A\wedge B}{A},\; \frac{A\wedge B}{B}$

A가 사실이라는 가정 하에 B가 사실이면, 'A이면 B'도 사실이다. $\begin{array}{c}\bar{A}\\\vdots\\ B\\\hline A\Rightarrow B\end{array}$
(가정,assumption한 것 위에는 윗줄을 긋는다.)

'A이면 B'가 사실이고 A가 사실이면, B가 사실이다. $\frac{A\Rightarrow B\quad A}{B}$

A가 사실이면, 임의의 B에 대해서 'A 또는 B'도 사실이고 'B 또는 A'도 사실이다. $\frac{A}{A\vee B}\;\frac{A}{B\vee A}$

이것은 새로운 사실을 증명,proof하는 과정.

(중략)

이런 증명과정은 프로그래밍언어,programming_language 에서 제공하는 것(statement?)들과 일대일 대응. 프로그램 한 줄 ↔ 증명의 한 줄. 이것을 커리-하워드_동치 Curry-Howard_isomorphism {

커리-하워드_대응 { tmp quote: "정확히 말하면 커리-하워드 대응은 논리의 증명 연산(proof_calculus)과 컴퓨터의 형 체계(type_system)가 대응된다는 진술이다. 예를 들어 힐베르트 체계(Hilbert_system)와 콤비네이터 논리(combinatory_logic)가, 자연 연역(자연연역,natural_deduction - curr at 연역,deduction - 작성중)과 람다 계산(람다대수,lambda_calculus)이 대응된다." }

Curry–Howard_correspondence rel. 동형사상,isomorphism } 라고 한다.

(후략)

... QQQ 이것의 이름? standard form?
일단 see

Rule_of_inference#Standard_form를 보면,

standard_form:

전제1
전제2
…
전제n
결론

ex.