656/556 2003 1w 09 predicates LPC
Assigned work:
   Do the exercise on the "Algorithm Apply" Handout to
	generate x.y+ (-x).(-y) from x.y and (-x).(-y) and
	check that the result is x<->y.


Predicate Logic= LPC=
	Propositional operations +
	predicates  + quantifiers + terms

Book
	2.1 Need for a richer language
		Jackson handout 

		Common patterns
			for all x( P -> Q)
			for some x ( P and Q)
			for no x(P and Q) = not for some(P and Q).
			for one x(P and Q) 
		Uncommon patterns (be suspicious of these)
			for all x (P and Q)
			for some x ( P->Q)
	2.2 LPC Syntax
		Terms
		WFF
			not and or implies
			for all
			for some
		   priorities
		   free and bound variables
		Substitution   \phi[t/x]
	2.3 Proof Theory
		Natural deduction
			Rules for =  (its algebra!)
			Rules for "for all"
			Rules for "for some"
			   if it is true for t then it is true for something.
			   if any value implies P and there is a value then P.
		Equivalences
	

discounts case study (again)
 abbreviations
    D(d,p,n):= discount on day d for person p is n%.
    T(d):= d is a Tuesday.
    C(p):= p has a club card.
    S(p):= p is a senior.
    10,5,0: terms.
 formulas
	(r1): for all p,d( C(p) /\T(d) -> D(d,p,10)).
	(r2): for all p,d( C(p) /\ - T(d) -> D(d,p,5)).
	(r3): for all p,d( S(p) /\ C(p) -> D(d,p,10)).
	(r4): for all p,d(-C(p) /\  S(p) -> D(d,p,5)).
	(r5): for all p,d( -C(p) /\ - S(p) -> D(d,p,0)).

Expressed in Prolog	
	http://ftp.csci.csusb.edu/dick/cs656/prolog/discounts.plg

Penguin example

Assigned work: Read
	Introduction to Prolog
	Handout on Semantic Tableaux
	Chapter 2, section 2.4

lab
  http://www.csci.csusb.edu/dick/cs656/prolog/lab1.html

Next
  Complete study of chapter 2.
  Concentrate on the Semantics (section 2.4)
  You need to know the results shown in section 2.5
	but not how to prove them in this class.
  http://www.csci.csusb.edu/dick/cs656/class/10.html