11/2/09 11:50am. Resolution Inference rule

Using the original resolution inference rule 

	(A OR B) AND ( NOT A OR C)
we derive the sentence 
	B OR C
NOTE: This does not mean the two truth tables are identical when we assign values to A, B, and C. Its is similar to the inference rule that if we know a sentence P, then we know P OR Q, i.e. 
	P
we derive the sentence 
	P OR Q

i.e If P is "It is raining" and Q is "Fred is a student", then if
we know P (It is raining), we can definitively say P OR Q, (it is
raining OR fred is a student). The inference rules only help us prove
a goal, and are not meant to derive identical truth tables about
individual sentence.



Resolution is an example of entailment.
Sentence alpha entails sentence beta if beta is true in all worlds
where alpha is true.
I.e.

Vars  |         alpha              | beta   |  alpha -> beta
A B C | (A OR B) AND ( NOT A OR C) | B OR C |
T T T | T                          | T      | T
T T F | F                          | T      | T
T F T | T                          | T      | T
T F F | F                          | F      | T
F T T | T                          | T      | T
F T F | T                          | T      | T
F F T | F                          | T      | T
F F F | F                          | F      | T




Resolution can always be used to either confirm or refute
a sentence, but it cannot be used to enumerate sentences. 



 FIRST DAY ANNOUNCEMENT 




 No discussion section this Friday (9/25) and Friday (10/2)







The textbook assignment (problems 1.11 and 1.12) is postponed for now - the
due date will be announced later.





HW1 is due online next Friday, October 9, at 11:59 pm. Start early! Keep in
mind that this upcoming weekend will be the only one you will have before the
HW1 deadline.





Also, the TA's office hours next week will be Monday 11:30 am-12:30 pm
and Thursday 9:30-10:30 am in BH 4428, or by appointment. Please post
questions regarding the homework on the CourseWeb forum or drop by her
office hours next week.  




 Comments in Lisp 


The semicolon ';' is the Lisp comment character. 
Comments are to the right of the semicolon, i.e.

	(defun square (x)  ; x is the parameter to square
		(* x x))   ; the value of x*x is returned


When writing lisp code, comment your functions liberally.



Use the "defun" keyword for defining functions, i.e.

         (defun square (x) (* x x ))


If you must create global variable (please try to avoid using them),
use the "setq" macro instead of the "define" keyword when setting global
variables, i.e.

         (setq pi 3.14159)


		

 Increasing the size of the LISP stack to prevent stack overflow


When coding some of your LISP projects, you  may run into a problem that 
gcl throws a stack overflow error after too many function invocations.
The stack size can be increased by typing

	(setq si::*multiply-stacks* 4)

which increases the stack size by a factor of 4. If this is not
sufficient, you can use a larger increase factor than 4.


 Turning in Projects


Please read this page on how to
submit, what to submit, and what to turn in in class.


Here are some examples 
of trees and how they're represented in lisp.


   Regarding Submit and turning in projects: 
If you submit a file, you remain the owner of
that file until the end of the day. So if you submit hw1.lsp on a
Wednesday, you can resubmit as many times as you want the same filename
through that Wednesday.  However, the next day after you submit, you
lose ownership of the file, and you can only resubmit by using a
different name. So your best bet is to submit the files when you have
completed the homework.



Please send any comments, questions, suggestions, or spelling
corrections to 
rosen@cs.ucla.edu.