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)

;|bicondit-intro

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

;disj-cond

;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"

:forwards-premises

"P"

"(P -> Q)"

:variables P Q)

;cond-antecedent-simp

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

;exportation

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

;simp

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

(setf *forwards-logical-reasons*

(reverse

(list

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

modus-tollens1

conditional-modus-tollens

exportation

disj-antecedent-simp

cond-antecedent-simp

disj-simp

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

disj-cond-2

contra-conditionalization

))

===============================================================================================

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.