CS 1502 Formal Methods in Computer Science

CS 1502 Formal Methods in Computer Science Lecture Notes 11 1 Example Infer A C from A B and B C. A B BC AC

This argument is known as the Transitivity of the Biconditional. 2 Using Resolution A B is (A B) (B A) {A, B} {B,A} B C is (B C) (C B) {B,

C} {C, B} (A C) is (A C ) (A C) {A, C}

{A, C} Resolution Proof: In Lecture 3 Using Fitch 4

Law of Excluded Middle P P A Tautology 5 Exercise 6.33 (in the pdf solution) 6

Exercise 6.33 (shorter version) 7 Using DeMorgans, with Taut Con doing the work for you 8 Using DeMorgans, but

we do the work(turns out to be redundant) 9 Law of Excluded Middle P P Use with V-Elim in Proofs! To introduce it: Use Taut Con, if the rules allow Otherwise, insert proof 6.33

10 Exercise 8.53 (on LPL Web site) Note: Fitch lines after line 4 And 11 were

eaten by adobe. They should be there. 11 Example

Prove this argument is valid from no premises. (P Q) (P Q) Logical truth 12 Example 13

Prove this argument Horned(unicorn) (Elusive(unicorn) Dangerous(unicorn)) (Elusive(unicorn) Mythical(unicorn)) Rare(unicorn) Mammal(unicorn) Rare(unicorn) Horned(unicorn) Mammal(unicorn) Proof is on the next slide; Go through it for practice on your own. 14 1. Horned(unicorn) (Elusive(unicorn) Dangerous(unicorn) 2. (Elusive(unicorn) Mythical(unicorn)) Rare(unicorn)

3. Mammal(unicorn) Rare(unicorn) 4. Horned(unicorn) 5. Elusive(unicorn) Dangerous(unicorn) 6. Elusive(unicorn) 7. Elusive(unicorn) Mythical(unicorn) 8. Rare(unicorn) 9. Mammal(unicorn) Elim 1,4 Elim 5 Intro

Elim 2,7 10. Rare(unicorn) 11. Elim 3,9 12. Mammal(unicorn) Intro 9-11

13. Horned(unicorn) Mammal(unicorn) Intro 8,10 Intro 4-12 15 Informal Proof Example Prove there exists irrational numbers b and c such that bc is rational.

Proof: Consider = 22. This number is either rational or irrational. If is rational we are finished since b = c = 2 . Assume is irrational. Consider 2 = 2. Again we are finished since b = and c = 2. 16 English Translation EGs PQ

If P then Q (If you are human then you are a mammal) P implies Q (Being a human implies being a mammal) If P, Q (If you are human, you are a mammal) P only if Q (Youll live a long time only if you eat veggies) P is sufficient for Q (Knowing youre living a long time is sufficient to know you eat veggies) Q is necessary for P (Eating veggies is necessary to live a long time) Q if P (You are a mammal if you are human)

17 P Q Home(max) Library(claire) Large(b) Cube(b) If not P then Q If Max is not home, then Claire is at the library If b is not large, then it is a cube Unless P, Q Unless Max is at home, Claire is at the library

Unless b is large, b is a cube Q, unless P Claire is at the library unless Max is home B is a cube unless b is large Why not for last two? (section 7.3 and lecture) 18 Lecture: look at related questions on Assignment 3, in 7.12 and 7.15

19

Recently Viewed Presentations

  • Herbie  An Introduction to WiP Limits Speaker: John

    Herbie An Introduction to WiP Limits Speaker: John

    How might you limit work in progress? Henry Ford, observed excess WiP and reduced space. TaiichiOhno, used cards to limit items worked on. Eli Goldratt, observed that WiPis constrained only by your bottleneck . Balance production line, all workstations to...
  • Unit 4: Writing for the News 4-4 Working on our LEDEs

    Unit 4: Writing for the News 4-4 Working on our LEDEs

    "Surprising her with her favorite gourmet pizza was the best part!" excitedly reported Mrs. Hillary Bernard after she and her husband, Travis Bernard, enjoyed a birthday dinner at their friends' home in Charlotte, NC the evening of Saturday, March 4th,...
  • Free & Reduced

    Free & Reduced

    FOOD & NUTRITION ANNUAL REPORT School Year 2004-05 Program Accomplishments Baked desserts removed from lunch menu Increased quantity and variety of fresh fruits & vegetables on daily lunch menus Introduced salad bars at Robbins Elementary& DeLong Middle School; piloted at...
  • Background Number of pupils on Roll Number of FSM pupils ...

    Background Number of pupils on Roll Number of FSM pupils ...

    New School(YsgolHarriTudur/Henry Tudor School). Enclosed siteChange in EthosRestricted entrance and exit points. Enclosed school site with a much improved environment. There is a change in ethos - The school has a new recently appointed head mistress with a new vision.
  • School Council Bylaws - hwdsb.on.ca

    School Council Bylaws - hwdsb.on.ca

    School Councils may also wish to develop bylaws related to the following: A School Council Code of Ethics and/or Council Norms and Values. General expectations regarding meetings (e.g., attendance, promptness)
  • De OMT a UML

    De OMT a UML

    Standish. Group. A cada mil linhas de código são encontrados entre 20 e 30 bugs (2% a 3%) - Sustainable. Computer Consortium . Inspeção de software reduz entre 60% e 90% dos defeitos em software e 25% de seus custos...
  • 예수님의 신성 인식 - All for Jesus!

    예수님의 신성 인식 - All for Jesus!

    예수안에 신성과 인성이 본질적으로 함께 한다는 소위 "후포스테틱 유니온" 교리가 최초로 반포된 것은 기원후 451년 챨스돈 공회에서였다. 예수 그리스도라는 하나의 본질 (Hupostasis) 혹은 인격 (Person)안에신성과 인성이 어떻게 함께 했나를 규정한 것이다.
  • Doctrine of Sin - Biblical Studies

    Doctrine of Sin - Biblical Studies

    Nature of Sin. Terms used for "sin" in the Bible. Old Testament: ... Root word is a picture of Archery. Missing the mark. Sin falls short of God's glory . ... Between Man & God. We are by nature in...