Difference between r1.56 and the current

@@ -9,7 +9,7 @@

* 강한귀납? strong_induction Naver:strong.induction Google:strong.induction
* 구조귀납? structural_induction Naver:structural.induction Google:structural.induction { WpEn:Structural_induction }
* [[반례,counterexample]]를 하나 이상 들기? - proof by counterexample

* 모든 [[경우,case]]를 따지기? exhaustive case analysis

* 모든 [[경우,case]]를 따지기? exhaustive case analysis / ex. proof by truth table : [[논리학,logic]], [[불_대수,Boolean_algebra]]의 어떤 간단한 문제들은 [[진리표,truth_table]]를 사용한 증명이 가능

* 대우에 의한 증명 contrapositive method of proof - [[proof_by_contraposition]]? 명제를 직접 증명하기 어려우면 그 명제의 [[대우,contraposition]]명제를 이용하는
* [[불변성,invariance]](그래서 그 양은 [[불변량,invariant]])을 사용하는 - rel. [[상수,constant]]
...(이목록에있는것들은 not mutually exclusive. 예를 들어 귀류법은 간접증명과 rel.).... QQQ 증명방법을 체계적으로 categorize하여 정리한 목록같은거 ??)

@@ -215,5 +215,4 @@

https://proofwiki.org/wiki/Definition:Proof
https://mathworld.wolfram.com/Proof.html

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

Proof techniques

direct - 직접증명 direct_proof
indirect - see 간접증명,indirect_proof { 수학백과: 간접증명 - easy }
모순,contradiction을 이용 - see 귀류법,proof_by_contradiction - ex. 정지문제,halting_problem
귀납,induction(귀납법) - proof by induction
- 수학적귀납법,mathematical_induction 사실 귀납은 아니지 않나? 명칭만 귀납? 귀납 유사? 아님 귀납 맞음?....
- 강한귀납? strong_induction strong.induction strong.induction
- 구조귀납? structural_induction structural.induction structural.induction { Structural_induction }
반례,counterexample를 하나 이상 들기? - proof by counterexample
모든 경우,case를 따지기? exhaustive case analysis / ex. proof by truth table : 논리학,logic, 불_대수,Boolean_algebra의 어떤 간단한 문제들은 진리표,truth_table를 사용한 증명이 가능
대우에 의한 증명 contrapositive method of proof - proof_by_contraposition? 명제를 직접 증명하기 어려우면 그 명제의 대우,contraposition명제를 이용하는
불변성,invariance(그래서 그 양은 불변량,invariant)을 사용하는 - rel. 상수,constant

...(이목록에있는것들은 not mutually exclusive. 예를 들어 귀류법은 간접증명과 rel.).... QQQ 증명방법을 체계적으로 categorize하여 정리한 목록같은거 ??)

double counting, counting in two ways - Double_counting_(proof_technique)
bijective proof, bijective_proof - 두 집합,set 사이 전단사,bijection를 이용한, 전단사함수,bijective_function가 있는지를 찾는 ... Bijective_proof
(combinatorial_proof Combinatorial_proof는 proof by double counting, bijective proof 둘 중 하나를 뜻한다. 위 둘)
visual proof = Proof_without_words - 도형 등 시각화,visualization를 사용한.

일부 링크는 논리,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.

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

semantic proof

proof-theoretic_semantics
proof-theoretic semantics
증명이론적(증명론적) 의미론?

Proof-theoretic_semantics
https://plato.stanford.edu/entries/proof-theoretic-semantics/
"proof-theoretic semantics"

proof-theoretic semantics
Up: 증명,proof 이론,theory -> 증명이론,proof_theory or 증명론,proof_theory / 의미론,semantics?

proof_system - writing
MKLINK: 형식체계,formal_system
https://proofwiki.org/wiki/Definition:Proof_System

formal_proof - writing
MKLINK: 형식체계,formal_system
2023-05-24 :
https://proofwiki.org/wiki/Definition:Formal_Proof
redir to https://proofwiki.org/wiki/Definition:Proof_System/Formal_Proof

tableau_proof
https://proofwiki.org/wiki/Definition:Tableau_Proof

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

번역들
"증명보조기(proof assistants)"[2]

Agda { https://www.pls-lab.org/en/Agda } // Agda

Agda proof
Arend { https://www.pls-lab.org/en/Arend } // Arend

Arend proof
Coq {

https://coq.inria.fr/
https://www.pls-lab.org/Coq
https://en.wikipedia.org/wiki/Coq }

Idris

Idris proof

PVS { https://www.pls-lab.org/en/PVS } // PVS

PVS proof
...

Bmks en
Proof Assistants Stack Exchange
https://proofassistants.stackexchange.com/

Twin
https://www.pls-lab.org/en/Proof_assistants
}

proof_theory
{
proof theory
증명론 or 증명이론 ?
curr. 증명이론,proof_theory

Up: 증명,proof 이론,theory
} // proof theory

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 {

커리-하워드_대응 { 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.