3.1 증명 전략 (Proof Strategy) 이산수학 (Discrete Mathematics) 2006년 봄학기 문양세

Slides:



Advertisements
Similar presentations
Lecture 9 프로그램 실행의 비용 computation cost – 시간 time, 메모리 memory – tractable vs intractable problems.
Advertisements

(Mathematical Induction)
Inductive semantic definition. inductive semantic definition.
이산수학(Discrete Mathematics)  정수와 나눗셈 (The Integers and Division)
이산수학(Discrete Mathematics)  정수와 나눗셈 (The Integers and Division)
귀납과 재귀 (Induction and Recursion)
적분방법의 연속방정식으로부터 Q=AV 방정식을 도출하라.
이산수학 논리∙명제에서 알고리즘까지 √ 원리를 알면 IT가 맛있다 ehanbit.net.
양태, 증거성, 의외성 통사론 기초
Chapter 7. 조건문.
Report #2 - Solution 문제 #1: 다음과 같이 프로그램을 작성하라.
REINFORCEMENT LEARNING
Problems of Finite Difference Method (유한차분법)
이산수학(Discrete Mathematics)
이산수학(Discrete Mathematics)
최현진 정경대학 정치외교학과 국제정치론 2014 가을학기 제1주(2) 최현진 정경대학 정치외교학과
Mathematics Review for Algorithm
공개키 암호화 프로그래밍 전자상거래보안.
11장. 포인터 01_ 포인터의 기본 02_ 포인터와 Const.
2007 1학기 11 프로젝트 기초 실습.
보고서 #5(제출기한: 10/14) 다음 문제를 해결하시오.
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
Mathematics Review for Algorithm
일차방정식의 풀이 일차방정식의 풀이 순서 ① 괄호가 있으면 괄호를 먼저 푼다.
이산수학(Discrete Mathematics)
이산수학(Discrete Mathematics)
Ⅲ. 이 차 방 정 식 1. 이차방정식과 그 풀이 2. 근 의 공 식.
1.4 중첩된 한정기호 (Nested Quantifiers) 이산수학 (Discrete Mathematics)
MATLAB
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy)
프로그래밍 개요
어서와 C언어는 처음이지 제14장.
(Relations and Its Properties)
2002년도 대한토목학회 학술발표회 Semi-active Fuzzy control for Seismic Response Reduction Using MR Damper K-M Choi1), H-J Jung1) J-H Lee2) and I-W Lee1) 1) Department.
자료구조: CHAP 7 트리 –review 순천향대학교 컴퓨터공학과 하 상 호.
이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy)
Term Projects 다음에 주어진 2개중에서 한 개를 선택하여 문제를 해결하시오. 기한: 중간 보고서: 5/30 (5)
Chapter 2. 논리와 명제.
이산수학(Discrete Mathematics)
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
이산수학 (Discrete Mathematics)
이산수학(Discrete Mathematics)
이산수학(Discrete Mathematics)  명제의 동치 (Propositional Equivalence)
논리와 명제 기본 개념 논리 연산자와 진리표 논리적 동치 한정 기호.
6.1 점화 관계 (Recurrence Relations)
데이터마이닝, 빅데이터, 데이터과학: 정의 데이터마이닝(data mining)
메모리 타입 분석을 통한 안전하고 효율적인 메모리 재사용
3강. 컴퓨터와의 기본적인 소통수단 - I 연산자란? 컴퓨터와 소통하기 위한 다양한 방법들
알고리즘 알고리즘이란 무엇인가?.
이산수학 (Discrete Mathematics)
이산수학(Discrete Mathematics) 비둘기 집 원리 (The Pigeonhole Principle)
약식 진리표를 이용한 타당성 증명 진리표 그리기 방법의 한계
제12장. Algorithmic Computation의 한계
이산수학(Discrete Mathematics)  집합 연산 (Set Operations)
점화와 응용 (Recurrence and Its Applications)
자연연역과 연역 추론의 법칙들 기계적인 진리함수적 연산 방식을 이용하는 진리표 그리기 방식과 달리, ‘자연연역(natural deduction)’은 타당한 연역적 추론의 법칙들을 활용하여 논증의 타당성 여부를 검증하는 방식이다.
쉽게 배우는 알고리즘 2장. 점화식과 점근적 복잡도 분석
이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy)
제 22 강 논리식 및 논리 값 shcho.pe.kr.
이산수학(Discrete Mathematics) 수열과 합 (Sequences and Summations)
제 3장. Regular Languages 와 Regular Grammars
(Predicates and Quantifiers)
이산수학(Discrete Mathematics)  술어와 한정기호 (Predicates and Quantifiers)
수치해석 ch3 환경공학과 김지숙.
DNA Implementation of Version Space Learning
(Permutations and Combinations)
교착 상태 해결 : 교착 상태 탐지 교착 상태 탐지(Deadlock Detection)
진리표를 이용한 타당성 증명 진리표(truth table) : 단순 문장들이 진리값을 상이하게 가질 수 있는 가능한 모든 경우를 남김없이 열거한 표 (ex) 오늘은 날씨가 맑거나 비가 올 것이다. 오늘은 날씨가 맑다 비가 온다 오늘은 날씨가 맑거나 비가 올 것이다. T.
Presentation transcript:

