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