증명,proof

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

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

증명된 명제,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.com/heuristic/theorem_yoo.htm


4색정리 four_color_theorem 의 증명의 특징 - tbw.






proof_assistant
{
similar? syn? : theorem_prover - 정리,theorem 증명기?



proof_theory
{
증명론 or 증명이론 ?
curr. RR:증명이론,proof_theory


[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 { WpKo:커리-하워드_대응 { tmp quote: "정확히 말하면 커리-하워드 대응은 논리의 증명 연산(proof_calculus)과 컴퓨터의 형 체계(type_system)가 대응된다는 진술이다. 예를 들어 힐베르트 체계(Hilbert_system)와 콤비네이터 논리(combinatory_logic)가, 자연 연역(자연연역,natural_deduction - curr at 연역,deduction - 작성중)과 람다 계산(람다대수,lambda_calculus)이 대응된다." } WpEn:Curry–Howard_correspondence rel. 동형사상,isomorphism } 라고 한다.

(후략)

... QQQ 이것의 이름? standard form?
일단 see WpEn:Rule_of_inference#Standard_form를 보면,

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

ex.
$\frac{A\to B\\A}{B}$
이것은 명제논리,propositional_logic의 RR:modus_ponens.

또한 Hilbert_systems for two 명제논리,propositional_logics 문단을 보면, 시퀀트,sequent notation - 시퀀트 표기법 sequent_notation - 은 다음 기호
{
WpEn:Turnstile_(symbol)
TeX: \vdash
⊢ U+22A2 right tack
⊦ U+22A6 assertion sign
}
를 써서
(전제1), (전제2) ⊦ (결론)
ex. modus ponens는 // RR:전건긍정,modus_ponens
(MP) A, A → B ⊢ B
이렇게 쓴다.
tmp search links:
Google:증명나무 Google:proof.tree Google:proof.tree latex
frac, array 로 그리는 것이 상당히 까다로운데 적당한 방법 찾을 것. 근데 mimetex에서 맘껏 쓸 수 없어서 문제다. 방법??

[edit]

Books


The Art of Proof
[ISBN-1441970223]


[edit]

Bmks en

[edit]

MKLINK

----