3.1 증명 전략 (Proof Strategy) 이산수학 (Discrete Mathematics) 2006년 봄학기 문양세 강원대학교 컴퓨터과학과

$3.1 Proof Strategy (review $1.5 Methods of Proof) Overview of Chapter 3 3.1 Proof Strategy $3.1 Proof Strategy (review $1.5 Methods of Proof) $3.2 Sequences and Summations $3.3 Mathematical Induction $3.4 Recursive Definitions and Structural Induction $3.5 Recursive Algorithms

추론 규칙(rules of inference) 용어(Terminology) (1/3) 3.1 Proof Strategy 정리(theorem) 정리란 참(true)으로 밝혀진 명제이다. A statement that has been proven to be true. 공리(axiom, postulates) 증명된 정리 혹은 증명하고자 하는 정리의 가정이다. Assumptions (often unproven) defining the structures about which we are reasoning. 추론 규칙(rules of inference) 논리적으로 유효한 주장(logically valid deductions)을 사용하여, 가정을 결론으로 이끌어가는 증명의 과정이다. Patterns of logically valid deductions from hypotheses to conclusions.

용어(Terminology) (2/3) 보조정리(lemma) 따름정리(corollary) 3.1 Proof Strategy 보조정리(lemma) 다른 정리를 증명하는데 사용하는 간단한 정리이다. A minor theorem used as a stepping-stone to proving a major theorem. “복잡한 내용이 정리이고, 간단한 내용이 보조정리”를 의미하는 것은 아님에 유의! 따름정리(corollary) 어떤 정리가 증명되면, 이에 의하여 자연스럽게 증명되는 정리이다. A minor theorem proved as an easy consequence of a major theorem.

용어(Terminology) (3/3) 가설(conjecture) 이론(theory) 3.1 Proof Strategy 가설(conjecture) 증명되지는 않았지만 참으로 믿어지는 명제이다. A statement whose truth values has not been proven. (A conjecture may be widely believed to be true, regardless.) 이론(theory) 주어진 공리(axiom)으로부터 증명이 가능한 모든 정리(theorem)의 집합이다. The set of all theorems that can be proven from a given set of axioms.

추론 규칙 (Inference Rules) (1/2) 3.1 Proof Strategy 추론 규칙의 의미 주어진 가정(antecedent)이 참(true)일 때, 결론(consequent)가 참이라는 패턴 “x = 3”(= p)이면, “x + 1 = 4”(= q)이다. 상기 예에서 p(가정)가 참이면, q(결론)은 참이 된다. 추론 규칙의 표기 antecedent 1 antecedent 2 … 가정  consequent 결론 “”은 “therefore”를 의미한다.

