Assignment due Monday, 1/31/05. You can do this assignment either in your three-member groups or, if you are unable to meet, you can do it individually. I recommend the former if possible.

In the file Rules_3-30.lisp, the backwards and forwards reasons were hand-coded rather than using the reason-macros, in the mistaken belief that this would be faster. To illustrate that it is not, your assignment is to recode some of these reasons using the reason-macros, and then compare the run time of OSCAR on problem 37. So:


First run (test 37) and record the run-time.

Next, creat a file using the following template, filling in definitions for bicondit-intro, disj-cond, cond-antecedent-simp, exportation, and simp:


; addition
; from P and Q, infer (P & Q)
(def-backwards-reason ADDITION
:conclusions "(P & Q)"
:backwards-premises "P" "Q"
:variables P Q)

;Backwards reason: from (P -> Q) and (Q -> P), infer (P <-> Q)

;Backwards reason: from (~P -> Q) infer (P v Q)

;modus ponens
;Forwards reason: from P and (P -> Q) infer Q

(def-forwards-reason MODUS-PONENS
:conclusions "Q"
"(P -> Q)"
:variables P Q)

;Forwards reason: from ((P -> Q) -> R) infer both (~P -> R) and (Q -> R)


;Forwards reason: from ((P & Q) -> R) infer (P -> (Q -> R))

;Forwards reason: from (P & Q) infer both P and Q.


(setf *forwards-logical-reasons*
neg-ug neg-eg EI UI
E-removal A-removal
simp neg-elim neg-disj neg-condit neg-bicondit-simp
DM bicondit-simp modus-ponens
cond-simp1 cond-simp2

(setf *backwards-logical-reasons*
(list adjunction neg-intro i-neg-disj i-neg-condit i-neg-bicondit
bicondit-intro disj-cond i-DM conditionalization
i-neg-ug i-neg-eg EG UG


Note that the formulas must be quoted, and note the spaces and parentheses in the formulas.

Finally, load this file, and then run (test 37) again and compare the run time.