[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/09
[Index] || [Contents] || [Grades] Mon Mar 3 14:43:01 PST 2003
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

	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
			not and or implies
			for all
			for some
		   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.

discounts case study (again)
    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.
	(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	

Penguin example

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


  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.