Mathematical InductionIncomplete InductionNot So Lucky GuessBasic MetavocabularyOutlineLinear InductionLinear Induction SchemaArithmetic ExamplesArithmetic ProblemClausal FormResolution ProofSlide 12Slide 13Induction and ResolutionLinear Induction MethodEven and OddEven and Odd ProblemBinary AdditionBinary Addition ProblemSlide 20Slide 21Slide 22Intuition for Structural InductionBinary Tree RepresentationSlide 25ReverseReverse ProblemSlide 28Ordered InductionBase CaseGoldbach’s ConjectureSummaryMathematical InductionComputational Logic Lecture 16Michael Genesereth Spring 200401/13/19 2Incomplete InductionDefinitionf(1)=1f(x+1)=f(x)+2*x+1DataConjectureIn this case, the answer is correct. Lucky Guess.1 = 1 = 121+3 = 4 = 221+3+5 = 9 = 321+3+5+7 = 16 = 421+3+5+7+9 = 25 = 52f(x) =x201/13/19 3Not So Lucky GuessData:“Theorem” by Fermat (1601-1665):Fact discovered (mercifully) after his death:Oops.221+1 = 22+1= 5222+1 = 24+1= 17223+1 = 28+1= 257224+1 = 216+1= 65537prime(22x+1)225+1=4,294,967,297=641* 6,700,41701/13/19 4DataBase Case: Prove for n=1f(1)=1=12Inductive Case: Assume true for x; prove for x+1f(x+1)=f(x)+2*x+1f(x+1)=x2+2*x+1f(x+1)=(x+1)2Jules Henri Poincare (1854-1912) credited with invention.Basic Metavocabulary1 = 1 = 121+3 = 4 = 221+3+5 = 9 = 321+3+5+7 = 16 = 4201/13/19 5OutlineLinear Induction Input: successor function on individuals Output: universally quantified conclusionsStructural Induction Input: constructor function for structures Output: universally quantified conclusionsOrdered Induction Input: ordering relation on individuals Output: universally quantified conclusions01/13/19 6Linear InductionLinearly Structured World:In other words, there is a distinguished base element and there is a successor function, which, starting at the base element, enumerates all elements in the universe of discourse.Base element: eSuccessor function: f• → • → •e f(e) f( f(e))01/13/19 7Linear Induction SchemaIf a property holds of the base element and if it holds of a successor whenever it holds of an element, we would like to assert that it holds of all elements in the universe of discourse.[e] x.([x][f(x)]) x.[x]Base case: [e]Inductive case: x.([x][f(x)]) Inductive antecedent: [x] Inductive consequent: [f(x)]) Conclusion: x.[x]Analogy to students in class passing on messages01/13/19 8Object constant: 0Unary function constant: s (+1)Binary relation constants: even, odd, integerInduction Schema:[0] x.([x][s(x)]) x.[x]Instance of Induction Schema:integer(0)x.(integer(x) integer(s(x)))x.integer(x)Instance of Induction Schema: (even(0)odd(0)) x.(even(x)odd(x)even(s(x))odd(s(x))) x.(even(x)odd(x))Arithmetic Examples01/13/19 9Object constant: 0Unary function constant: s (+1)Binary relation constants: integerAxiomsinteger(0)x.(integer(x) integer(s(x)))Goal:x.integer(x)Induction Schema:integer(0)x.(integer(x) integer(s(x)))x.integer(x)Arithmetic Problem01/13/19 10Clausal Form integer(0)x.(integer(x) integer(s(x)))x.integer(x)I: (integer(0)x.(integer(x)integer(s(x))))x.integer(x)N: integer(0)x.(integer(x)integer(s(x)))x.integer(x) integer(0)x.(integer(x) integer(s(x)))x.integer(x) integer(0)x.(integer(x)integer(s(x)))x.integer(x) integer(0)x.(integer(x)integer(s(x)))x.integer(x)S:E: integer(0)(integer(a)integer(s(a)))x.integer(x)A: integer(0)(integer(a)integer(s(a)))integer(x)D: integer(0)integer(a)integer(x) integer(0)integer(s(a))integer(x)O: {integer(0), integer(a), integer(x)} {integer(0), integer(s(a)), integer(x)}01/13/19 11Resolution Proof1. {integer(0)} Premise2. {¬integer(x),integer(s(x))} Premise3. {¬integer(0),integer(a),integer(x)} Induction4. {¬integer(0),¬integer(s(a)),integer(x)} Induction5. {¬integer(c)} Goal6. {integer(a),integer(x)} 1,37. {¬integer(s(a)),integer(x)} 1,48. {integer(s(a)),integer(x)} 2,69. {integer(x)} 7,810. {} 5,901/13/19 12Object constant: 0Unary function constant: sBinary relation constants: even, oddAxiomseven(0)x.(even(x) odd(s(x)))x.(odd(x) even(s(x)))Goal:x.(even(x) odd(x))Induction Schema:(even(0)odd(0)) x.(even(x)odd(x)even(s(x))odd(s(x))) x.(even(x)odd(x))Arithmetic Problem01/13/19 13Clausal Form(even(0)odd(0)) x.(even(x)odd(x)even(s(x))odd(s(x))) x.(even(x)odd(x)) {even(0), even(a), odd(a), even(x), odd(x)} {odd(0), even(a), odd(a), even(x), odd(x)} {even(0), even(s(a)), even(x), odd(x)} {even(0), odd(s(a)), even(x), odd(x)} {odd(0), even(s(a)), even(x), odd(x)} {odd(0), odd(s(a)), even(x), odd(x)}01/13/19 14Induction and ResolutionUnderstandability Okay for computers Terrible for humansGenerality: Induction is an axiom schema. Resolution works on sentences.01/13/19 15Linear Induction MethodUsing the Induction schema to prove a universally quantified formula.(1) Base Case. Prove the base case.(2) Inductive Case. Assume ground version of induction antecedent (induction hypothesis) and prove corresponding version of induction consequent.If successful, the universally quantified conclusion holds. Why? Deduction Theorem.01/13/19 16Even and OddAxiomseven(0)even(x) odd(s(x))odd(x) even(s(x))Desired Conclusion:x.(even(x)odd(x))Induction Axiom:(even(0)odd(0)) x.(even(x)odd(x)even(s(x))odd(s(x))) x.(even(x)odd(x))01/13/19 17Even and Odd Problem1. {even(0)} Induction2. {¬even(x),odd(s(x))} Premise3. {¬odd(x),even(s(x))} Axiom4. {even(a),odd(a)} Induction5. {¬even(s(a))} Goal6. {¬odd(s(a))} Goal7. {¬odd(a)} 2,68. {¬even(a)} 3,59. {even(a)} 4,710. {} 8,901/13/19 18Binary AdditionObject constant: 0Unary function constant: sBinary function constant: +Chain Axioms:s(x)=s(y) x=yAddition Axioms:x+0=xx+s(y)=s(x+y)s(x)+y=s(x+y)01/13/19 19Binary Addition ProblemQuestion:x.0+x=xAxioms:s(x)=s(y) x=yx+0=xx+s(y)=s(x+y)s(x)+y=s(x+y)Goal:x.0+x=xInduction Axiom:0+0=0 x.(0+x=x 0+s(x)=s(x)) x.0+x=x01/13/19 20Binary Addition Problem1. {¬s(x) =s(y),x=y} Axiom2. {x+0=x} Axiom3. {x+s(y) =s(x+y)} Axiom4. {s(x)+y=s(x+y)} Axiom5. {0+a=a} Induction6.
View Full Document
Unlocking...