;; -*- Lisp -*-

;;;; Natural deduction examples for TRE.

;; Copyright (c) 1988, 1995 Kenneth D. Forbus, Northwestern University and
;; Johan de Kleer, Xerox PARC.
;; Please see legal notice in Building Problem Solvers for conditions of use.

;; Please note: TRE by itself cannot solve many of these problems.  The ability to
;; make assumptions, which FTRE provides via a context mechanism, and the TMS-based
;; TRE's provide in various ways, is needed to fully implement KM*.


(defvar *nd-rules* 
  #+Lucid
  "/u/bps/tre/nd.lisp"
  #+Symbolics
  "Rube:>bps>tre>nd.lisp"
  #+GCLISP
  "c:\\GCLISP2\\BPS\\TRE\\ND.LSP")

(defun restart (title &optional (debugging nil))
  (create-tre title :debugging debugging)
  (load *nd-rules*))

(defun ex1 (&optional (debugging? nil)) 
   ;tests NI, CE, OI, and contradiction detection.
  (restart "Ex 1" debugging?)
  (run-forms '((assert! '(implies p q))
	       (assert! '(not q))
	       (assert! '(show (not p))))))

(defun ex2 (&optional (debugging? nil)) ;tests CI and OE.
  (restart "Ex 2" debugging?)
  (run-forms '((assert! '(or (not P) R))
	       (assert! '(implies R Q))
	       (assert! '(show (implies P Q))))))

(defun ex3 (&optional (debugging? nil)) ;tests AE and AI.
  (restart "Ex 3" debugging?)
  (run-forms '((assert! '(and A B))
	       (assert! '(and B C))
	       (assert! '(show (and A B C))))))

(defun ex4 (&optional (debugging? nil)) ;tests BI and "Star Trek" problem
  (restart "Ex 4" debugging?)
  (run-forms '((assert! 'contradiction)
	       (assert! '(show (iff P Q))))))

(defun ex5 (&optional (debugging? nil)) ;tests indirect proof.
  (restart "Ex 5" debugging?)
  (run-forms '((assert! '(implies (not p) q))
	       (assert! '(not q))
	       (assert! '(show p)))))

;;; Here are some examples from class

(defun ex6 (&optional (debugging? nil))
  (restart "Ex 6" debugging?)
  (run-forms '((assert! '(iff (and R L (not P)) J))
	       (assert! '(implies (not A) (not R)))
	       (assert! '(not A))
	       (assert! '(show (not J))))))

(defun ex7 (&optional (debugging? nil))
  (restart "Ex 7" debugging?)
  (run-forms '((assert! '(implies (and J C) P))
	       (assert! '(iff (and M C) (or P J)))
	       (assert! 'J)
	       (assert! '(show (and P M))))))

(defun ex8 (&optional (debugging? nil))
  (restart "Ex 8" debugging?)  ;; A tough one
  (run-forms
    '((assert! '(show (implies (implies p q)
			       (or (not p) q)))))))

(defun ex9 (&optional (debugging? nil))
  (restart "Ex " debugging?)
  (run-forms '((assert! '(or (and F G) (and G B)))
	       (assert! '(implies F (not G)))
	       (assert! '(show B)))))