추론 규칙 (Inference Rules) (2/2) 3.1 Proof Strategy 각 추론 규칙은 “항진 명제인 함축(implication)”에 해당한다. ant.1 ant.2 …  con. 에 해당하는 tautology는 “((ant.1  ant.2  … )  con.”이다.

추론 규칙 종류 Rule of inference Tautology Name p  p  q p  (p  q) 3.1 Proof Strategy Rule of inference Tautology Name p  p  q p  (p  q) Addition p  q  p (p  q)  p Simplification q  p  q ((p)  (q))  (p  q) Conjunction p  q  q (p  (p  q))  q Modus ponens (the mode of affirming) ¬q  ¬p (¬q  (p  q))  ¬p Modus tollens (the mode of denying) q  r  p  r ((p  q)  (p  r))  (p  r) Hypothetical syllogism p  q ¬p ((p  q)  ¬p)  q Disjunctive syllogism ¬p  r  q  r ((p  q)  (¬p  r))  (q  r) Resolution

Formal Proofs Format Proof의 정의 예제 6 (in $1.5) 3.1 Proof Strategy Format Proof의 정의 Formal proof란 주어진 가정(antecedent)에 기반하여 추론 규칙을 적용한 일련의 단계(step)를 거쳐서 결론(consequent)을 도출하는 과정이다. 증명(proof)은 주어진 모든 가정이 true일 때 결론이 true임을 보이는 과정이다. 예제 6 (in $1.5) 다음 가정이 “We will be home by sunset.”이라는 결론을 도출함을 보여라. “It is not sunny this afternoon and it is colder than yesterday.” “We will go swimming only if it is sunny.” “If we do not go swimming, then we will take a canoe trip.” “If we take a canoe trip, then we will be home by sunset.” 풀이 p = “It is sunny this afternoon.” q = “It is colder than yesterday.” r = “We will go swimming.” s = “We will take a canoe trip.” t = “We will be home by sunset.” 단계 과정 이유 1 ¬p  q 가정 2 ¬p 단계 1의 simplification 3 r  p 4 ¬r 단계 2, 3 기반의 Modus tollens 5 ¬r  s 6 s 단계 4, 5 기반의 Modus ponens 7 s  t 8 t 단계 6, 7 기반의 Modus ponens

Inference Rules for Quantifiers (1/2) 3.1 Proof Strategy Quantifier를 포함하는 추론 규칙 Universal instantiation xP(x)가 주어졌을 때, xP(x)이 true라면, domain에 속하는 임의의 값(요소) c에 대해서 P(c)가 true임을 보이는데 사용되는 추론 규칙이다. Universal generalization xP(x)가 주어졌을 때, domain에 속하는 모든 값(요소) c에 대해서 P(c)가 true이면, xP(x)가 true임을 보일 때 사용되는 추론 규칙이다. Existential instantiation xP(x)가 주어졌을 때, xP(x)가 true라면, domain안에 P(c)를 true로 하는 값(요소) c가 적어도 하나 이상 있다는 것을 나타내는 추론 규칙이다. Existential generalization xP(x)가 주어졌을 때, 특정 값(요소) c에 대해서 P(c)가 true이면, xP(x)이 true라는 추론 규칙이다.

Inference Rules for Quantifiers (2/2) 3.1 Proof Strategy Quantifier 사용 명제의 추론 규칙 정리 Rule of inference Tautology Name xP(x)  P(c) xP(x)  P(c) Universal instantiation P(c) for an arbitrary c P(c) for an arbitrary c  xP(x) Universal generalization xP(x)  P(c) for some c xP(x)  P(c) for some c Existential instantiation P(c) for an some c P(c) for an some c  xP(x) Existential generalization

Proof Methods 함축(implication) p  q의 증명을 위하여, 다음 방법들을 사용한다. 3.1 Proof Strategy 함축(implication) p  q의 증명을 위하여, 다음 방법들을 사용한다. Direct proof: Assume p is true, and prove q. Indirect proof: Assume ¬q, and prove ¬p. (대우의 증명에 해당) Vacuous proof: Prove ¬p by itself. (가정이 false임을 증명) Trivial proof: Prove q by itself. (결론이 항시 true임을 증명) Proof by cases: To prove (p1  p2  ....  pn)  q, prove ((p1  q)  (p2  q)  ....  (pn  q)) Proof by Contradiction: A method for proving p. Assume ¬p, and prove some proposition q is contradiction (i.e., q is always false.) Then, ¬pF, which is only true if ¬p=F Thus, p is true.  주어진 가정(p)을 부정(false)했을 때 항상 false가 되는 명제 q가 있음을 보이면, p의 가정이 잘못되었으므로 p는 true가 된다.

Forward & Backward Reasoning (1/2) 3.1 Proof Strategy Forward Reasoning (전진 추론) 주어진 가정 및 알려진 정리 등을 사용하여 결론을 도출해 가는 방법 Example: Let n  N, such that n is not divisible by 2 or 3. Then, n2−1 is divisible by 24. Since n is not divisible by 2 or 3, it follows that n = 6k + 1 or 6k + 5. (6k, 6k + 2, 6k + 3, and 6k + 4 are divisible by 2 or 3.) Case 1: (n = 6k + 1) n2 − 1 = ((6k + 1)2 − 1) = (36k2 + 24k) = 12(3k + 1)k 12(3k + 1)k is divisible by 24 since (3k + 1)k is even. Case 2: (n = 6k + 5) n2 − 1 = (n + 1)(n − 1) = (6k + 6)(6k + 4) = 12(k + 1)(3k + 2) 12(k + 1)(3k + 2) is divisible by 24 since (k + 1)(3k + 2) is even. Therefore, n2 − 1 is divisible by 24.

Forward & Backward Reasoning (2/2) 3.1 Proof Strategy Backward Reasoning (후진 추론) 결론(q)에서 출발하여 가정(p)이 참임을 이끌어 가는 방법 Example: Let a,b  R, with ab. Then (a+b)/2 > . Conclusion is true if (a + b) > , which is true if (a + b)2 > 4ab, which is true if a2 + 2ab + b2 > 4ab, which is true if a2 − 2ab + b2 > 0, which is true if (a − b)2 > 0, which is true. 상기 예제를 Forward Reasoning으로 증명하는 경우 (a − b)2 > 0  a2 − 2ab + b2 > 0  a2 + 2ab + b2 > 4ab  (a + b)2 > 4ab  (a + b) >  (a+b)/2 >

가설과 증명 (Conjecture & Proof) 3.1 Proof Strategy 가설의 형식화 가능한 많은 형태의 증거에 기초하여 가설을 형식화한다. 기존 정리나 명제를 사용하여 원하는 가설을 만들어내거나, 직관이나 결과가 성립한다는 믿음에 기초하여 가설을 만들어 낸다. 가설의 증명 가설이 형식화되면 목표는 이를 증명하는 것이다. 증명하게 되면, 가설은 정리가 된다. 증명하지 못하면, 가설은 결국 가설로 남게 된다. 예제 가설: a > 2이고 n이 양의 정수이면, an − 1은 합성수이다. (예: 32 − 1 = 8 = 23) (누군가가 직관(뛰어난 통찰력)을 사용하여 이런 가설을 생각했다 하자.) 증명: an − 1 = (a − 1)(an-1 + … + a + 1) 1 < (a − 1) < an − 1이므로, a − 1은 an − 1의 인수이고, 결국 an − 1은 합성수이다.  결과적으로, 상기 가설은 정리가 된다.

가설과 반례 (Conjecture & Conterexample) 3.1 Proof Strategy 가설에 대한 반례 그럴듯한 가설을 제시하였는데, 이의 증명이 어려운 경우, 반례를 생각하게 된다. 반례를 들 수 있으면, 그 가설은 false가 되어 정리가 되지 못한다. 예제 (Leonhard Euler) 가설: n  3인 모든 정수 n에 대해서, n − 1개의 양의 정수들의 n 제곱의 합은 어떤 수의 n제곱이 될 수 없다. (예: n = 3, a3 + b3을 만족하는 c3은 없다.) 반례 1(n = 4): 95,8004 + 217,5194 + 414,5604 = 422,4814 (1988, Noam Elkies) 반례 2(n = 5): 275 + 845 + 1105 + 1335 = 1445 (1966, Lander & Parkin) 나머지는 밝혀진 반례가 없다. 그렇다면, 다른 경우(예: n  6)에 대해서는 가설이 혹시 참이 아닐까?

유명한 가설들 (1/2) 페르마(Fermat)의 마지막 정리 방정식 3.1 Proof Strategy 페르마(Fermat)의 마지막 정리 방정식 가설: xn + yn = zn은 n > 2인 정수일 때, xyz  0인 x, y, z에 대해 해를 갖지 않는다. n = 3인 경우에 대해서는 Euler에 의해 증명됨 n = 4인 경우에 대해서는 Fermat에 의해 증명됨 나머지에 대해서는 타원 곡선 이론이라는 매우 복잡한 정수론 분야에 의해서 1990년대에 Andrew Wiles에 의해 비로소 증명됨 (350년 만에 증명됨) 비로소, 페르마의 마지막 방정식은 가설에서 정리가 되었다.

유명한 가설들 (2/2) 골드바흐(Christian Goldbach) 가설: n > 2인 짝수 n은 두 소수의 합이다. 3.1 Proof Strategy 골드바흐(Christian Goldbach) 가설: n > 2인 짝수 n은 두 소수의 합이다. 예: 4 = 2 + 2, 6 = 3 + 3, 8 = 5 + 3, 10 = 7 + 3, 12 = 7 + 5, … 컴퓨터 이전: 백만 단위까지 증명 (by hand) 컴퓨터 이후: 4∙1014까지 증명(2002년 중반) 아직(?) 증명되지는 않았으나 대부분 수학자는 true라 믿고 있음 유사 가설: n > 2인 짝수 n은 적어도 6개의 소수의 합으로 표현됨 (1995, Ramare 증명)  아직(?) 증명되지는 않았으나 대부분 수학자는 true라 믿고 있고, 곧 풀릴 것?

The Halting Problem (정지 문제) (1/2) 3.1 Proof Strategy Alan Turing discovered in the 1930’s that there are problems unsolvable by any algorithm. (튜링은 “어떠한 알고리즘으로도 풀 수 없는 문제가 있음”을 밝혔다.) The desired function is H(P,I) = the truth value of the statement “Program P, given input I, eventually halts”. (H(P,I) = “프로그램 P와 P의 입력 I가 주어졌을 때, 이 프로그램 P가 정지하는지”의 여부를 판단하는 함수) 튜링은 이러한 함수 H(P,I)가 존재하지 않음을 증명하였다. Implies general impossibility of predictive analysis of arbitrary computer programs. (임의의 프로그램에 대한 예측 분석이 일반적으로 불가능함을 의미한다.)

The Halting Problem (정지 문제) (2/2) 3.1 Proof Strategy 정지 문제의 증명 (by contradiction) H(P,I) = 주어진 Program P와 입력 I에 대해서, 만일 P가 정지하면 “정지”를 출력하고, 그렇지 않으면(만일 P가 무한루프이면) “무한루프”를 출력한다. K(P) = 주어진 Program P에 대해서 H(P,P)가 “정지”를 출력하면, 무한루프를 수행하고, H(P,P)가 “무한루프”를 출력하면, 정지한다. H(K,K) = (H(P,I)의 입력으로 P = K와 I = K를 주는 경우) H(K,K)가 “정지”를 출력하면, K(K)는 무한루프를 수행한다.  모순!  H()는 출력으로 Program K가 정지한다고 하였는데, 실제 K는 무한루프를 수행하므로 모순이다. H(K,K)가 “무한루프”를 출력하면, K(K)는 정지한다.  모순!  H()는 출력으로 Program K가 무한루프를 수행한다 하였는데, 실제 K는 정지하므로 모순이다. 결국, 정지 문제를 해결하는 H(P,I)는 존재하지 않는다!