이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy)

Slides:



Advertisements
Similar presentations
게임이론 Von Neumann Theory of Games and Economic Behavior with Oskar Morgenstern, widely recognized as the first formal treatment.
Advertisements

2012 년 봄학기 강원대학교 컴퓨터과학전공 문양세 이산수학 (Discrete Mathematics)  중첩된 한정기호 (Nested Quantifiers)
Lecture 9 프로그램 실행의 비용 computation cost – 시간 time, 메모리 memory – tractable vs intractable problems.
(Mathematical Induction)
Compiler Lecture Note, Inroduction to FL theory
6.9 Redundant Structures and the Unit Load Method
귀납과 재귀 (Induction and Recursion)
Chaper 2 ~ chaper 3 허승현 제어시스템 설계.
정 의 학습의 일반적 정의 기계학습(Machine Learning)의 정의
양태, 증거성, 의외성 통사론 기초
강좌 개요 2009년 1학기 컴퓨터의 개념 및 실습.
과목 홈페이지  전산학개론 이메일 숙제를 제출할 경우, 메일 제목은 반드시 ‘[전산학개론]’으로 시작.
REINFORCEMENT LEARNING
제 6 장 데이터 타입 6.1 데이터 타입 및 타입 정보 6.2 타입의 용도 6.3 타입 구성자 6.4 사례 연구
Problems of Finite Difference Method (유한차분법)
이산수학(Discrete Mathematics)
증명 수학적 귀납법 직접 증명법 간접 증명법 재귀법 프로그램 검증.
이산수학(Discrete Mathematics) 수학적 귀납법 (Mathematical Induction)
Mathematics Review for Algorithm
Dynamic Programming.
Internet Computing KUT Youn-Hee Han
제 5장 퍼지이론 (Fuzzy theory) Slide 1 (of 48).
Chapter 2. Finite Automata Exercises
Discrete Math II Howon Kim
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
Mathematics Review for Algorithm
계수와 응용 (Counting and Its Applications)
논문을 위한 통계 논문과 통계의 기초 개념 하성욱 한성대학교 대학원.
이산수학(Discrete Mathematics)
Medical Instrumentation
Chapter 1 Welcome Aboard.
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy)
제 4 장. Regular Language의 특성
Data Mining Final Project
Mathematical Description of Continuous-Time Signals
3.1 증명 전략 (Proof Strategy) 이산수학 (Discrete Mathematics) 2006년 봄학기 문양세
이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy)
Introduction to Programming Language
Discrete Math II Howon Kim
이산수학(Discrete Mathematics)
Dynamic Programming.
이산수학(Discrete Mathematics)  증명 방법 (Methods of Proof)
퍼지 이론 (Fuzzy Theory) 컴퓨터를 인간에 가깝게 하는 일의 어려움 Zadeh의 퍼지 집합
이산수학(Discrete Mathematics)
논리와 명제 기본 개념 논리 연산자와 진리표 논리적 동치 한정 기호.
CEO가 가져야 할 품질 혁신 마인드.
주요 내용 명제 조건 명제와 쌍조건 명제 술어와 한정사 논리적 기호로 문장을 표현. 주요 내용 명제 조건 명제와 쌍조건 명제 술어와 한정사 논리적 기호로 문장을 표현.
이산수학 (Discrete Mathematics)
이산수학(Discrete Mathematics) 비둘기 집 원리 (The Pigeonhole Principle)
이산수학(Discrete Mathematics)
MR 댐퍼의 동특성을 고려한 지진하중을 받는 구조물의 반능동 신경망제어
제12장. Algorithmic Computation의 한계
점화와 응용 (Recurrence and Its Applications)
자연연역과 연역 추론의 법칙들 기계적인 진리함수적 연산 방식을 이용하는 진리표 그리기 방식과 달리, ‘자연연역(natural deduction)’은 타당한 연역적 추론의 법칙들을 활용하여 논증의 타당성 여부를 검증하는 방식이다.
ALL KILL 레이어 변경 요청 [PC] 레이어 삭제.
창 병 모 숙명여대 전산학과 자바 언어를 위한 CFA 창 병 모 숙명여대 전산학과
1. 관계 데이터 모델 (1) 관계 데이터 모델 정의 ① 논리적인 데이터 모델에서 데이터간의 관계를 기본키(primary key) 와 이를 참조하는 외래키(foreign key)로 표현하는 데이터 모델 ② 개체 집합에 대한 속성 관계를 표현하기 위해 개체를 테이블(table)
Definitions (정의) Statistics란?
이산수학(Discrete Mathematics)
The general form of 0-1 programming problem based on DNA computing
이산수학(Discrete Mathematics) 수열과 합 (Sequences and Summations)
(Predicates and Quantifiers)
이산수학(Discrete Mathematics)  술어와 한정기호 (Predicates and Quantifiers)
Python Tutorial 4: Data Structures
[CPA340] Algorithms and Practice Youn-Hee Han
퍼지 이론 (Lecture Note #13) 인공지능 이복주 단국대학교 컴퓨터공학과
Python 기본.
Chapter 7: Deadlocks.
Presentation transcript:

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

Proof Strategy (review “Methods of Proof”) Sequences and Summations Overview Proof Strategy Proof Strategy (review “Methods of Proof”) Sequences and Summations Mathematical Induction Recursive Definitions and Structural Induction Recursive Algorithms

추론 규칙(rules of inference) 용어(Terminology) (1/3) 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. (예: n이 짝수라면 n = 2k라 나타낼 수 있다.) 추론 규칙(rules of inference) 논리적으로 유효한 주장(logically valid deductions)을 사용하여, 가정을 결론으로 이끌어가는 증명의 과정이다. Patterns of logically valid deductions from hypotheses to conclusions.

용어(Terminology) (2/3) 보조정리(lemma) 따름정리(corollary) 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) 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) Proof Strategy 추론 규칙의 의미 주어진 가정(antecedent)이 참(true)일 때, 결론(consequent)가 참이라는 패턴 “x = 3”(= p)이면, “x + 1 = 4”(= q)이다. 상기 예에서 p(가정)가 참이면, q(결론)은 참이 된다. 추론 규칙의 표기 antecedent 1 antecedent 2 … 가정  consequent 결론 “”은 “therefore”를 의미한다.

추론 규칙 (Inference Rules) (2/2) 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) 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) 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.” “If we will go swimming, then it is sunny this afternoon.” “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) 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) 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 (자세한 내용은 노트 05 참조) 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) - skip 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) - skip 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) 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) 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)의 마지막 정리 방정식 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은 두 소수의 합이다. 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 증명)

The Halting Problem (정지 문제) (1/2) - skip 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) - skip 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)는 존재하지 않는다!