#| -*-Scheme-*-

$Id: tms-examples.scm 3875 2007-08-24 18:24:03Z cph $

Copyright (C) 2006,2007 Massachusetts Institute of Technology

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or (at
your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301,
USA.

|#

;;;; TMS: examples

(declare (usual-integrations))

(define tms
  (tms:make "n"
	    (lambda (node justification)
	      (tms:write-comment
	       `(,(if justification 'supported 'unsupported)
		 ,(tms:node-name node))))))

(define a (tms:make-node tms 'A))
(define b (tms:make-node tms 'B))
(define c (tms:make-node tms 'C))
(define d (tms:make-node tms 'D))
(define e (tms:make-node tms 'E))
(define f (tms:make-node tms 'F))
(define g (tms:make-node tms 'G))
(define h (tms:make-node tms 'H))
(define i (tms:make-node tms 'I))

(tms:justify-node e 'MP `(and ,a ,b))
(tms:justify-node e 'X c)
(tms:justify-node g 'Y e)
(tms:justify-node h 'Z `(and ,e ,f))
(tms:justify-node f 'W `(and ,c ,d))

(tms:assume-node c)
;(supported (n78 = c))
;(supported (n79 = e))
;(supported (n80 = g))
;Unspecified return value

(tms:node-supported? c)
;Value: #t

(tms:node-supported? e)
;Value: #t

(tms:why? g)
;((n80 = g) <== (y (n79 = e)))
;((n79 = e) <== (x (n78 = c)))
;((n78 = c) premise)
;Unspecified return value

(tms:retract-node c)
;(unsupported (n78 = c))
;(unsupported (n80 = g))
;(unsupported (n79 = e))
;Unspecified return value

(tms:assume-node a)
;(supported (n81 = a))
;Unspecified return value

(tms:assume-node b)
;(supported (n82 = b))
;(supported (n79 = e))
;(supported (n80 = g))
;Unspecified return value

(tms:assume-node c)
;(supported (n78 = c))
;Unspecified return value

(tms:assume-node d)
;(supported (n83 = d))
;(supported (n84 = f))
;(supported (n85 = h))
;Unspecified return value

(tms:retract-node a)
;(unsupported (n81 = a))
;Unspecified return value

(tms:why? h)
;((n85 = h) <== (z (n79 = e) (n84 = f)))
;((n79 = e) <== (x (n78 = c)))
;((n84 = f) <== (w (n78 = c) (n83 = d)))
;((n78 = c) premise)
;((n83 = d) premise)
;Unspecified return value

(tms:retract-node d)
;(unsupported (n83 = d))
;(unsupported (n85 = h))
;(unsupported (n84 = f))
;Unspecified return value

(tms:justify-node i 'U f)
;Unspecified return value

(tms:justify-node i 'Q g)
;(supported (n86 = i))
;Unspecified return value

(tms:justify-node d 'R i)
;(supported (n83 = d))
;(supported (n84 = f))
;(supported (n85 = h))
;Unspecified return value

(tms:why? h)
;((n85 = h) <== (z (n79 = e) (n84 = f)))
;((n79 = e) <== (x (n78 = c)))
;((n84 = f) <== (w (n78 = c) (n83 = d)))
;((n78 = c) premise)
;((n83 = d) <== (r (n86 = i)))
;((n86 = i) <== (q (n80 = g)))
;((n80 = g) <== (y (n79 = e)))
;Unspecified return value

(tms:retract-node c)
;(unsupported (n78 = c))
;(unsupported (n85 = h))
;(unsupported (n84 = f))
;(unsupported (n83 = d))
;(unsupported (n86 = i))
;(unsupported (n80 = g))
;(unsupported (n79 = e))
;Unspecified return value

(tms:assume-node a)
;(supported (n81 = a))
;(supported (n79 = e))
;(supported (n80 = g))
;(supported (n86 = i))
;(supported (n83 = d))
;Unspecified return value

(tms:why? d)
;((n83 = d) <== (r (n86 = i)))
;((n86 = i) <== (q (n80 = g)))
;((n80 = g) <== (y (n79 = e)))
;((n79 = e) <== (mp (n81 = a) (n82 = b)))
;((n81 = a) premise)
;((n82 = b) premise)
;Unspecified return value

(tms:assume-node c)
;(supported (n78 = c))
;(supported (n84 = f))
;(supported (n85 = h))
;Unspecified return value

(tms:retract-node c)
;(unsupported (n78 = c))
;(unsupported (n84 = f))
;(unsupported (n85 = h))
;Unspecified return value