어떤 [[명제,proposition]]가 참([[진리,truth]])임을 명백하고 모호하지 않게(unequivocally) 입증하는(demonstrate) 엄밀한 수학적 주장([[논증,argument]]). 증명된 수학적 [[진술,statement]]은 [[정리,theorem]]라고 한다. (MW) Proof techniques * direct - 직접증명 direct_proof * indirect - see [[간접증명,indirect_proof]] { [[https://terms.naver.com/entry.naver?docId=3404938&cid=47324&categoryId=47324 수학백과: 간접증명]] - easy } * [[모순,contradiction]]을 이용 - see [[귀류법,proof_by_contradiction]] - ex. [[정지문제,halting_problem]] * [[귀납,induction]](귀납법) - proof by induction * [[수학적귀납법,mathematical_induction]] ''사실 귀납은 아니지 않나? 명칭만 귀납? 귀납 유사? 아님 귀납 맞음?....'' * 강한귀납? 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 * 대우에 의한 증명 contrapositive method of proof - [[proof_by_contraposition]]? 명제를 직접 증명하기 어려우면 그 명제의 [[대우,contraposition]]명제를 이용하는 * [[불변성,invariance]](그래서 그 양은 [[불변량,invariant]])을 사용하는 - rel. [[상수,constant]] ...(이목록에있는것들은 not mutually exclusive. 예를 들어 귀류법은 간접증명과 rel.).... QQQ 증명방법을 체계적으로 categorize하여 정리한 목록같은거 ??) * double counting, counting in two ways - [[WpEn:Double_counting_(proof_technique)]] * bijective proof, bijective_proof - 두 [[집합,set]] 사이 [[전단사,bijection]]를 이용한, [[전단사함수,bijective_function]]가 있는지를 찾는 ... WpEn:Bijective_proof * (combinatorial_proof WpEn:Combinatorial_proof 는 proof by double counting, bijective proof 둘 중 하나를 뜻한다. 위 둘) * visual proof = WpEn:Proof_without_words - 도형 등 [[시각화,visualization]]를 사용한. 일부 링크는 [[논리,logic]]에서 가져옴 i.e. MKL '''증명'''된 [[명제,proposition]] 중 자주 사용되며 기본이 되는 것들을 [[정리,theorem]]라고 한다. TBW: [[문제,problem]]를 푸는(solve) 것([[해,solution]]를 구하는 것)과 [[명제,proposition]]를 '''증명'''하는(prove) 것 ('''증명,proof'''을 작성하는 것)의 차이를 비교서술... 증명의 [[패턴,pattern]]이나 [[전략,strategy]] etc chk 맞는지 { [[명제,proposition]]가 [[참,true]]인지 [[거짓,false]]인지 알 수 없을 때 '''증명'''을 해서 알아낸다. 하지만 진리임에도(참이면서도) '''증명'''되지 않는 수학적 명제가 존재한다.[* https://terms.naver.com/entry.naver?docId=3570783&cid=58944&categoryId=58970] } 증명의 다른 표현: 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" Ggl:"semantic proof" [[proof-theoretic_semantics]] proof-theoretic semantics 증명이론적(증명론적) 의미론? WpEn:Proof-theoretic_semantics https://plato.stanford.edu/entries/proof-theoretic-semantics/ "proof-theoretic semantics" Ggl:"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)"[* https://terms.naver.com/entry.naver?docId=5668917&cid=60207&categoryId=60207] Agda { https://www.pls-lab.org/en/Agda } // Agda Ggl:Agda+proof Arend { https://www.pls-lab.org/en/Arend } // Arend Ggl:Arend+proof Coq { https://coq.inria.fr/ https://www.pls-lab.org/Coq https://en.wikipedia.org/wiki/Coq } Idris Ggl:Idris+proof PVS { https://www.pls-lab.org/en/PVS } // PVS Ggl: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. [[RR:증명이론,proof_theory]]'' Up: [[증명,proof]] [[이론,theory]] } // proof theory Ggl:"proof theory" ---- = 증명나무 = // 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_logic]]s 문단을 보면, [[시퀀트,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에서 맘껏 쓸 수 없어서 문제다. 방법?? ---- = Books = Book of Proof 3e [[ISBN(0989472124)]] http://www.people.vcu.edu/~rhammack/BookOfProof/ The Art of Proof [[ISBN(1441970223)]] Free Introduction to Mathematical Proofs textbook https://hefferon.net/proofs/ = Bmks en = https://www.cut-the-knot.org/proofs/ Archive of Formal Proofs https://www.isa-afp.org/ [[Isabelle]]{ https://isabelle.in.tum.de/ Up: [[proof_assistant]] }을 사용해 만든? Proof Explorer - Home Page - Metamath https://us.metamath.org/mpeuni/mmset.html The Development of Proof Theory (Stanford Encyclopedia of Philosophy) https://plato.stanford.edu/entries/proof-theory-development/ = MKLINK = [[derivation]] [[reduction]] [[theorem_proving]] - for [[정리,theorem]] ---- Twins: http://www.aistudy.com/math/proof.htm // ALSOIN [[theorem_proving]] http://www.aistudy.com/math/theorem_proving.htm [[WpKo:증명_(수학)]] - 쉬움 [[WpEn:Mathematical_proof]] [[https://terms.naver.com/entry.naver?docId=3405334&cid=47324&categoryId=47324 수학백과: 증명]] - 쉬움 https://ncatlab.org/nlab/show/proof http://oeis.org/wiki/Proofs https://proofwiki.org/wiki/Definition:Proof https://mathworld.wolfram.com/Proof.html