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 CNOTE: 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.
Pwe 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 returnedWhen 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 firstname.lastname@example.org.