[Index] || [Contents] || [Grades] Mon Mar 3 14:43:02 PST 2003

656/556 2003 1w 10 Predicate Calculus semantics LPC Assigned work: Reading! Handout: Semantic tableaux for LPC Section 2.4 semantics Models of a set of formulas Worlds in which the formulas are all true. A world has a set of objects, maps and sets. Small worlds can be shown using tables. Semantic Models can disprove formulas and sequents To show P|-Q, start a tableau with P, not Q. Semantic tableaux (almost always) generate counter-examples. At the worst they wander off missing a good branch. Generates a model OR closes off all possibilities. They rely on your ingenuity to substitute the best terms into "for all" formula. (example. it took 5 goes over 3 hours for Ex2.7#7d) Section 2.5 results Limits on logic! There is no program to prove/disprove all formulae. Limitted help from tools. But we do have PVS. Good news: The predicate calculus is the machine code of thinking! We usually reason intuitively using higher level concepts: numbers, sets, functions, algebra, ..., maths We refine our thinking down to the predicate level when we get doubts about our higher level thinking. Further, the typical project has lots of trivial stuff and very little hard to do stuff. Further, we have special logics that are good in real projects and have algorithms and TOOLS. (CTL next for example). more prolog The disproof of the penguin! http://www.csci.csusb.edu/dick/cs656/prolog/penguin.plg Assigned work: Prepare a 2sided "cheat sheet" 11><8.5 for the midterm. Hand in with midterm for 3pts. lab http://www.csci.csusb.edu/dick/cs656/prolog/lab2.html next Midterm on Logic: PC, OBBDs, LPC http://www.csci.csusb.edu/dick/cs656/class/11.html