;;; -*- Mode: LISP; Syntax: Common-lisp; -*-

;;;; Indirect proof mechanism for LTRE
;;; Last Edited 1/29/93, by KDF

;;; Copyright (c) 1986-1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

(proclaim '(special *ltre*))

(defun try-indirect-proof (fact &optional (*ltre* *ltre*))
  (unless (known? fact)
    (with-contradiction-handler (ltre-ltms *ltre*)
      #'(lambda (contradictions ltms &aux assumptions)
	  (setq assumptions
		(assumptions-of-clause
		 (car contradictions)))
	  (let ((the-node
		 (find (datum-tms-node (referent fact t))
		       assumptions)))
	    (when the-node
	      (let ((status (tms-node-label the-node)))
		(retract-assumption the-node)
		(add-nogood the-node status
			    assumptions)))))
      ;; Assume the negation
       (assuming `((:not ,fact)) *ltre*
		 (run-rules)))
   (known? fact)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Example of indirect proof

(defun indirect-proof-example ()
  (in-ltre (create-ltre "Indirect Proof Example"))
  (assert! '(:or p q) 'user)
  (assert! '(:implies p r) 'user)
  (assert! '(:implies q r) 'user)
  (known? 'r)
  (try-indirect-proof 'r)
  (known? 'r))