>> [CS656/556 Course Materials]
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).
The disproof of the penguin!
Assigned work: Prepare a 2sided "cheat sheet" 11><8.5 for
the midterm. Hand in with midterm for 3pts.
Midterm on Logic: PC, OBBDs, LPC