(define (make-logic-rules)
  (clear-rules)
  (remember-rules
   '(A0 IF
	(? P)
	(NOT (? P))
	THEN
	(STOP)				; Stops chaining
	SAYING ("Contradiction ~a ~a" (? P) (NOT (? P))))
   ;; And introduction
   '(A1 IF 
	(? P)
	(? Q)
	THEN
	((? P) AND (? Q))
	SAYING ("And introduction from ~a, ~a" 
		(? P) (? Q)))
   ;; And elimination
   '(A2 IF 
	((? P) AND (? Q))
	THEN 
	(? P)
	(? Q)
	SAYING ("And elimination from ~a"
		((? P) AND (? Q))))
   ;; Double Negation
   '(A3 IF
	(? P)
	THEN
	(NOT (NOT (? P)))
	SAYING ("Double negation from ~a"
		(? P)))
   ;; Double negation
   '(A4 IF
	(NOT (NOT (? P)))
	THEN
	(? P)
	SAYING ("Double negation from ~a"
		(NOT (NOT (? P)))))
   ;; Modus Ponens
   '(A5 IF
	((? P) => (? Q))
	(? P)
	THEN
	(? Q)
	SAYING ("Modus Ponens from ~a, ~a" 
		((? P) => (? Q)) (? P)))
   ;; Modus Tollens
   '(A6 IF
	((? P) => (? Q))
	(NOT (? Q))
	THEN
	(NOT (? P))
	SAYING ("Modus Tollens from ~a, ~a" 
		((? P) => (? Q)) (NOT (? Q))))
   ;; De Morgan's
   '(A7 IF
	(NOT ((? P) AND (? Q)))
	THEN
	((NOT (? P)) OR (NOT (? Q)))
	SAYING ("De Morgan's from ~a"
		(NOT ((? P) AND (? Q)))))
   '(A8 IF
	((NOT (? P)) OR (NOT (? Q)))
	THEN
	(NOT ((? P) AND (? Q)))
	SAYING ("De Morgan's from ~a"
		((NOT (? P)) OR (NOT (? Q)))))
   '(A9 IF
	(NOT ((? P) OR (? Q)))
	THEN 
	((NOT (? P)) AND (NOT (? Q)))
	SAYING ("De Morgan's from ~a"
		(NOT ((? P) OR (? Q)))))
   '(A10 IF
	 ((NOT (? P)) AND (NOT (? Q)))
	 THEN 
	 (NOT ((? P) OR (? Q)))
	 SAYING ("De Morgan's from ~a"
		 ((NOT (? P)) AND (NOT (? Q)))))
   ;; Implication Definition
   '(A11 IF
	 ((? P) => (? Q))
	 THEN
	 ((NOT (? P)) OR (? Q))
	 SAYING ("Implication definition from ~a"
		 ((? P) => (? Q))))
   '(A12 IF
	 ((NOT (? P)) OR (? Q))
	 THEN
	 ((? P) => (? Q))
	 SAYING ("Implication definition from ~a"
		 ((NOT (? P)) OR (? Q))))
   ;; Implication introduction
   '(A13 IF
	 (? P)
	 (? Q)
	 THEN
	 ((? Q) => (? P))
	 SAYING ("Implication introduction from ~a, ~a"
		 (? P) (? Q)))
   ;; Implication distribution
   '(A14 IF
	 ((? P) => ((? Q) => (? R)))
	 THEN
	 (((? P) => (? Q)) => ((? P) => (? R)))
	 SAYING ("Implication distribution from ~a" 
		 ((? P) => ((? Q) => (? R)))))
   )
  (format #t "~%Logic rules recorded."))

;; This is proof by contradiction.  We have added to negation of what we 
;; are trying to prove (win you) to the axioms.  So we should be able to
;; reach a contradiction.
(define (make-test)
  (clear-assertions)
  (remember-assertions
   '(Heads => (Win Me))
   '(Tails => (Not (Win You)))
   '((Not Heads) => Tails)
   '((Win You) => (Not (Win Me)))
   '(Win You))
  (format #t "~%Logic test recorded:")
  (display-assertions *assertions*))

(define (logic-run-rules rules-fn)
 (make-logic-rules)
 (rules-fn)
 (chain)
 (display-assertions *assertions*))

(define (logic-run)
  (logic-run-rules make-test))