;                                                                                OSCAR_3.31

#|This is the  agent-architecture OSCAR, described in chapter nine of COGNITIVE
CARPENTRY.|#

#| This is based upon OSCAR_3.30.  It converts variables between conclusions and interests, and
fixes some errors in the use of the match in discharging reductios. |#

;(when (null (find-package "OSCAR")) (make-package "OSCAR"))
;
;(in-package "OSCAR")

;; 1/30/05

(setf *version* "OSCAR_3.31")

(princ "Loading ") (princ *version*) (terpri)

(proclaim
  '(special *act-executors* *altered-nodes* *answered-discount*
 *auxiliary-backwards-rules* *auxiliary-forwards-rules*
 *auxiliary-forwards-rules* *backwards-logical-reasons* *backwards-reasons* *backwards-rules*
 *backwards-substantive-reasons* *base-interest* *base-priority* *blocked-conclusions*
 *cancelled-c-lists* *comparison-log* *concluded-interest-priority* *d-trace*
 *dependent-interests* *dependent-nodes* *desires* *direct-reductio-interests*
 *display-inference-queue* *display?* *environmental-input* *executable-operations*
 *forwards-logical-reasons* *forwards-reasons* *forwards-rules* *forwards-substantive-reasons*
 *independent-reductio-suppositions* *inference-graph* *inference-number* *inference-number*
 *inference-queue* *inherited-non-reductio-suppositions* *interest-links* *interest-map*
 *interest-number* *interest-record* *interest-scheme-number* *interest-schemes* *interests*
 *link-number* *log-on* *non-reductio-supposition-nodes* *optative-dispositions* *pause* *percepts*
 *permanent-ultimate-epistemic-interests* *premises* *priority-interests* *prob-compiler-loaded*
 *problem-number* *problems* *problems-loaded* *processed-conclusions* *processed-desires*
 *q&i-modules* *query-number* *queue-number* *reasoning-log* *reductio-discount*
 *reductio-interest* *reductio-supposition-nodes* *skolem-free-suppositions* *skolem-multiplier*
 *start-trace* *support-link-number* *support-links* *test-log* *time-limit* *tools-loaded*
 *trees-loaded* *ultimate-epistemic-interests* *unused-suppositions* *proofs?*
 *use-logic* *use-reductio* *version* ei adjunction is-desire is-inference is-percept oscar-pathname reductio
  *deleted-arguments* *relevant-nodes* *open-position-for-assignment-tree-window*
 *flash-affected-nodes* *flash-defeatees* *flash-defeaters* *flash-ancestors*
 *flash-consequences* *flash-support-link-bases* *flash-support-links* *deductive-only*
 *flash-relevant-nodes* *graph-ancestors* *graph-relevant-nodes* *menu-dialog*
 *message* *start-display* *cycle* *assignment-tree-window* *assignment-tree-subview*
 *monitor-assignment-tree* *assignment-tree-window-size* *assignment-tree-dialog*
 *graphics-initialized* *graphics-on* *graph-log* *graphics-pause* *nodes-displayed* 
 *og-nodes* *og* *graph-interests* *speak* *d-node-number* *discrimination-net*
 *top-d-node* *operators* *quantifier-number* *conditional-node* *disjunction-node*
 *undercutter-node* *conjunctive-undercutter-node* *ip-number* *is-number* *display-box*
 *quantifier-discount* *package-name* *display-button* *trace-button* *constructed-plans*
  *constructed-goals* *constructed-desires* *plan-number* *goal-number*
 *fixed-ultimate-epistemic-interests* *temporal-decay* *temporal-projection* *causal-implication*
 *new-links* *used-nodes* *used-interests* *unprocessed-nodes* *unprocessed-interests*
 *interests-used-in-proof* *temporal-decay-minimum* *instantiated-premise-number*
 *strictly-relevant-nodes* *not-strictly-relevant-nodes* ug))

(defvar *package-name* (package-name *package*))

(defvar *temporal-projection* nil)
(defvar *causal-implication* nil)
(defvar *temporal-decay* .9999)
(defvar *temporal-decay-minimum* (/ (log .5) (log *temporal-decay*)))
(defvar *pause* nil)
(defvar *time-limit* 5)
(defvar *syntax-loaded* nil)
(defvar *prob-compiler-loaded* nil)
(defvar *problems-loaded* nil)
(defvar *tools-loaded* nil)
(defvar *premises* nil)
(defvar *ultimate-epistemic-interests* nil)
(defvar *permanent-ultimate-epistemic-interests* nil)
(defvar *fixed-ultimate-epistemic-interests* nil)
(defvar *forwards-rules* nil)
(defvar *backwards-rules* nil)
(defvar *auxiliary-forwards-rules* nil)
(defvar *auxiliary-backwards-rules* nil)
(defvar *optative-dispositions* nil)
(defvar *doxastic-optative-dispositions* nil)
(defvar *trees-loaded* nil)
(defvar *display-inference-queue* nil)
(defvar *display?* nil)
(defvar *trace* nil)
(defvar *d-trace* nil)
(defvar *start-trace* nil)
(defvar *start-display* nil)
(defvar *proofs?* nil)
(defvar *use-logic* t)
(defvar *use-reductio* t)
(defvar *log-on* nil)
(defvar *priority-interests* nil)
(defvar *blocked-conclusions* nil)
(defvar *answered-discount* .5)
(defvar *base-priority* .1)
(defvar *reductio-interest* .23)
(defvar *reductio-discount* .23)
(defvar *quantifier-discount* .95)
(defvar *EI-adjustment* 2.5)
(defvar *skolem-multiplier* 10)
(defvar *concluded-interest-priority* .001)
(defvar *forwards-substantive-reasons* nil)
(defvar *backwards-substantive-reasons* nil)
(defvar *environmental-input* nil)
(defvar *executable-operations* nil)
(defvar *assignment-tree-dialog* nil)
(defvar *assignment-tree-subview* nil)
(defvar *monitor-assignment-tree* nil)
(defvar *deductive-only* nil)
(defvar *affected-nodes* nil)
(defvar *graphics-on* nil)
(defvar *graph-log* nil)
(defvar *graphics-pause* nil)
(defvar *graph-interests* nil)

(when (not (boundp 'oscar-pathname)) (setf oscar-pathname "G5 backup:Documents:OSCAR:OSCAR FOLDER:"))

(when (null *tools-loaded*)
     (load (concatenate 'string oscar-pathname "Oscar-tools"))
     (setf *tools-loaded* t))

(when (null *syntax-loaded*)
     (load (concatenate 'string oscar-pathname "Syntax_3"))
     (setf *syntax-loaded* t))

(if (not (fboundp 'gc)) (defun gc () t))

;========================== OSCAR =========================

;---------------------------------  support-linkS ----------------------------------

(defstruct (support-link (:print-function print-support-link)
                                           (:conc-name nil))
    (support-link-number 0)
    (support-link-target nil)   ;; the node supported by the link
    (support-link-basis nil)   ;; a list of inference-nodes
    (support-link-rule nil)  ;; a substantive reason or a string describing an inference rule
    (defeasible? nil)  ;; t if the inference is a defeasible one
    (support-link-defeaters nil)
    (defeating-assignment-trees nil)
    (support-link-discount-factor 1.0)  ;; This is the discount-factor provided by the link-rule.
    (support-link-nearest-defeasible-ancestors nil)
    (support-link-reason-strength 1.0)  ;; the strength of the reason
    (support-link-strength nil)  ;; min of reason-strength and undefeated-degrees-of-support for basis
    (support-link-binding nil)
    (support-link-conclusive-defeat-status nil)
    (temporal-link nil)
    (generating-interest-link nil)
    (support-link-clues nil))

(defun print-support-link (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "support-link #" stream)
    (princ (support-link-number x) stream) (princ " for node " stream)
    (princ (inference-number (support-link-target x)) stream)
    (princ ">" stream))

#| This finds the support-link with support-link-number n. |#
(defunction support-link (n)
    (find-if #'(lambda (L) (equal (support-link-number L) n))
                 *support-links*))

; -------------------------------------- INFERENCE-NODES -------------------------------------- 

(defstruct (inference-node (:print-function print-inference-node)
                                                     (:conc-name nil))
    (inference-number 0)
    (node-sequent nil)
    (node-formula nil)
    (node-supposition nil)
    (node-kind nil)   ;;:percept, :desire, or :inference
    (support-links nil)
    (node-justification nil)  ;; a keyword if the node is given or a supposition
    (consequent-links nil)
    (old-undefeated-degree-of-support nil) ;; the degree prior to the last computation of defeat statuses
    (reductio-ancestors nil)
    (non-reductio-supposition nil)
    (maximal-degree-of-support 0)  ;; maximal strength of support-links
    (node-defeatees nil)
    (undefeated-degree-of-support nil)
    (node-ancestors nil)
    (nearest-defeasible-ancestors nil)
    (answered-queries nil)
    (deductive-only nil)   ;; If conclusion is for deductive purposes only, this is t.
    (generated-interests nil)
    (generating-interests nil);; interest generating sup
    (cancelled-node nil)
    (discounted-node-strength nil)
    (processed? nil)  ;;  T if node has been processed.
    (node-variables nil)
    (discharged-interests nil)  ;; triples (interest unifier unifiers) where unifiers is produced by
                                                     ;; appropriately-related-suppositions.  unifier and unifiers are
                                                     ;; left nil in cases where they will not be used.
    (node-supposition-variables nil)
    (interests-discharged? nil)   ;; records whether interests have been discharged
    (reductios-discharged (not *use-reductio*))  ;; records whether reductio-interests have been discharged
    (readopted-supposition 0)  ;; number of times the node has been readopted as a supposition
    (node-discount-factor 1.0)  ;; This is the discount-factor provided by the node-rule.
                                                ;;  it's only use is in ei.
    (node-c-list nil)
    (node-queue-node nil)
    (enabling-interests nil)  ;; if the node is obtained by discharging inference-links, this is the
                                                   ;; list of resultant-interests of the links.
    (motivating-nodes nil)  ;; nodes motivating the inference, not included in the basis.
    (generated-direct-reductio-interests nil)
    (generated-defeat-interests nil)
    (generating-defeat-interests nil)  ;; interest in defeaters discharged by this node
    (temporal-node nil)  ;; nil or the cycle on which the node was constructed
   (background-knowledge nil)
    (non-reductio-supposition? nil)
    (anchoring-interests nil)
    )

(defun print-inference-node (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Node " stream)
    (princ (inference-number x) stream) (princ ">" stream))

(defunction nf (n) 
    (when (numberp n) (setf n (node n)))
    (prinp (node-formula n))
    (node-formula n))

(defunction udos (n) (undefeated-degree-of-support n))

(defunction mdos (n) (maximal-degree-of-support n))

(defunction adjust-for-time (strength node)
    (let ((delta (- *cycle* (temporal-node node))))
      (cond ((>= delta *temporal-decay-minimum*) 0.0)
                ((zerop strength) 0.0)
                (t (- (* (+ strength 1) (expt *temporal-decay* delta)) 1)))))

;(defunction adjust-for-time (strength node)
;    (let* ((t0 (temporal-node node))
;              (decay (expt *temporal-decay* (- *cycle* t0))))
;      (if (< decay strength) decay strength)))

(defunction adjust-for-decay (strength decay)
    (if (or (zerop strength) (< decay .5)) 0.0 (- (* (+ strength 1) decay) 1)))

(defunction compute-maximal-degree-of-support (node)
    (cond
      (*deductive-only* 1.0)
      ((temporal-node node)
        (adjust-for-time (maximal-degree-of-support node) node))
      (t (maximal-degree-of-support node))))

(defunction compute-undefeated-degree-of-support (node)
    (cond
      (*deductive-only* 1.0)
      ((temporal-node node)
        (adjust-for-time (undefeated-degree-of-support node) node))
      (t (undefeated-degree-of-support node))))

(defunction compute-old-undefeated-degree-of-support (node)
    (if (and (temporal-node node) (old-undefeated-degree-of-support node))
      (adjust-for-time (old-undefeated-degree-of-support node) node)
      (old-undefeated-degree-of-support node)))

(defunction compute-discounted-node-strength (node)
    (if (temporal-node node)
      (adjust-for-time (discounted-node-strength node) node)
      (discounted-node-strength node)))

(defunction deductive-node (n)
   (and (not (background-knowledge n))
            (member nil (nearest-defeasible-ancestors n))))

(defunction node-consequences (n)
    (mapcar #'support-link-target (consequent-links n)))

(defunction node (n)
    (find-if #'(lambda (node) (equal (inference-number node) n))
                 *inference-graph*))

(defunction display-inference-node (n )
    (if (numberp n) (setf n (node n)))
    (princ "  # ") (princ (inference-number n)) (princ "   ")
    (when (not (equal (node-kind n) :inference)) (princ (node-kind n)) (princ "         "))
    (prinp (node-formula n))
    (when (node-supposition n)
         (princ "    supposition: ") (set-prinp (node-supposition n)))
    (if (zerop (undefeated-degree-of-support n)) (princ "                  DEFEATED"))
    (terpri) 
    (cond ((node-justification n) (princ "  ") (princ (node-justification n)) (terpri))
                ((support-links n)
                  (princ "  Inferred by:") (terpri)
                  (dolist (L* (support-links n))
                      (princ "                support-link #") (princ (support-link-number L*))
                      (princ " from ") (princ-set (mapcar #'inference-number (support-link-basis L*)))
                      (princ " by ") (princ (support-link-rule L*))
                      (when (support-link-defeaters L*)
                           (princ "  defeaters: ")
                           (princ-set (mapcar #'inference-number (support-link-defeaters L*))))
                      (when (defeating-assignment-trees L*) (princ "   DEFEATED"))
                      (terpri))))
    (princ "  undefeated-degree-of-support: ") (princ (undefeated-degree-of-support n)) (terpri)
    (cond ((deductive-node n)
                 (princ "  This node encodes a deductive argument.") (terpri)))
    (when (node-defeatees n)
         (princ "  defeatees: ")
         (princ "{ ")
         (let ((L (car (node-defeatees n))))
            (princ "link ")
            (princ (support-link-number L)) (princ " for node ")
            (princ (inference-number (support-link-target L))))
         (dolist (L (cdr (node-defeatees n)))
             (princ " , ")
             (princ "link ")
             (princ (support-link-number L)) (princ " for node ")
             (princ (inference-number (support-link-target L))))
         (princ " }")
         (terpri)))

(defunction display-support-link (L)
   (if (numberp L) (setf L (support-link L)))
    (let ((n (support-link-target L)))
     (princ "  # ") (princ (inference-number n)) (princ "   ")
     (when (not (equal (node-kind n) :inference)) (princ (node-kind n)) (princ "         "))
     (prinp (node-formula n))
     (when (node-supposition n)
         (princ "    supposition: ") (set-prinp (node-supposition n)))
     (terpri) 
     (princ "  Inferred by support-link #") (princ (support-link-number L))
     (princ " from ") (princ-set (mapcar #'inference-number (support-link-basis L)))
     (princ " by ") (princ (support-link-rule L))
     (when (support-link-clues L)
         (princ " with clues ")
         (princ-set (mapcar #'inference-number (support-link-clues L))))
     (when (support-link-defeaters L)
         (princ "  defeaters: ") (princ-set (mapcar #'inference-number (support-link-defeaters L))))
     (terpri)
     (when (and (reason-p (support-link-rule L)) (reason-description (support-link-rule L)))
         (princ "  ") (princ (reason-description (support-link-rule L))) (terpri))
     (let ((links (remove L (support-links n))))
       (when links
           (princ "  Previously inferred by:") (terpri)
           (dolist (L* links)
              (princ "                support-link #") (princ (support-link-number L*))
              (princ " from ") (princ-set (mapcar #'inference-number (support-link-basis L*)))
              (princ " by ") (princ (support-link-rule L*))
              (when (support-link-clues L*)
                  (princ " with clues ")
                  (princ-set (mapcar #'inference-number (support-link-clues L*))))
              (when (support-link-defeaters L*)
                  (princ "  defeaters: ")
                        (princ-set (mapcar #'inference-number (support-link-defeaters L*))))
              (terpri))))
    ; (princ "  nearest-defeasible-ancestors: ")
    ; (princ (nearest-defeasible-ancestors n)) (terpri)
      (when (node-defeatees n)
           (princ "  defeatees: ")
           (princ "{ ")
           (let ((L (car (node-defeatees n))))
              (princ "link ")
              (princ (support-link-number L)) (princ " for node ")
              (princ (inference-number (support-link-target L))))
           (dolist (L (cdr (node-defeatees n)))
               (princ " , ")
               (princ "link ")
                (princ (support-link-number L)) (princ " for node ")
                (princ (inference-number (support-link-target L))))
           (princ " }") (terpri)))
    (terpri))

(defunction display-unsupported-node (n )
    (if (numberp n) (setf n (node n)))
    (terpri) (princ "  # ") (princ (inference-number n)) (princ "   ")
    (when (not (equal (node-kind n) :inference)) (princ (node-kind n)) (princ "         "))
    (prinp (node-formula n))
    (when (node-supposition n)
         (princ "    supposition: ") (set-prinp (node-supposition n)))
    (if (zerop (undefeated-degree-of-support n)) (princ "                  DEFEATED"))
    (terpri)
    (when (keywordp (node-justification n)) (princ "  ") (princ (node-justification n)) (terpri))
    ; (princ "  maximal-degree-of-support: ") (princ (compute-maximal-degree-of-support n)) (terpri)
    ; (princ "  undefeated-degree-of-support: ") (princ (compute-undefeated-degree-of-support n)) (terpri)
    (when (and *display?* *graphics-on*)
         (when *graphics-pause* (pause-graphics))
         (draw-n n *og* *nodes-displayed*)
         (push n *nodes-displayed*)))

(defunction subsumes (sequent1 sequent2)
   (and (equal (sequent-formula sequent1) (sequent-formula sequent2))
            (subsetp= (sequent-supposition sequent1) (sequent-supposition sequent2))))

(when (null *trees-loaded*)
     (load (concatenate 'string oscar-pathname "Assignment-trees_3-26"))
     (setf *trees-loaded* t))

;======================================================
; -------------------------------------- CONCLUSIONS -------------------------------------- 

(defstruct (d-node (:conc-name nil) (:print-function print-d-node))
    d-node-number
    (d-node-description nil)
    (discrimination-tests nil)
    (d-node-c-lists nil)
    (d-node-i-lists nil)
    (parent-d-node nil)
    (d-node-forwards-reasons nil)  ;; a list of partially-instantiated-premises
    (d-node-backwards-reasons nil)  ;; a list of non-degenerate backwards-reasons
    (d-node-interest-schemes nil)  ;; a list of partially-instantiated-premises
    (d-node-degenerate-backwards-reasons nil)
    )

(defunction print-d-node (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "d-node: " stream)
    (princ (d-node-number x) stream) (princ ">" stream))

(defunction d-node (n)
    (find-if #'(lambda (dn) (eql (d-node-number dn) n)) *discrimination-net*))

(defunction display-d-node (dn depth test)
   ; (setf d dn de depth te test)
    ;; (step (display-d-node d de te))
    (let ((pp *print-pretty*))
      (setf *print-pretty* nil)
      (line-indent depth)
      (princ "--")
      (if test (prinp-test test) (princ dn))
      (princ "   ")
      (terpri)
      (dolist (cl (d-node-c-lists dn)) (line-indent depth) (princ "       ") (princ cl) (terpri))
      (dolist (il (d-node-i-lists dn)) (line-indent depth) (princ "       ") (princ il) (terpri))
      (dolist (ip (d-node-forwards-reasons dn))
          (line-indent depth)
          (cond ((ip-basis ip) (princ "       instantiated-premise ") (princ (ip-number ip)) (princ " for "))
                      (t (princ "       first premise for ")))
          (princ (ip-reason ip))
          (princ ": ")
          (let ((p (match-sublis (ip-binding ip) (fp-formula (ip-premise ip)))))
            (if (and (negationp p) (negationp (negand p))) (setf p (negand (negand p))))
            (prinp p))
          (terpri))
      (dolist (br (d-node-backwards-reasons dn)) (line-indent depth) (princ "       conclusion for ")
                 (princ br) (terpri))
      (dolist (br (d-node-degenerate-backwards-reasons dn)) (line-indent depth) (princ "       conclusion for ")
                 (princ br) (terpri))
      (dolist (is (d-node-interest-schemes dn))
          (line-indent depth)
          (princ "       interest-scheme ") (princ (is-number is)) (princ " for interest ")
          (princ (interest-number (is-target-interest is)))
          (princ " by ")
          (princ (is-reason is))
          (princ ": ")
          (let ((p (match-sublis (is-binding is) (fp-formula (is-premise is)))))
            (if (and (negationp p) (negationp (negand p))) (setf p (negand (negand p))))
            (prinp p))
          (terpri))
      (setf *print-pretty* pp)))

(defunction formula-code (P)
    (setf *quantifier-number* 0)
    (multiple-value-bind (code term-list) (formula-code* P nil)
         (values (reverse code) term-list)))

(defunction formula-code* (P descriptor)
    (cond ((listp P)
                 (let ((description nil) (elt-num 1) (term-list nil))
                    (cond
                      ;; This handles notational variants.
                      ((or (eq (car p) 'all) (eq (car P) 'some))
                        (setf P
                                 (cons (car P) (subst (list 'q-var (incf *quantifier-number*)) (mem2 P) (cddr P)))))
                      ((eq (car P) 'at)
                        (setf term-list (cddr P))
                        (setf P (list (car P) (cadr P))))
                      ((eq (car P) 'throughout)
                        (setf term-list (cdr (mem3 P)))
                        (setf P (list (car P) (cadr P) (list (car (mem3 P))))))
                      ((and (symbolp (car P))
                                 (not (member (car P) *operators*))
                                 (not (member (car P) '(~ & v -> <-> all some ? @))))
                        (setf term-list (cdr P))
                        (setf P (list (car P)))))
                    (dolist (Q P)
                        (let ((Q-descriptor (cons elt-num descriptor)))
                           (cond ((not (listp Q))
                                        (push (cons (reverse Q-descriptor) Q) description))
                                       (t 
                                         (multiple-value-bind (d tl) (formula-code* Q Q-descriptor)
                                              (setf term-list (append tl term-list))
                                              (setf description (append d description))
                                              )))
                           (incf elt-num)))
                    (values description term-list)))
                (t (values (list (cons descriptor P)) nil))))

(defun display-discrimination-net (&optional (nodes *discrimination-net*))
    (setf *callees* nil)
    (setf *blank-line* nil)
    (setf *line-columns* nil)
    (display-discrimination-node *top-d-node* nil 0 t nodes)
    nil)

(defun ddn (&optional (nodes *discrimination-net*)) (display-discrimination-net nodes))

(defun display-discrimination-node (d-node listees depth last? nodes &optional test)
    (when (member d-node nodes)
         (when (null depth)
              (setf depth 0) (setf listees nil))
         (cond ((or (mem d-node listees) (mem d-node *callees*))
                     (line-indent depth)
                     (when (not (mem depth *line-columns*)) (princ "|"))
                     (princ "--") (princ d-node) (princ " .....") (terpri)
                     (setf *blank-line* nil)
                     (cond (last? (pull depth *line-columns*))
                               (t (pushnew depth *line-columns* :test 'eql))))
                   (t
                     (let* ((DC (discrimination-tests d-node))
                               (number (length (discrimination-tests d-node)))
                               (number* (round (/ number 2)))
                               (draw-line?
                                 (or (mem d-node listees)
                                       (mem d-node *callees*)
                                       (some #'(lambda (C) (not (mem c listees))) (discrimination-tests d-node)))))
                       (pushnew d-node listees :test 'equal)
                       (push d-node *callees*)
                       (when (and (not *blank-line*) (> number* 0))
                            (line-indent depth) (terpri) (setf *blank-line* t))
                       (dotimes (n number*)
                           (let ((test (mem1 DC)))
                             (cond
                               ((zerop n)
                                 (display-discrimination-node (cdr test) listees (1+ depth) nil nodes test))
                               ((cdr DC) (display-discrimination-node (cdr test) listees (1+ depth) nil nodes test))
                               (t (display-discrimination-node (cdr test) listees (1+ depth) t nodes test))))
                           (setf DC (cdr DC)))
                       (pushnew depth *line-columns* :test 'eql)
                       (display-d-node d-node depth test)
                       (setf *blank-line* nil)
                       (when last? (pull depth *line-columns*))
                       (when (> number 0) (pushnew (1+ depth) *line-columns* :test 'eql))
                       (dolist (test DC)
                           (cond
                             ((cdr DC)
                               (display-discrimination-node (cdr test) listees (1+ depth) nil nodes test))
                             (t (display-discrimination-node (cdr test) listees (1+ depth) t nodes test)))
                           (setf DC (cdr DC)))
                       (when
                            (and (not *blank-line*) draw-line?)
                            (line-indent depth) (terpri) (setf *blank-line* t))
                       )))))

#| The list of instantiated-premises for a forwards-reason. |#
(defunction reason-ips (reason)
    (let ((ips nil))
      (dolist (dn *discrimination-net*)
          (dolist (ip (d-node-forwards-reasons dn))
              (when (equal (ip-reason ip) reason) (push ip ips))))
      ips))

#| The list of interest-schemes for a backwards-reason. |#
(defunction reason-iss (reason)
    (let ((iss nil))
      (dolist (dn *discrimination-net*)
          (dolist (is (d-node-interest-schemes dn))
              (when (equal (ip-reason is) reason) (push is iss))))
      iss))

(defunction d-node-ancestors (dn)
    (let ((pn (parent-d-node dn)))
      (when pn (cons pn (d-node-ancestors pn)))))

(defunction d-node-descendants (dn)
    (when (discrimination-tests dn)
         (let ((nodes (a-range (discrimination-tests dn))))
           (append nodes (unionmapcar #'d-node-descendants nodes)))))

#| Display the part of the discrimination-net that contains d-node number n. |#
(defunction show-d-node (n)
    (let* ((dn (if (numberp n) (d-node n) n))
              (nodes (cons dn (append (d-node-ancestors dn) (d-node-descendants dn)))))
      (display-discrimination-net nodes)))

(defunction show-interest (n)
    (let* ((in (if (numberp n) (interest n) n))
              (dn (i-list-d-node (interest-i-list in)))
              (nodes (cons dn (append (d-node-ancestors dn) (d-node-descendants dn)))))
      (display-discrimination-net nodes)))

(defunction show-node (n)
    (let* ((node (if (numberp n) (node n) n))
              (dn (c-list-d-node (node-c-list node)))
              (nodes (cons dn (append (d-node-ancestors dn) (d-node-descendants dn)))))
      (display-discrimination-net nodes)))

#| This displays all d-nodes directly relevant to the reason. |#
(defunction show-reason (reason)
    (let ((nodes nil))
      (cond ((forwards-reason-p reason)
                  (dolist (dn *discrimination-net*)
                      (when (some #'(lambda (ip) (equal (ip-reason ip) reason)) (d-node-forwards-reasons dn))
                           (push dn nodes))))
                ((backwards-reason-p reason)
                  (dolist (dn *discrimination-net*)
                      (when
                           (or (member reason (d-node-backwards-reasons dn))
                                 (member reason (d-node-degenerate-backwards-reasons dn))
                                 (some #'(lambda (is) (equal (is-reason is) reason)) (d-node-interest-schemes dn)))
                           (push dn nodes)))))
      (setf nodes
               (unionmapcar+
                 #'(lambda (dn) (cons dn (append (d-node-ancestors dn) (d-node-descendants dn))))
                 nodes))
      (display-discrimination-net nodes)))

(defunction prinp-test (test)
    (princ "(") (princ (caar test)) (princ " . ") (prinp (cdar test)) (princ ") : ") (princ (cdr test)))

(defstruct (c-list (:print-function print-c-list)
                              (:conc-name nil))
    (c-list-formula nil)
    (corresponding-i-lists nil)
    (c-list-nodes nil)
    (c-list-processed-nodes nil)
    (link-defeatees nil)
    (reductio-interests nil)
    (c-list-variables nil)
    (c-list-contradictors nil)
    (c-list-term-list nil)
    (c-list-d-node nil)
    (generated-instantiated-premises nil)
    (supported-interest-schemes nil))

(defun print-c-list (x stream depth)
    (declare (ignore depth))
    (princ "#<c-list for " stream)
    (prinp (c-list-formula x) stream) (princ ">" stream))

(defunction processed-c-list-for (formula)
    (cdr (find-if #'(lambda (cl) (notational-variant formula (car cl))) *processed-conclusions*)))

(defunction notational-variant (p q &optional vars)
    (cond ((null p) (null q))
                ((listp p)
                  (and (listp q)
                            (cond ((and (or (eq (car p) 'some) (eq (car p) 'all))
                                                  (eq (car p) (car q)))
                                                        (notational-variant (cdr p) (cdr q)
                                                                                          (cons (cons (cadr p) (cadr q)) vars)))
                                        ((listp (car q)) (and (notational-variant (car p) (car q) vars)
                                                                    (notational-variant (cdr p) (cdr q) vars)))
                                        ((or (eql (car p) (car q))
                                                (and vars
                                                          (mem (cons (car p) (car q)) vars)))
                                          (notational-variant (cdr p) (cdr q) vars)
                                          ))))
                (t (and (not (listp q))
                             (or (eql p q)
                                   (mem (cons p q) vars))))))

(defunction nodes-for (formula)
    (let ((c-list (c-list-for formula)))
       (if c-list (c-list-nodes c-list))))

(defunction processed-nodes-for (formula)
    (let ((c-list (processed-c-list-for formula)))
       (if c-list (c-list-nodes c-list))))

(defunction display-conclusions ()
    (princ "(") (terpri)
    (princ "================== CONCLUSIONS ===================")
    (let* ((**conclusions**
               (unionmapcar
                 #'(lambda (dn)
                       (unionmapcar
                         #'(lambda (cl) (c-list-nodes cl)) (d-node-c-lists dn)))
                 *discrimination-net*))
              (conclusions
                (order **conclusions**
                            #'(lambda (c1 c2)
                                  (< (inference-number c1) (inference-number c2))))))
       (dolist (conclusion conclusions)
           (display-conclusion conclusion)
           (terpri) (princ "---------------------------------------------------")))
    (princ ")") (terpri))

(defunction display-conclusion (n)
    (terpri) (princ n)
    (when (not (equal (node-kind n) :inference))
         (terpri) (princ "  kind: ") (princ (node-kind n)))
    ; (terpri) (princ "  maximal-degree-of-support: ") (princ (compute-maximal-degree-of-support n))
    (terpri) (princ "  undefeated-degree-of-support: ") (princ (compute-undefeated-degree-of-support n))
    (dolist (Q (answered-queries n))
        (terpri) (princ "  This answers ") (princ Q)))

(defunction display-conclusions-by-supposition ()
    (princ "(") (terpri)
    (let ((suppositions nil))
       (dolist (dn *discrimination-net*)
           (dolist (cl (d-node-c-lists dn))
               (dolist (c (c-list-nodes cl))
                   (pushnew (node-supposition c) suppositions :test '==)
                   (setf suppositions
                            (order suppositions
                                        #'(lambda (s1 s2)
                                              (or (< (length s1) (length s2))
                                                    (and (= (length s1) (length s2))
                                                              (lessp s1 s2)))))))))
       (let* ((**conclusions**
                  (unionmapcar
                    #'(lambda (dn)
                          (unionmapcar
                            #'(lambda (cl) (c-list-nodes cl)) (d-node-c-lists dn)))
                    *discrimination-net*)))
          (dolist (sup suppositions)
              (princ "==========================================") (terpri)
              (princ "Conclusions with supposition ") (set-prinp sup) (princ ":") (terpri)
              (let* ((sup-conclusions
                         (subset #'(lambda (c) (== (node-supposition c) sup))
                                        **conclusions**))
                        (conclusions
                          (order sup-conclusions
                                      #'(lambda (c1 c2)
                                            (< (inference-number c1) (inference-number c2))))))
                 (dolist (c conclusions)
                     (when (== (node-supposition c) sup)
                          (princ "    #") (princ (inference-number c)) (princ "  ")
                          (prinp (node-formula c)) (terpri)))))))
    (princ ")") (terpri))

(defunction display-c-lists ()
    (princ "(") (terpri)
    (dolist (dn *discrimination-net*)
        (dolist (cl (d-node-c-lists dn))
            (princ "==========================================") (terpri)
            (princ "c-list-formula: ") (prinp (c-list-formula cl)) (terpri)
            (let ((conclusions
                      (order (c-list-nodes cl)
                                  #'(lambda (c1 c2)
                                        (let ((s1 (node-supposition c1))
                                                (s2 (node-supposition c2)))
                                           (or (< (length s1) (length s2))
                                                 (and (= (length s1) (length s2))
                                                           (lessp s1 s2))))))))
               (dolist (c conclusions)
                   (princ "    #") (princ (inference-number c))
                   (princ "   sup = ") (set-prinp (node-supposition c))
                   (terpri)))))
    (princ ")") (terpri))

(defunction display-processed-c-lists ()
    (princ "(") (terpri)
    (dolist (cl *processed-conclusions*)
        (princ "==========================================") (terpri)
        (princ "c-list-formula: ") (prinp (car cl)) (terpri)
        (let ((conclusions
                  (order (c-list-nodes (cdr cl))
                              #'(lambda (c1 c2)
                                    (let ((s1 (node-supposition c1))
                                            (s2 (node-supposition c2)))
                                       (or (< (length s1) (length s2))
                                             (and (= (length s1) (length s2))
                                                       (lessp s1 s2))))))))
           (dolist (c conclusions)
               (princ "    #") (princ (inference-number c))
               (princ "   sup = ") (set-prinp (node-supposition c))
               (terpri))))
    (princ ")") (terpri))

(defunction ?-variables (formula)
    (cond ((and formula (listp formula))
                (union (?-variables (car formula)) (?-variables (cdr formula))))
              ((atom formula)
                (if (equal (car (explode (write-to-string formula))) "?") (list formula)))))

#| (? formula), where formula can contain variables of the form "?x",  returns a list of all 
known conclusions matching the formula. |#
(defunction ? (formula)
    (when (stringp formula) (setf formula (reform formula)))
    (let* ((d-node (d-node-for formula))
              (nodes (search-d-nodes formula d-node)))
      (cond (nodes
                  (terpri)
                  (princ "The following answers are known for the query (? ") (prinp formula) (princ "):") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                   (dolist (node nodes)
                       (princ "    ") (princ (node-formula node)) (princ "    by node #")
                       (princ (inference-number node)) (terpri))
                   (terpri))
                (t 
                  (terpri) (princ "No answers are known for the query (? ") (prinp formula) (princ ").") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                  (terpri)))
      nodes))

(defunction search-d-nodes (formula d-node)
    (let ((nodes nil)
            (?-vars (?-variables formula)))
      (dolist (c-list (d-node-c-lists d-node))
          (dolist (node (c-list-nodes c-list))
              (when (and (null (node-supposition node))
                                  (match formula (node-formula node) ?-vars))
                   (push node nodes))))
      (append nodes
                     (unionmapcar #'(lambda (dt) (search-d-nodes formula (cdr dt)))
                                             (discrimination-tests d-node)))))

(defunction ?interests (formula)
    (when (stringp formula) (setf formula (reform formula)))
    (let* ((d-node (d-node-for formula))
              (interests (search-d-node-interests formula d-node)))
      (cond (interests
                  (terpri)
                  (princ "The following interests were adopted for the query (? ") (prinp formula) (princ "):") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                   (dolist (interest interests)
                       (princ "    ") (princ (interest-formula interest)) (princ "    by interest #")
                       (princ (interest-number interest)) (terpri))
                   (terpri))
                (t 
                  (terpri) (princ "No interests were adopted for the query (? ") (prinp formula) (princ ").") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                  (terpri)))
      interests))

(defunction search-d-node-interests (formula d-node)
    (let ((interests nil)
            (?-vars (?-variables formula)))
      (dolist (i-list (d-node-i-lists d-node))
          (dolist (interest (i-list-interests i-list))
              (when (and (null (node-supposition interest))
                                  (match formula (interest-formula interest) ?-vars))
                   (push interest interests))))
      (append interests
                     (unionmapcar #'(lambda (dt) (search-d-node-interests formula (cdr dt)))
                                             (discrimination-tests d-node)))))

; ---------------------------- ULTIMATE-EPISTEMIC-INTERESTS -----------------------------

(defstruct (query (:print-function print-query)
                                (:conc-name nil))
   (query-number 0)
   (query-formula nil)
   (query-strength 0)
   (query-queue-node nil)
   (deductive-query nil)  ;; t if the query is whether the query formula is deductively provable
   (positive-query-instructions nil) ;; a list of functions applicable to an inference-node
   (negative-query-instructions nil) ;; a list of functions applicable to an inference-node
   (query-answers nil)  ;;a list of inference-nodes
   (answered? nil)  ;; t if some answer is justified to degree greater than or equal
                                   ;; to the degree of interest, nil otherwise
   (query-interest nil)   ;; the interest recording the query
   (negative-query-interest nil)  ;; the negative-interest for a whether-query
   (?-constraint nil))  ;; a function which when applied to the ?-vars yields a discharge-condition
                                    ;; for the query-interest, constraining the instantiating terms.

(defun print-query (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Query " stream) (princ (query-number x) stream)
    (princ ": " stream) (princ (pretty (query-formula x)) stream)
    (princ ">" stream))

(defunction ?-query-p (Q)
    (and (query-p Q) (?-genp (query-formula Q))))

#| This returns two values: the matrix, and the list of ?-variables. |#
(defunction ?-matrix (p &optional vars)
    (push (q-variable p) vars)
    (let ((formula (q-matrix p)))
       (cond ((?-genp formula) (?-matrix formula vars))
                   (t (values formula vars)))))

(defunction whether-query-p (Q)
    (and (query-p Q) (whether-formula (query-formula Q))))

(defunction query (n)
    (find-if #'(lambda (c) (equal (query-number c) n))
                 *ultimate-epistemic-interests*))

(defunction show-query (Q)
    (if (numberp Q) (setf Q (query Q)))
    (princ Q) (terpri))

(defunction show-queries ()
    (terpri)
    (princ
      "================== ULTIMATE EPISTEMIC INTERESTS ===================")
    (terpri)
    (dolist (Q *ultimate-epistemic-interests*)
        (show-query Q)))

(defunction inclusive-node-ancestors (node)
    (cons node (node-ancestors node)))

(defunction ancestral-links (node)
    (unionmapcar+ #'support-links (inclusive-node-ancestors node)))

(defunction display-query (Q)
    (princ "  Interest in ") (prinp (query-formula Q)) (terpri)
    (cond ((null (answered? Q))
                 (princ "  is unsatisfied.")
                 (when (null (query-answers Q)) (princ "  NO ARGUMENT WAS FOUND."))
                 (terpri))
                ((or (whether-query-p Q) (?-query-p Q))
                  (dolist (C (query-answers Q))
                      (when (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                           (princ "  is answered by node ")
                           (princ (inference-number C)) (princ ":  ")
                           (princ (pretty (node-formula C))) (terpri)
                           (let ((skolem-functions (skolem-functions (node-formula C))))
                              (when skolem-functions
                                   (let* ((sf (mem1 skolem-functions))
                                             (support-link
                                               (find-if #'(lambda (SL)
                                                                 (and (eq (support-link-rule SL) EI)
                                                                           (occur sf (node-formula (support-link-target SL)))
                                                                           (not (occur sf (node-formula (mem1 (support-link-basis SL)))))))
                                                            (ancestral-links C))))
                                      (when support-link
                                           (let* ((node (mem1 (support-link-basis support-link)))
                                                     (formula (node-formula node))
                                                     (var (q-variable formula)))
                                              (princ "  where ") (princ sf) (princ " is any ") (princ var)
                                              (princ " such that ") (princ (q-matrix formula)) (princ ",") (terpri)
                                              (princ "  and the existence of such")
                                              (if (equal var "x") (princ " an ") (princ " a ")) (princ var)
                                              (princ " is guaranteed by node ") (princ (inference-number node)) (terpri))))))
                           )))
                (t (dolist (C (query-answers Q))
                       (when (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                            (princ "  is answered affirmatively by node ")
                            (princ (inference-number C)) (terpri)))))
    (princ "---------------------------------------------------") (terpri))

(defunction display-queries ()
    (terpri)
    (princ
      "================== ULTIMATE EPISTEMIC INTERESTS ===================")
    (terpri)
    (dolist (Q *ultimate-epistemic-interests*)
        (display-query Q)))

(defunction answers (formula query)
   (let ((query-formula (query-formula query)))
     (if (?-genp query-formula)
       (instance-of formula query-formula)
       (equal formula query-formula))))

#| This assumes that formula2 is indefinite. |#
(defunction instance-of (formula1 formula2)
    (match (mem2 formula2) formula1 (list (mem2 (mem1 formula2)))))

(defunction in-interest (sequent)
    (let ((interests (interests-for (sequent-formula sequent) nil)))
       (when interests
            (some #'(lambda (interest) (null (interest-supposition interest)))
                         interests))))

(defunction adopt-ultimate-interest (query)
    (push query *ultimate-epistemic-interests*)
    (when (not (in-interest (list nil (query-formula query))))
         (queue-query-for-interest query)))

(defunction queue-query-for-interest (query)
    (let ((node
              (make-inference-queue-node
                :queue-number (incf *queue-number*)
                :enqued-item query
                :item-kind :query
                :item-complexity (complexity (query-formula query))
                :discounted-strength (query-strength query)
                :degree-of-preference (query-preference query))))
       (setf (query-queue-node query) node)
       (setf *inference-queue* (ordered-insert node *inference-queue* #'i-preferred))))

; -------------------------------------- INTERESTS -------------------------------------- 

(defstruct (instantiated-premise (:print-function print-instantiated-premise) (:conc-name ip-))
    (reason nil)
    (binding nil)  ;; cumulative binding prior to this premise
    (basis nil)
    (premise nil)
    (remaining-premises nil)  ;; premises left to be instantiated
    (instantiations nil)  ;; instantiations of node-variables in previous premises
    (used-premise-variables nil)  ;; premise-variables bound in earlier premises
    (used-variables nil)  ;; conclusion-variables occurring in basis
    (derived-premises nil)  ;; instantiated-premises immediately following this one
    (d-node nil)
    (number 0)
    (clues nil)
     (initial?  nil))   ;; records whether the premise is the initial premise of the reason

(defun print-instantiated-premise (x stream depth)
    (declare (ignore depth))
    (princ "<instantiated-premise " stream) (princ (ip-number x) stream) (princ " for " stream)
    (princ (ip-reason x) stream)
    (princ ">" stream))

(defstruct (interest-scheme (:include instantiated-premise)
                                                    (:print-function print-interest-scheme) (:conc-name is-))
    (target-interest nil)
    (supposition nil)
    (supposition-variables nil)
    (instance-function nil)
    (generating-node nil))

(defun print-interest-scheme (x stream depth)
    (declare (ignore depth))
    (princ "<<interest-scheme " stream) (princ (is-number x) stream) (princ " for " stream)
    (princ (is-target-interest x) stream) (princ " by " stream) (princ (ip-reason x) stream) (princ ">>" stream))

#| This finds the interest-scheme with is-number n. |#
(defunction interest-scheme (n)
    (let ((is nil))
      (some #'(lambda (dn)
                       (find-if #'(lambda (i)
                                         (and (equal (is-number i) n)
                                                  (setf is i)))
                                   (d-node-interest-schemes dn)))
                  *discrimination-net*)
      is))

#| This finds the instantiated-premise with ip-number n. |#
(defunction instantiated-premise (n)
    (let ((ip nil))
      (some #'(lambda (dn)
                       (find-if #'(lambda (i)
                                         (and (equal (ip-number i) n)
                                                  (setf ip i)))
                                   (d-node-forwards-reasons dn)))
                  *discrimination-net*)
      ip))

(defmacro is-derived-interest-schemes (is) `(is-derived-premises ,is))

(defstruct (interest-link (:print-function print-interest-link)
                                           (:conc-name nil))   ; "An interest-graph-link"
    (link-number 0)
    (resultant-interest nil)
    (link-interest nil)
    (link-interest-formula nil)
    (link-interest-condition nil)
    (link-binding nil)
    (link-rule nil)
    (remaining-premises nil)
    (supporting-nodes nil)
    (link-instantiations nil)
    (link-supposition nil)
    (link-defeaters nil)
    (link-defeat-status nil)
    (link-strength 0)  ; maximum-degree-of-interest conveyed
    (link-generating-node nil)
    (discharged-link nil)
    (interest-match nil)
    (interest-reverse-match nil)
    (generating-link nil)
    (link-premise nil)
    (link-clues nil)
    )

(defun print-interest-link (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Link " stream)
    (princ (link-number x) stream)
    (when (resultant-interest x)
      (princ ": for  interest #" stream) (princ (interest-number (resultant-interest x)) stream))
    (princ " by " stream) (princ (link-rule x) stream)
    (princ ">" stream))

(defunction link (n)
    (find-if #'(lambda (node) (equal (link-number node) n)) *interest-links*))

(defunction display-links ()
    (dolist (L *interest-links*) (princ L) (terpri)))

(defunction display-link (L)
    (princ "INTEREST-LINK #") (princ (link-number L)) (terpri)
    (princ "  resultant-interest: ") (princ (resultant-interest L)) (terpri)
    (princ "  supporting-nodes: ") (princ (supporting-nodes L)) (terpri)
    (princ "  link-interest: ") (princ (link-interest L)) (terpri)
    (princ "  remaining-premises: ") (princ (remaining-premises L)) (terpri)
    (princ "  reason: ") (princ (link-rule L)) (terpri)
    (princ "  link-interest: ") (princ (link-interest L)) (terpri)
    )

(defstruct (interest (:print-function print-interest)
                                    (:conc-name nil))   ; "An interest-graph-node"
    (interest-number 0)
    (interest-sequent nil)
    (interest-formula nil)
    (interest-supposition nil)
    (right-links nil)
    (left-links nil)
    (degree-of-interest *base-priority*)
    (last-processed-degree-of-interest nil)
    (interest-defeat-status nil)
    (discharged-degree nil)  ;; used in computing priorities
    (deductive-interest nil)
    (cancelled-interest nil)
    (interest-queue-node nil)
    (interest-i-list nil)
    (maximum-degree-of-interest 0)
    (interest-defeatees nil)
    (reductio-interest nil)  ;; is the interest partly for reductio?
    (direct-reductio-interest nil)
    (generated-suppositions nil)
    (generating-nodes nil)
    (interest-priority 0)
    (interest-variables nil)
    (discharge-condition nil)  ;;a function of node, unifier, and interest-link
    (interest-supposition-variables nil)
    (cancelling-node nil)
    (discharging-nodes nil)
    (interest-supposition-nodes nil)
    (generated-interest-schemes nil)
    (defeater-binding nil)
    (generating-defeat-nodes nil)
    (cancelled-left-links nil)
   (non-reductio-interest t)  ;; is the interest partly for non-reductio?
    (anchored-nodes nil)
    (text-discharge-condition nil)  ;; a text statement of the discharge condition
    (enabled-nodes nil)  ;; the nodes for which this is an enabling-interest
    )

#|
(defun print-interest (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Interest " stream)
    (princ (interest-number x) stream)
    (princ ": " stream) (prinp-sequent (interest-sequent x) stream)
    (princ ">" stream))
|#

(defun print-interest (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Interest " stream)
    (princ (interest-number x) stream)
   ; (princ ": " stream) (prinp-sequent (interest-sequent x) stream)
    (princ ">" stream))

(defunction ifm (n)
    (when (numberp n) (setf n (interest n)))
    (prinp (interest-formula n))
    (interest-formula n))

(defstruct (i-list (:print-function print-i-list)
                              (:conc-name nil))
    (i-list-formula nil)
    (corresponding-c-lists nil)
    (i-list-interests nil)
    (i-list-queries nil)
    (reductio-trigger nil)
    (i-list-reductio-supposition nil)
    (i-list-variables)
    (i-list-term-list nil)
    (i-list-d-node nil))

(defun print-i-list (x stream depth)
    (declare (ignore depth))
    (princ "#<i-list for " stream)
    (prinp (i-list-formula x) stream) (princ ">" stream))

#| This returns three values -- the i-list and the match and its reverse. |#
(defunction i-list-for (formula i-vars)
    (multiple-value-bind (profile term-list) (formula-code formula)
         (let ((d-node (pursue-d-node-for profile *top-d-node*)))
           (when d-node
                (some
                  #'(lambda (il)
                        (multiple-value-bind
                             (match match*)
                             (one-one-match term-list (i-list-term-list il) i-vars (i-list-variables il))
                             (when match
                                  (return-from i-list-for (values il match match*)))))
                  (d-node-i-lists d-node))))))

#| If p and q match one-one, this returns the match and its reverse-match. |#
(defunction one-one-match (p q p-vars q-vars)
    (let* ((match (match p q p-vars))
              (match* (reverse-match match)))
       (when
            (and match
                      (or (eq match t)
                            (and
                              (subsetp (a-range match) q-vars)
                              (equal (match-sublis match* q) p))))
            (values match match*))))

#| This returns two values -- the list of interests, and the match |#
(defunction interests-for (formula i-vars)
    (multiple-value-bind
         (i-list match)
         (i-list-for formula i-vars)
         (if i-list (values (i-list-interests i-list) match))))

#| c-variables is the list of node-variables. |#
(defunction matching-i-lists-for (term-list c-variables d-node)
    (let ((i-lists nil))
       (dolist (il (d-node-i-lists d-node))
           (let ((unifier (unifier term-list (i-list-term-list il) c-variables (i-list-variables il))))
              (if unifier (push (list il unifier) i-lists))))
       i-lists))

#| c-variables is the list of node-variables. |#
(defunction matching-c-lists-for (term-list i-variables d-node)
    (let ((c-lists nil))
       (dolist (cl (d-node-c-lists d-node))
           (let ((unifier (unifier  (c-list-term-list cl) term-list (c-list-variables cl) i-variables)))
              (if unifier (push (list cl unifier) c-lists))))
       c-lists))

(defunction store-interest (interest &optional i-list)
   ; (when (eq (interest-number interest) 11) (setf i interest il i-list) (break))
    ;; (step (store-interest i il))
    (push interest *interests*)
    (cond (i-list
                 (push interest (i-list-interests i-list))
                 (let ((reductio-sup (i-list-reductio-supposition i-list)))
                    (when reductio-sup
                         (push interest  (generating-interests reductio-sup))
                         (push reductio-sup (generated-suppositions interest))))
                 (setf (interest-i-list interest) i-list))
                (t 
                  (multiple-value-bind (profile term-list) (formula-code (interest-formula interest))
                       (index-interest interest profile term-list *top-d-node*)))))

#| (descrimination-tests d-node) is an a-list of pairs (test . dn), where test has the form of the
car of a formula-code, and dn is a d-node. |#
(defunction index-interest (interest profile term-list d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node)))
            (new-profile (cdr profile)))
      (cond (dn
                  (if new-profile (index-interest interest new-profile term-list dn)
                       (store-interest-at-d-node interest term-list dn)))
                (new-profile
                  (index-interest-at-new-nodes interest term-list d-node new-profile (car profile)))
                (t (store-interest-at-new-d-node
                      interest term-list d-node (car profile))))))

(defunction fetch-I-list-for (term-list d-node)
    (find-if #'(lambda (il)
                      (equal term-list (i-list-term-list il)))
                 (d-node-i-lists d-node)))

(defunction store-interest-at-d-node (interest term-list dn)
   ; (when (eq interest (interest 11)) (setf i interest tl term-list d dn) (break))
    ;; (step (store-interest-at-d-node i tl d))
    (let* ((formula (interest-formula interest))
              (i-variables (interest-variables interest))
              (i-list (fetch-i-list-for term-list dn)))
       (cond (i-list
                    (push interest (i-list-interests i-list))
                    (let ((reductio-sup (i-list-reductio-supposition i-list)))
                       (when reductio-sup
                            (push interest  (generating-interests reductio-sup))
                            (push reductio-sup (generated-suppositions interest)))))
                   (t (let ((c-lists (matching-c-lists-for term-list i-variables dn)))
                         (setf i-list (make-i-list
                                            :i-list-formula formula
                                            :corresponding-c-lists c-lists
                                            :i-list-interests (list interest)
                                            :reductio-trigger
                                            (appropriate-for-reductio-supposition formula)
                                            :i-list-variables i-variables
                                            :i-list-term-list term-list
                                            :i-list-d-node dn
                                            ))
                         (push i-list (d-node-i-lists dn))
                         (dolist (cl c-lists)
                             (push (cons i-list (cdr cl)) (corresponding-i-lists (mem1 cl)))))))
       (setf (interest-i-list interest) i-list)))

#| Test is the final member of the formula-profile for the node-formula. |#
(defunction store-interest-at-new-d-node (interest term-list d-node test)
   ; (when (eq interest (interest 7)) (setf i interest tl term-list d d-node ts test) (break))
    ;; (step (store-interest-at-new-node i tl d ts))
    (let* ((i-variables (interest-variables interest))
              (formula (interest-formula interest))
              (dn (make-d-node
                       :d-node-number (incf *d-node-number*)
                       :d-node-description (cons test (d-node-description d-node))
                       :parent-d-node d-node))
              (i-list (make-i-list
                          :i-list-formula formula
                          :i-list-interests (list interest)
                          :reductio-trigger
                          (appropriate-for-reductio-supposition formula)
                          :i-list-variables i-variables
                          :i-list-term-list term-list
                          :i-list-d-node dn
                          )))
       (push dn *discrimination-net*)
       (push (cons test dn) (discrimination-tests d-node))
       (setf (d-node-i-lists dn) (list i-list))
       (setf (interest-i-list interest) i-list)))

(defunction find-matching-i-lists-for (formula variables)
    (multiple-value-bind (profile term-list) (formula-code formula)
         (pursue-i-lists-for formula profile term-list variables *top-d-node*)))
    
(defunction pursue-i-lists-for (formula profile term-list variables d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-i-lists-for formula new-profile term-list variables dn))
                 (t (matching-i-lists-for term-list variables dn)))))))

(defunction index-interest-at-new-nodes (interest term-list d-node profile test)
    (let ((dn (make-d-node
                     :d-node-number (incf *d-node-number*)
                     :d-node-description (cons test (d-node-description d-node))
                     :parent-d-node d-node)))
       (push (cons test dn) (discrimination-tests d-node))
       (push dn *discrimination-net*)
       (let ((desc (cdr profile)))
          (cond (desc (index-interest-at-new-nodes interest term-list dn desc (car profile)))
                      (t (store-interest-at-new-d-node interest term-list dn (car profile)))))))

(defunction pursue-d-node-for (profile d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-d-node-for new-profile dn))
                 (t dn))))))

(defunction store-interest-with-c-lists (interest c-lists)
  ;  (when (eq (interest-number interest) 25) (setf i interest cl c-lists) (break))
    ;; (step (store-interest-with-c-lists i cl))
    (multiple-value-bind (profile term-list) (formula-code (interest-formula interest))
         (declare (ignore profile))
         (cond
           (c-lists
             (push interest *interests*)
             (let* ((formula (interest-formula interest))
                       (dn (c-list-d-node (caar c-lists)))
                       (i-list (fetch-i-list-for term-list dn))
                       (i-variables (interest-variables interest)))
                (cond (i-list
                             (push interest (i-list-interests i-list))
                             (let ((reductio-sup (i-list-reductio-supposition i-list)))
                                (when reductio-sup
                                     (push interest  (generating-interests reductio-sup))
                                     (push reductio-sup (generated-suppositions interest)))))
                            (t (setf i-list (make-i-list
                                                  :i-list-formula formula
                                                  :corresponding-c-lists c-lists
                                                  :i-list-interests (list interest)
                                                  :reductio-trigger
                                                  (appropriate-for-reductio-supposition formula)
                                                  :i-list-variables i-variables
                                                  :i-list-term-list term-list
                                                  :i-list-d-node dn
                                                  ))
                                (push i-list (d-node-i-lists dn))
                                (dolist (cl c-lists)
                                    (push (cons i-list (cdr cl)) (corresponding-i-lists (mem1 cl))))))
                (setf (interest-i-list interest) i-list)))
           (t (store-interest interest)))))

(defunction appropriate-for-reductio-supposition (formula)
    (and
      (not (conjunctionp formula))
      (not (conditionalp formula))
      (not (biconditionalp formula))
      (not (disjunctionp formula))
      (not (u-genp formula))
      (not (undercutterp formula))
      (or (not (negationp formula))
            (atomic-formula (mem2 formula)))))

(defunction store-inference-node (node formula)
   ; (when (eql (inference-number node) 14) (setf n node f formula) (break))
    ;; (step (store-inference-node n f))
    (multiple-value-bind (profile term-list) (formula-code formula)
         (index-inference-node node profile term-list *top-d-node*)))

#| (descrimination-tests d-node) is an a-list of pairs (test . dn), where test has the form of the
car of a formula-code, and dn is a d-node. |#
(defunction index-inference-node (node profile term-list d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node)))
            (new-profile (cdr profile)))
       (cond (dn
                    (if new-profile (index-inference-node node new-profile term-list dn)
                         (store-inference-node-at-d-node node term-list dn)))
                   (new-profile
                     (index-inference-node-at-new-nodes node term-list d-node new-profile (car profile)))
                   (t
                     (store-inference-node-at-new-d-node
                        node term-list d-node (car profile))))))

(defunction fetch-c-list-for (formula d-node)
    (find-if #'(lambda (cl) (notational-variant formula (c-list-formula cl)))
                 (d-node-c-lists d-node)))

(defunction store-inference-node-at-d-node (node term-list dn)
    (let* ((formula (node-formula node))
              (c-list (fetch-c-list-for formula dn))
              (c-variables (node-variables node)))
       (cond (c-list
                    (if (is-inference node) (push node (c-list-nodes c-list))))
                   (t (let ((i-lists (matching-i-lists-for term-list c-variables dn)))
                         (setf c-list (make-c-list
                                             :c-list-formula formula
                                             :corresponding-i-lists i-lists
                                             :c-list-nodes (if (is-inference node) (list node))
                                             :reductio-interests
                                             (appropriate-for-reductio-interest formula)
                                             :c-list-variables c-variables
                                             :c-list-term-list term-list
                                             :c-list-d-node dn
                                             ))
                         (push c-list (d-node-c-lists dn))
                         (dolist (il i-lists)
                             (push (cons c-list (cdr il)) (corresponding-c-lists (mem1 il)))))
                       (when
                            (appropriate-for-contradictors formula)
                            (setf (c-list-contradictors c-list)
                                     (find-matching-c-lists-for (neg formula) (c-list-variables c-list)))
                            (dolist (cl (c-list-contradictors c-list))
                                (push (list c-list (reverse (mem2 cl)))
                                            (c-list-contradictors (mem1 cl)))))))
       (setf (node-c-list node) c-list)))

#| Test is the final member of the formula-profile for the node-formula. |#
(defunction store-inference-node-at-new-d-node (node term-list d-node test)
    (let* ((c-variables (node-variables node))
              (dn (make-d-node
                       :d-node-number (incf *d-node-number*)
                       :d-node-description (cons test (d-node-description d-node))
                       :parent-d-node d-node))
              (formula (node-formula node))
              (c-list (make-c-list
                          :c-list-formula formula
                          :c-list-nodes (list node)
                          :reductio-interests
                          (appropriate-for-reductio-interest formula)
                          :c-list-variables c-variables
                          :c-list-term-list term-list
                          :c-list-d-node dn
                          )))
       (push dn *discrimination-net*)
       (push (cons test dn) (discrimination-tests d-node))
       (setf (d-node-c-lists dn) (list c-list))
       (when
            (appropriate-for-contradictors formula)
            (setf (c-list-contradictors c-list)
                     (find-matching-c-lists-for (neg formula) (c-list-variables c-list)))
            (dolist (cl (c-list-contradictors c-list))
                (push (list c-list (reverse (mem2 cl)))
                            (c-list-contradictors (mem1 cl)))))
       (setf (node-c-list node) c-list)))

(defunction find-matching-c-lists-for (formula variables)
    (multiple-value-bind (profile term-list) (formula-code formula)
         (pursue-c-lists-for formula profile term-list variables *top-d-node*)))
    
(defunction pursue-c-lists-for (formula profile term-list variables d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-c-lists-for formula new-profile term-list variables dn))
                 (t (matching-c-lists-for term-list variables dn)))))))

(defunction index-inference-node-at-new-nodes (node term-list d-node profile test)
    (let ((dn (make-d-node
                     :d-node-number (incf *d-node-number*)
                     :d-node-description (cons test (d-node-description d-node))
                     :parent-d-node d-node)))
       (push (cons test dn) (discrimination-tests d-node))
       (push dn *discrimination-net*)
       (let ((desc (cdr profile)))
          (cond (desc (index-inference-node-at-new-nodes node term-list dn desc (car profile)))
                      (t (store-inference-node-at-new-d-node node term-list dn (car profile)))))))

(defunction d-node-for (formula)
    (let ((profile (formula-code formula)))
         (pursue-d-node-for profile *top-d-node*)))

(defunction c-list-for (formula)
    (let ((d-node (d-node-for formula)))
       (if d-node
          (fetch-c-list-for formula d-node))))

(defunction pursue-c-list-for (formula profile d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-c-list-for formula new-profile dn))
                 (t (fetch-c-list-for formula dn)))))))

(defunction store-inference-node-with-c-list (node formula c-list)
    ; (when (equal *inference-number* 31) (setf c node f formula cl c-list) (break))
    ;; (step (store-inference-node-with-c-list c f cl))
    (cond (c-list
                 (push node (c-list-nodes c-list))
                 (setf (node-c-list node) c-list))
                (t (store-inference-node node formula))))

(defunction appropriate-for-reductio-interest (formula)
    (and
      (not (conjunctionp formula))
      (not (disjunctionp formula))   ;; if we use disj-simp
      (not (biconditionalp formula))
      (or (not (conditionalp formula))                                         ;; these assume:
            (and (not (conjunctionp (antecedent formula)))       ;; exportation
                      (not (disjunctionp (antecedent formula)))        ;; disj-antecedent-simp
                      (not (conditionalp (antecedent formula)))))     ;; cond-antecedent-simp
      (not (u-genp formula))
      (not (e-genp formula))
      (or (not (negationp formula))
            (atomic-formula (negand formula))
            (undercutterp (negand formula)))))

(defunction appropriate-for-contradictors (formula)
    (and
      (not (conjunctionp formula))
      (not (disjunctionp formula))   ;; if we use disj-simp
      (not (biconditionalp formula))
      (not (u-genp formula))
      (not (e-genp formula))
      (or (not (negationp formula))
            (atomic-formula (mem2 formula))
            (undercutterp (mem2 formula))
            (conditionalp (mem2 formula)))))

(defunction cancelled-c-list-for (formula)
    (e-assoc formula *cancelled-c-lists*))

(defunction store-processed-inference-node (node)
    (setf (processed? node) T)
    (push node (c-list-processed-nodes (node-c-list node))))

#| This finds the interest with interest-number n. |#
(defunction interest (n)
    (find-if #'(lambda (i) (eql (interest-number i) n)) *interests*))

#| This returns the degree of interest for either an interest or a query. |#
(defunction degree-of-interest* (n)
    (if (interest-p n) (degree-of-interest n) (query-strength n)))

(defunction interest-sequent* (n)
    (if (interest-p n) (interest-sequent n) (list nil (query-formula n))))

(defunction display-interest (interest)
    (if (numberp interest) (setf interest (interest interest)))
    (princ "                                        # ") (princ (interest-number interest)) (princ "  ")
    (when (deductive-interest interest) (princ "deductive "))
    (when (reductio-interest interest) (princ "reductio "))
    (princ "interest:")
    (terpri)
    (princ "                                           ") (prinp  (interest-formula interest))
    (when (interest-supposition interest)
         (princ "    supposition: ")
         (set-prinp (interest-supposition interest)))
    (terpri)
    (when
         (some #'(lambda (L) (query-p (resultant-interest L)))
                     (right-links interest))
         (princ "                                        This is of ultimate interest") (terpri))
    (let ((L (lastmember (right-links interest))))
      (when (and L (not (query-p (resultant-interest L))))
           (princ "                                        For ")
           (when (reductio-interest (resultant-interest L)) (princ "reductio "))
           (princ "interest ")
           (princ (interest-number (resultant-interest L)))
           (princ " by ") (princ (link-rule L))
           (let ((nodes (supporting-nodes L)))
             (when nodes
                  (cond ((equal (length nodes) 1)
                              (princ " using node ")
                              (princ (inference-number (mem1 nodes))))
                            (t
                              (princ " using nodes ")
                              (print-list (mapcar
                                                #'(lambda (conclusion)
                                                      (inference-number conclusion))
                                                nodes) 40)))))
           (let ((nodes (link-clues L)))
             (when nodes
                  (cond ((equal (length nodes) 1)
                              (princ " with clue ")
                              (princ (inference-number (mem1 nodes))))
                            (t
                              (princ " with clues ")
                              (print-list (mapcar
                                                #'(lambda (conclusion)
                                                      (inference-number conclusion))
                                                nodes) 40)))))
           (terpri))
      (when (discharge-condition interest)
           (princ "                                        Discharge condition: ") (terpri)
           (princ "                                             ")
           (display-discharge-condition interest L) (terpri)))
    (terpri))

(defunction display-discharge-condition (interest link)
    (let ((binding
              (mapcar
                #'(lambda (x) (cons (car x) (if (and (cdr x) (listp (cdr x))) (list 'quote (cdr x)) (cdr x))))
                (link-binding link))))
      (print-pretty  (sublis binding (text-discharge-condition interest)))))

(defunction display-interests ()
    (princ "(") (terpri)
    (princ "================== INTERESTS ===================")
    (terpri)
    (let* ((**interests**
                (unionmapcar
                  #'(lambda (dn)
                        (unionmapcar #'(lambda (il) (i-list-interests il)) (d-node-i-lists dn)))
                  *discrimination-net*))
              (interests
                (order **interests**
                           #'(lambda (c1 c2)
                                 (< (interest-number c1) (interest-number c2))))))
      (dolist (interest interests)
          (princ "#") (princ (interest-number interest))
          (cond ((deductive-interest interest) (princ "  deductive interest: "))
                    ((reductio-interest interest) (princ "  reductio interest: "))
                    (t (princ "  interest: ")))
          (prinp (interest-formula interest))
          (when (interest-supposition interest)
               (princ "    supposition: ")
               (set-prinp (interest-supposition interest)))
          (terpri)
          (when
               (some #'(lambda (L) (query-p (resultant-interest L)))
                           (right-links interest))
               (princ "     This is of ultimate interest") (terpri))
          (dolist (L (right-links interest))
              (when (not (query-p (resultant-interest L)))
                   (princ "     For ")
                   (when (reductio-interest (resultant-interest L)) (princ "reductio "))
                   (princ "interest ")
                   (princ (interest-number (resultant-interest L)))
                   (princ " by ") (princ (link-rule L))
                   (let ((nodes (supporting-nodes L)))
                     (when nodes
                          (cond ((equal (length nodes) 1)
                                      (princ " using node ")
                                      (princ (inference-number (mem1 nodes))))
                                    (t
                                      (princ " using nodes ")
                                      (print-list (mapcar
                                                        #'(lambda (conclusion)
                                                              (inference-number conclusion))
                                                        nodes) 40)))))
                   (let ((nodes (link-clues L)))
                     (when nodes
                          (cond ((equal (length nodes) 1)
                                      (princ " with clue ")
                                      (princ (inference-number (mem1 nodes))))
                                    (t
                                      (princ " with clues ")
                                      (print-list (mapcar
                                                        #'(lambda (conclusion)
                                                              (inference-number conclusion))
                                                        nodes) 40)))))
                   (terpri)))
          (when (interest-defeatees interest)
               (princ "     For the defeat of ")
               (print-list (mapcar #'inference-number (interest-defeatees interest)))
               (terpri))
          (princ "---------------------------------------------------") (terpri)))
    (princ ")") (terpri))

#| This builds chains of inference-ancestors. |#
(defunction interest-ancestor-chains (interest)
    (cond ((interest-p interest)
                 (let ((links (right-links interest)))
                    (cond ((null links) (list (list (list interest))))
                                (t 
                                  (unionmapcar
                                    #'(lambda (L)
                                          (mapcar
                                            #'(lambda (c)
                                                  (cons (list interest L) c))
                                            (interest-ancestor-chains (resultant-interest L))))
                                    links)))))
                (t (list nil))))

#| This is like interest-ancestor-chains, but leaves out the links. |#
(defunction right-branches (interest)
    (if (interest-p interest)
       (let ((links (right-links interest)))
          (cond ((null links) (list (list interest)))
                      (t 
                        (unionmapcar
                          #'(lambda (L)
                                (mapcar
                                  #'(lambda (c)
                                        (cons interest c))
                                  (right-branches (resultant-interest L))))
                           links))))))

(defunction good-interest-ancestor-chains (interest)
    (if (interest-p interest)
       (let ((links (right-links interest)))
          (cond ((null links) (list (list (list interest))))
                      (t 
                        (let ((i-list (interest-i-list interest)))
                        (unionmapcar
                          #'(lambda (L)
                                (remove nil
                                (mapcar
                                  #'(lambda (c)
                                        (when
                                             (and 
                                               (not 
                                                 (and 
                                                   (equal (link-rule L) reductio)
                                                   (or
                                                     (and
                                                       (mem2 (mem1 c))
                                                       (equal (link-rule (mem2 (mem1 c))) reductio))
                                                     (some #'(lambda (x)
                                                                       (and (mem2 x)
                                                                                 (equal (link-rule (mem2 x)) reductio)
                                                                                 (equal (interest-i-list (mem1 x))
                                                                                              i-list)))
                                                                  c)))))
                                             (cons (list interest L) c)))
                                  (good-interest-ancestor-chains (resultant-interest L)))))
                           links)))))))

;(defun display-good-interest-map ()
;    (terpri)
;    (let ((endpoints nil))
;       (dolist (i-list *interests*)
;           (dolist (interest (i-list-interests (cdr i-list)))
;               (when (null (left-links interest))
;                    (push interest endpoints))))
;       (princ "Endpoints of interest map: ")
;       (print-list (mapcar #'interest-number endpoints) 40) (terpri)
;      ; (setf *endpoints* endpoints)
;       (setf *interest-map* nil)
;       (dolist (i endpoints)
;           (princ "==============") (terpri)
;           (let ((chains (good-interest-ancestor-chains i)))
;              (cond (chains
;                           (princ "Chains for ") (princ i) (terpri)
;                           (dolist (c chains)
;                               (push c *interest-map*)
;                               (display-interest-ancestor-chain c)))
;                          (t (princ "No chains for ") (princ i) (terpri))))))
;    (princ "==============") (terpri) (terpri))
;
;(defun circular-chain (c)
;    (some #'(lambda (x)
;                        (some #'(lambda (y)
;                                            (equal (interest-i-list (mem1 x)) (interest-i-list (mem1 y))))
;                                      (cdr (mem x c))))
;                  c))
;
;(defun nested-reductio (c)
;    (some #'(lambda (x)
;                        (and
;                          (mem2 x)
;                          (equal (link-rule (mem2 x)) reductio)
;                          (let ((y (mem2 (car (cdr (mem x c))))))
;                             (and y (equal (link-rule y) reductio)))))
;                  c))
;
;(defun display-interest-ancestor-chain (c)
;    (dolist (n c)
;        (print-sequent (interest-sequent (mem1 n)))
;        (when (mem2 n)
;             (princ " <=") (princ (link-number (mem2 n))) (princ "= ")))
;    (terpri))
;
;(defun display-interest-ancestor-chains (n)
;    (dolist (c (interest-ancestor-chains (interest n)))
;        (display-interest-ancestor-chain c)))
;
;#| This builds chains of interests derived from interest. |#
;(defunction interest-chains (interest)
;    (if (interest-p interest)
;       (let ((links (left-links interest)))
;          (cond ((null links) (list (list (interest-number interest))))
;                      (t (mapcar #'(lambda (c) (cons (interest-number interest) c))
;                                          (unionmapcar=
;                                            #'(lambda (L) (interest-chains (link-interest L)))
;                                            links)))))))
;
;(defun display-interest-chain (c)
;    (print-sequent (interest-sequent (interest (mem1 c))))
;    (dolist (n (cdr c))
;        (princ " => ") (print-sequent (interest-sequent (interest n))))
;    (terpri))
;
;(defun interest-map ()
;    (let ((endpoints nil))
;                     (dolist (i-list *interests*)
;                         (dolist (interest (i-list-interests (cdr i-list)))
;                             (when (null (right-links interest))
;                                  (push interest endpoints))))
;       (unionmapcar #'interest-chains endpoints)))
;
;(defun display-interest-map (&optional n)
;    (terpri)
;    (let ((endpoints nil))
;       (cond (n (setf endpoints (list (interest n))))
;                   (t
;                     (dolist (i-list *interests*)
;                         (dolist (interest (i-list-interests (cdr i-list)))
;                             (when (null (right-links interest))
;                                  (push interest endpoints))))))
;       (cond ((null n)
;                    (princ "Endpoints of interest map: ")
;                    (print-list (mapcar #'interest-number endpoints) 40) (terpri))
;                   (t (princ "Interest-chains for interest #") (princ n) (terpri)))
;       (setf *interest-map* nil)
;       (dolist (i endpoints)
;           (princ "==============") (terpri)
;           (dolist (c (interest-chains i))
;               (push c *interest-map*)
;              ; (display-interest-chain c)
;               )))
;    (princ "==============") (terpri)
;    (terpri))

(defun derived-interests (interest)
    (mapcar #'link-interest (left-links interest)))

(defun print-sequent (S)
    (prinp (sequent-formula S)) (princ "/") (set-prinp (sequent-supposition S)))

(defunction display-interests-by-supposition ()
    (princ "(") (terpri)
    (let ((suppositions nil))
       (dolist (dn *discrimination-net*)
           (dolist (il (d-node-i-lists dn))
               (dolist (c (i-list-interests il))
                   (pushnew (interest-supposition c) suppositions :test '==)
                   (setf suppositions
                            (order suppositions
                                        #'(lambda (s1 s2)
                                              (or (< (length s1) (length s2))
                                                    (and (= (length s1) (length s2))
                                                              (lessp s1 s2)))))))))
       (let* ((**interests**
                  (unionmapcar
                    #'(lambda (dn)
                          (unionmapcar #'(lambda (il) (i-list-interests il)) (d-node-i-lists dn)))
                    *discrimination-net*)))
          (dolist (sup suppositions)
              (princ "==========================================") (terpri)
              (princ "Interests with supposition ") (set-prinp sup) (princ ":") (terpri)
              (let* ((sup-interests
                         (subset #'(lambda (c) (== (interest-supposition c) sup))
                                        **interests**))
                        (interests
                          (order sup-interests
                                      #'(lambda (c1 c2)
                                            (< (interest-number c1) (interest-number c2))))))
                 (dolist (c interests)
                     (when (== (interest-supposition c) sup)
                          (princ "    #") (princ (interest-number c)) (princ "  ")
                          (prinp (interest-formula c)) (princ "     ")
                          (when (reductio-interest c) (princ "reductio "))
                          (princ "for  ") 
                          (print-list
                            (remove-duplicates=
                              (mapcar
                                #'(lambda (L) (interest-number (resultant-interest L)))
                                (right-links c))) 40)
                          (terpri)))))))
    (princ ")") (terpri))

(defunction display-i-lists ()
    (princ "(") (terpri)
    (dolist (dn *discrimination-net*)
        (dolist (il (d-node-i-lists dn))
            (princ "==========================================") (terpri)
            (princ "i-list-formula: ") (prinp (i-list-formula il)) (terpri)
            (let ((interests
                      (order (i-list-interests il)
                                  #'(lambda (c1 c2)
                                        (let ((s1 (interest-supposition c1))
                                                (s2 (interest-supposition c2)))
                                           (or (< (length s1) (length s2))
                                                 (and (= (length s1) (length s2))
                                                           (lessp s1 s2))))))))
               (dolist (c interests)
                   (princ "    #") (princ (interest-number c)) (princ "  ")
                   (princ "   sup = ") (set-prinp (interest-supposition c)) (princ "     ")
                   (when (reductio-interest c) (princ "reductio "))
                   (princ "for  ") 
                   (print-list
                     (remove-duplicates=
                       (mapcar
                         #'(lambda (L) (interest-number (resultant-interest L)))
                         (right-links c))) 40)
                   (let ((derived-interests (derived-interests c)))
                      (when derived-interests
                           (princ "  generates ")
                           (print-list (mapcar #'interest-number derived-interests) 40)))
                   (terpri)))))
    (princ ")") (terpri))

; --------------------------------------  FORWARDS-REASONS -------------------------------------- 

#| This defines a generic structure whose slots are those used in common by both
backwards and forwards reasons.  If use-basis is nil, when a support-link is constructed, 
the basis is nil.  This is used by def-prob-rule. |#

(defstruct (reason (:print-function print-reason) (:conc-name nil))
    (reason-name nil)
    (reason-function nil)
    (reason-conclusions nil)
    (conclusions-function nil)
    (forwards-premises nil)
    (backwards-premises nil)
    (reason-variables nil)
    (defeasible-rule nil) 
    (reason-strength 1.0)
    (discount-factor 1.0)
    (reason-description nil)
    (reason-instantiated-premise nil)
    (backwards-premises-function nil)
    (temporal? nil)
    (undercutting-defeaters nil)
    (reason-defeatees)
    )

(defun print-reason (x stream depth)
    (declare (ignore depth)) (princ (reason-name x) stream))

;(defunction reason-strength+ (reason)
;    (if (stringp reason) 1.0 (reason-strength reason)))

(defunction reason (name)
    (let ((R (find-if #'(lambda (x) (equal (reason-name x) name)) *forwards-reasons*)))
       (when (null R)
            (setf R (find-if #'(lambda (x) (equal (reason-name x) name)) *backwards-reasons*)))
       R))

(defstruct (forwards-premise (:print-function print-f-premise) (:conc-name fp-))
    (formula nil)
    (kind :inference)
    (condition nil)
    (binding-function nil)
    (variables nil)
    (instantiator nil)
    (clue? nil)
    (node-specifier nil)  ;; bound to the node instantiating the premise in a link
    )

#| Condition1 is a predicate that an existing interest must satisfy to be used in
backwards reasoning as the left terminus of a link encoding this reason, and condition2
is a function which is applied to a new interest constructed for that purpose.
The application of this condition will normally be such as to set the values of slots
so that the resulting interest satisffies condition1. |#
(defstruct (backwards-premise (:print-function print-b-premise) (:conc-name bp-))
    (formula nil)
    (condition1 nil)
    (condition2 nil)
    (instantiator nil)
    (clue? nil)
    (text-condition nil)  ;; text specification of the discharge condition
    (node-specifier nil)  ;; bound to the node instantiating the premise in a link
    )

(defunction premise-node-specifier (premise)
    (cond ((backwards-premise-p premise) (bp-node-specifier premise))
              ((forwards-premise-p premise) (fp-node-specifier premise))))

(defunction print-f-premise (premise stream depth)
    (declare (ignore depth))
    (princ "#<premise: " stream)
    (prinp (fp-formula premise) stream)
    (princ ">" stream))

(defunction print-b-premise (premise stream depth)
    (declare (ignore depth))
    (princ "#<premise: " stream)
    (prinp (bp-formula premise) stream)
    (princ ">" stream))

(defunction clue? (premise)
    (cond ((forwards-premise-p premise) (fp-clue? premise))
              ((backwards-premise-p premise) (bp-clue? premise))))

(defunction construct-forwards-premise (P C V &optional B)
    (make-forwards-premise
      :formula P
      :condition C
      :binding-function B
      :variables V
      :instantiator (reason-instantiator P V)))

(defmacro cfp (P V &optional B) `(construct-forwards-premise ,P nil ,V ,B))

(defunction construct-backwards-premise (P C1 C2 V)
    (let ((V* (subset #'(lambda (x) (occur* x P)) V)))
      (make-backwards-premise
        :formula P
        :condition1 C1
        :condition2 C2
        :instantiator (reason-instantiator P V*))))

(defmacro cbp (P C1 C2 V) `(construct-backwards-premise ,P ,C1 ,C2 ,V))

(defstruct (forwards-reason (:include reason) (:print-function print-reason)
                                                       (:conc-name nil)))

(defun is-inference (c &rest r) (declare (ignore r)) (eq (node-kind c) :inference))

(defun is-desire (c &rest r) (declare (ignore r)) (eq (node-kind c) :desire))

(defun is-percept (c &rest r) (declare (ignore r)) (eq (node-kind c) :percept))

(setf is-inference #'is-inference)

(setf is-desire #'is-desire)

(setf is-percept #'is-percept)

#| This produces a match equivalent to applying m1 first and then m2. |#
(defunction merge-matches* (m1 m2)
    (cond ((null m1) m2)
                ((null m2) m1)
                ((eq m1 t) m2)
                ((eq m2 t) m1)
                (t
                  (let* ((m1* (mapcar #'(lambda (x) (cons (car x) (match-sublis m2 (cdr x)))) m1))
                            (domain (domain m1*))
                            (m2* (subset #'(lambda (x) (not (member (car x) domain))) m2)))
                     (append m1* m2*)))))

; --------------------------------------  BACKWARDS-REASONS -------------------------------------- 

(defstruct (backwards-reason (:include reason) (:print-function print-reason)
                                                           (:conc-name nil))
   (reason-condition nil)  ;; this is a predicate applied to the binding
   (reason-discharge nil)
   (reason-length 1)  ;; this is the number of backwards-premises
   (conclusions-binding-function nil)
   (conclusion-variables nil)
   (immediate-reason nil))

#| This can be blocked by a prior reductio-supposition, but this then converts it so that it is
no longer deductive-only.  Any node-descendants not inferred from other deductive-only
nodes are made not deductive-only, and all defeasible forwards-rules are applied to them. |#
(defunction queue-supposition (supposition instance-supposition e-vars discount-factor interest)
    ; (when (eq interest (interest 36)) (setf s supposition i instance-supposition e e-vars d discount-factor in interest) (break))
    ;; (step (queue-supposition s i e d in))
    (let ((sup (find-if #'(lambda (N) (equal (node-formula N) supposition))
                        *non-reductio-supposition-nodes*)))
     (cond (sup
              (incf (readopted-supposition sup))
              (push interest (generating-interests sup))
              (push sup (generated-suppositions interest))
              (when (and (deductive-only sup) (not (deductive-interest interest)))
                  (let ((nodes (convert-from-deductive-only sup)))
                    (dolist (C nodes)
                       (apply-forwards-defeasible-reasons C))))
              (values sup nil))
             (t
              (setf sup (subsuming-supposition supposition))  ;; an inference-node
              (cond ((null sup)
                       (queue-non-reductio-supposition
                        supposition instance-supposition e-vars discount-factor interest))
                      ((reductio-supposition sup)
                       (incf (readopted-supposition sup))
                       (push interest (generating-interests sup))
                       (convert-reductio-supposition sup discount-factor)
                       (values sup t)))))))

(defunction queue-non-reductio-supposition
    (supposition instance-supposition e-vars discount-factor interest)
    (let* ((sequent (list instance-supposition supposition))
              (deductive-only (deductive-interest interest)))
       (when (skolem-free supposition) (push supposition *skolem-free-suppositions*))
       (let* ((complexity 
                   (max 1 (* 2 (formula-complexity supposition))))
                 (priority (* discount-factor (interest-priority interest)))
                 (node
                   (make-inference-node
                     :inference-number (incf *inference-number*)
                     :node-sequent sequent
                     :node-formula supposition
                     :node-supposition instance-supposition
                     :node-kind :inference
                     :nearest-defeasible-ancestors (list nil)
                     :node-justification :supposition
                     :maximal-degree-of-support 1.0
                     :undefeated-degree-of-support 1.0
                     :discounted-node-strength priority
                     :deductive-only deductive-only
                     :node-variables e-vars
                     :node-supposition-variables e-vars
                     :node-discount-factor discount-factor
                     :generating-interests (list interest)
                     :non-reductio-supposition? t))
                 (queue-node
                   (make-inference-queue-node
                     :queue-number (incf *queue-number*)
                     :enqued-item node
                     :item-kind :conclusion
                     :discounted-strength priority
                     :item-complexity complexity
                     :degree-of-preference (/ discount-factor complexity))))
          (setf (non-reductio-supposition node) (list (cons (mem1 instance-supposition) node)))
          (setf (node-queue-node node) queue-node)
          (store-inference-node node (sequent-formula sequent))
          (push node (generated-suppositions interest))
          (push node *inference-graph*)
          (push node *non-reductio-supposition-nodes*)
          (if *log-on* (push node *reasoning-log*))
          (when (not *deductive-only*)
               (setf (node-UDs *assignment-tree*) (cons (cons node 1.0) (node-UDs *assignment-tree*)))
               (setf (node-MPUDs *assignment-tree*) (cons (cons node 1.0) (node-MPUDs *assignment-tree*))))
          (when *display?* (display-unsupported-node node))
          (discharge-interest-in node (corresponding-i-lists (node-c-list node)) nil t 1 nil)
          (setf *inference-queue* (ordered-insert queue-node *inference-queue* #'i-preferred))
          (when (and *display?* *graphics-on*)
               (when *graphics-pause* (pause-graphics))
               (draw-n node *og* *nodes-displayed*) (push node *nodes-displayed*))
          (values node t))))

#| This converts the supporting-nodes of node and its descendants to non-deductive-only
provided they are not inferred from other deductive-only conclusions.  It returns the list of
converted nodes. |#
(defunction convert-from-deductive-only (node)
    (setf (deductive-only node) nil)
    (let ((nodes (list node)))
       (dolist (L (consequent-links node))
           (let ((N (support-link-target L)))
              (when
                   (and (deductive-only N)
                             (not (some
                                       #'(lambda (L)
                                             (some
                                               #'(lambda (b) (deductive-only b))
                                               (support-link-basis L)))
                                       (support-links N))))
                   (setf nodes
                            (union nodes (convert-from-deductive-only N))))))
       nodes))

(defunction subsuming-supposition (supposition)
    (let* ((sup
              (find-if
                #'(lambda (N)
                      (let* ((P (node-formula N))
                                (f-vars (node-variables N))
                                (m (match P supposition f-vars)))
                         (and m (equal supposition (match-sublis m P)))))
                *non-reductio-supposition-nodes*)))
       (when (null sup)
            (setf sup
                     (find-if
                       #'(lambda (N)
                             (let* ((P (node-formula N))
                                       (f-vars (node-variables N))
                                       (m (match P supposition f-vars)))
                                (and m (equal supposition (match-sublis m P)))))
                       *reductio-supposition-nodes*)))
       sup))

; --------------------------------------  THE INFERENCE-QUEUE -------------------------------------- 

(defstruct (inference-queue-node (:print-function print-inference-queue-node)
                                                                (:conc-name nil))
   (queue-number 0)
   (enqued-item nil)  ;; either an interest or a conclusion or a query
   (item-kind nil)   ;; this will be :conclusion, :interest, or :query
   (item-complexity 0)
   (discounted-strength 0)
   (degree-of-preference 0))

(defun print-inference-queue-node (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Item " stream)
    (princ (queue-number x) stream) (princ ">" stream))

#| *inference-queue* is ordered by i-preference: |#
(defunction i-preferred (node1 node2)
    (> (degree-of-preference node1) (degree-of-preference node2)))

(defunction complexity (x)
    (cond ((null X) 0)
              ((stringp x) 1)
              ((atom x) 1)
              ((listp x) 
                (cond ((skolem-function (car x))
                            (cond ((null (cdr x)) 1)
                                      ((and (not (listp (cadr x))) (not (eq (cadr x) '=)))
                                        *skolem-multiplier*)
                                      ((and (listp (cadr x)) (skolem-function (caar (cdr x))))
                                        (* *skolem-multiplier* (1+ (complexity (cdr x)))))
                                      (t (apply #'+ (mapcar #'complexity x)))))
                          ;; the following handles functions that occur within their own scopes
                          ((and (not (null (cdr x)))
                                    (symbolp (car x))
                                    (not (member (mem1 x) *logical-constants*))
                                    (occur (car x) (cdr x)))
                            (* *skolem-multiplier* (1+ (complexity (cdr x)))))
                          ((or (u-genp x) (e-genp x)) (* *quantifier-discount* (complexity (q-matrix x))))
                          ((consp (cdr x)) (apply #'+ (mapcar #'complexity x)))
                          (t (+ (complexity (car x)) (complexity (cdr x))))))))

(defunction formula-complexity (formula)
    (cond ((mem formula *skolem-free-suppositions*) 0)
                (t (complexity formula))))

(defunction sequent-complexity (sequent)
    (let* ((sup (sequent-supposition sequent))
            (formula (sequent-formula sequent))
            (complexity
              (cond (sup
                          (+ (max 1 (formula-complexity formula))
                               (apply
                                 '+ (mapcar
                                      #'(lambda (P)
                                            (cond ((mem P *skolem-free-suppositions*) 0)
                                                      (t (complexity P))))
                                      sup))))
                        (t (max 1 (formula-complexity formula))))))
      ;  (when *display?*
      ;       (princ "The complexity of ") (print-sequent sequent) (princ " is ") (princ complexity) (terpri))
      complexity))

#|
(defunction sequent-complexity (sequent)
    (let ((sup (sequent-supposition sequent))
            (formula (sequent-formula sequent))
            (length 0))
       (let ((complexity
                 (cond (sup
                              (+ (max 1 (formula-complexity formula))
                                   (apply
                                     '+ (mapcar
                                           #'(lambda (P)
                                                 (cond ((mem P *skolem-free-suppositions*) 0)
                                                             (t (incf length) (complexity P))))
                                           sup))))
                             (t (max 1 (formula-complexity formula))))))
          ;  (when *display?*
          ;       (princ "The complexity of ") (print-sequent sequent) (princ " is ") (princ complexity) (terpri))
          (if (> length 2) (* complexity (expt 10 (* length length))) complexity))))
|#

#| This is the default computation of degree-of-preference for premises.  Premises
are triples consisting of a formula, a supposition, and a degree-of-support.
Premises are queued for immediate retrieval. |#
(defunction premise-preference (premise)
    (/ (mem2 premise) (complexity (mem1 premise))))

(defstruct (goal (:print-function print-goal) (:conc-name nil))
    (goal-number 0)
    (goal-formula nil)
    (goal-strength 1)
    (supporting-goal-node nil)  ;; the node supporting this as a suitable goal
    (goal-generating-desire nil)  ;; the desire, if there is on, that generates the goal
    (plans-for nil)  ;; the list of candidate plans that aim at the satisfaction of this goal
    (user-question-asked? nil))

(defunction print-goal (goal stream depth)
    (declare (ignore depth))
    (princ "#<goal: " stream)
    (princ (pretty (goal-formula goal)) stream)
    (princ ">" stream))

(defstruct (desire (:print-function print-desire) (:conc-name nil))
    (desire-number 0)
    (desire-content nil)
    (desire-object nil)  ;; the object of a desire will be a goal
    (desire-strength 0)
    (generated-plans nil)
    (desire-generating-interest nil)  ;; for epistemic-desires
    (desire-inference-node nil))  ;; the inference-node recording the desire

(defunction print-desire (desire stream depth)
    (declare (ignore depth))
    (princ "#<desire: " stream)
    (princ (pretty (desire-content desire)) stream)
    (princ ">" stream))

(defunction goal-generating-interest (goal)
    (let ((desire (goal-generating-desire goal)))
       (when desire (desire-generating-interest desire))))

(defstruct (percept (:print-function print-percept) (:conc-name nil))
    (percept-number 0)
    (percept-content nil)
    (percept-clarity 0)
    (percept-date 0))

(defunction print-percept (percept stream depth)
    (declare (ignore depth))
    (princ "#<percept: " stream)
    (princ (pretty (percept-content percept)) stream)
    (princ ">" stream))

#| This is the default computation of degree-of-preference for desires. |#
(defunction desire-preference (desire)
    (/ (desire-strength desire) (complexity (desire-content desire))))

#| This is the default computation of degree-of-preference for percepts. |#
(defunction percept-preference (percept)
    (/ (percept-clarity percept) (complexity (percept-content percept))))

(defunction discharged? (interest degree)
    (let ((discharged-degree (discharged-degree interest)))
       (and discharged-degree
                 (>= discharged-degree degree))))

#| The following is the default computation of interest-priority for defeaters. |#
(defunction defeater-priority (interest)
    (declare (ignore interest))
    *base-priority*)

#| The following is the default computation of the degree-of-preference for queries. |#
(defunction query-preference (query)
    (let ((complexity (complexity (query-formula query)))
            (strength
              (cond ((member query *permanent-ultimate-epistemic-interests*)
                           (query-strength query))
                          ((answered? query)
                            (* (query-strength query) *answered-discount*))
                          (t (query-strength query)))))
       (/ strength complexity)))

#| This is the default computation of degree-of-preference for an interest, where
priority is the interest-priority and complexity is the complexity of the interest-sequent. |#
(defunction interest-preference (priority complexity)
    (if (zerop complexity) priority (/ priority complexity)))

#| This reverses the default computation of degree-of-preference to compute priority
from preference. |#
(defunction retrieved-interest-priority (preference complexity)
    (* complexity preference))

(defunction interest-link-priority (link interest-priority interest)
    (if (or (link-defeat-status link)
               (let ((rn (resultant-interest link)))
                  (discharged? rn (maximum-degree-of-interest rn)))
               (and interest (discharged? interest (maximum-degree-of-interest interest))))
       *base-priority*
       interest-priority))

#| The following is the default computation of interest-priority for an interest on
the inference-queue that is concluded. |#
(defunction concluded-interest-priority (Q)
    (declare (ignore Q))
    *concluded-interest-priority*)

#| This must recompute reductio-ancestors, non-reductio-suppositions, deductive-only-status,
and apply forwards defeasible reasons. |#
(defunction convert-reductio-supposition (sup discount-factor)
    (setf (reductio-ancestors sup) (list (cons (node-formula sup) sup)))
   ; (setf (non-reductio-supposition sup) nil)
    (setf (non-reductio-supposition? sup) t)
    (let ((Q (node-queue-node sup)))
       (when Q
            (setf (degree-of-preference Q) (* discount-factor (/ 1 (item-complexity Q))))
            (setf *inference-queue*
                     (ordered-insert Q (remove Q *inference-queue*) #'i-preferred))))
    (let ((nodes
              (convert-from-deductive-only sup)))
       (dolist (C nodes)
           (when (deductive-in C sup)
                (let ((nr (find-if #'(lambda (x) (equal (cdr x) sup)) (non-reductio-supposition C))))
                   (when nr
                        (pull nr (non-reductio-supposition C))
                        (push nr (reductio-ancestors C))))))
       (dolist (C nodes)
           (apply-forwards-defeasible-reasons C))))

;======================================================
;------------------------------------------- REASONING ---------------------------------------

#| The following turn various displays on and off. |#
(defunction trace-on () (setf *display?* t) (setf *trace* t))
(defunction trace-off () (setf *trace* nil *start-trace* nil))
(defunction trace-from (n) (setf *start-trace* n *display?* nil *trace* nil))
(defun display-on () (setf *display?* t))
(defun display-off () (setf *display?* nil *trace* nil *start-trace* nil *start-display* nil))
(defun display-from (n) (setf *display?* nil *trace* nil *start-trace* nil *start-display* n))
(defun proof-on () (setf *proofs?* t))
(defun proof-off () (setf *proofs?* nil))
(defun logic-on () (setf *use-logic* t) (setf *use-reductio* t))
(defun logic-off () (setf *use-logic* nil) (setf *use-reductio* nil))
(defun reductio-on () (setf *use-reductio* t) (setf *use-logic* t))
(defun reductio-off () (setf *use-reductio* nil))
(defun log-on () (setf *log-on* t))
(defun log-off () (setf *log-on* nil))
(defun IQ-on () (setf *display-inference-queue* t))
(defun IQ-off () (setf *display-inference-queue* nil))
(defunction graph-log-on ()
    (setf *graph-log* t))
(defunction graph-log-off ()
    (setf *graph-log* nil))

#| When graphics-pause is on, the reasoning-display pauses after printing the node display 
and before graphing the node, and waits for a character (preferably a space) to be typed
in the Listener. |#
(defunction graphics-pause-on ()
    (setf *graphics-pause* t))
(defunction graphics-pause-off ()
    (setf *graphics-pause* nil))

#| The following does not perform the operations in parallel as it should, because
this program is designed to run in serial LISP.  The functions update-environmental-
input and update-percepts are extrinsic to the reasoner,
and are supplied by the operating environment of the reasoner.
Optative dispositions are functions from inputs to desires.  This code allows
us to have premises supplied artificially rather than by perception.
Premises are triples (formula, supposition, degree-of-justification).
Premises can be defeated by rebutting defeaters, but there is no way
to have an undercutting defeater.  |#
(defunction OSCAR ()
    (initialize-reasoner)
   (dolist (query *ultimate-epistemic-interests*)
      (reason-backwards-from-query query (query-strength query) 0))
    (setf *cycle* 0)
    (loop
      (update-environmental-input)
      (update-percepts)
      (dolist (input *environmental-input*)
          (dolist (disposition *optative-dispositions*)
              (pull input *environmental-input*)
              (queue-desire (funcall disposition input))))
      (dolist (percept *percepts*)
          (pull percept *percepts*)
          (queue-percept percept))
     (dolist (premise *premises*)
        (when (eql (mem3 premise) *cycle*)
            (pull premise *premises*)
            (queue-premise (list (mem1 premise) nil (mem2 premise)))))
       (think)
       (initiate-actions)
       (incf *cycle*)))

(defun initialize-reasoner ()
    (setf *new-links* nil)
    (setf *inference-graph* nil)
    (setf *processed-desires* nil)
    (setf *desires* nil)
    (setf *percepts* nil)
    (setf *interest-links* nil)
    (setf *inference-queue* nil)
    (setf *support-links* nil)
    (setf *interests* nil)
    (setf *interest-schemes* nil)
    (setf *reductio-supposition-nodes* nil)
    (setf *non-reductio-supposition-nodes* nil)
    (setf *altered-nodes* nil)
    (setf *reasoning-log* nil)
    (setf *direct-reductio-interests* nil)
    (setf *assignment-tree* (make-assignment-tree))
    (setf *Q&I-modules* nil)
    (setf *inherited-non-reductio-suppositions* nil)
    (setf *skolem-free-suppositions* nil)
    (setf *constructed-plans* nil)
    (setf *constructed-goals* nil)
    (setf *constructed-desires* nil)
    (setf pause-flag nil)
    (setf *cycle* 0)
    (setf *inference-number* 0)
    (setf *support-link-number* 0)
    (setf *interest-number* 0)
    (setf *interest-scheme-number* 0)
    (setf *queue-number* 0)
    (setf *link-number* 0)
    (setf *tree-number* 1)
    (setf *triangle-number* 0)
    (setf *unused-suppositions* 0)
    (setf *gensym-counter* 0)
    (setf *ip-number* 0)
    (setf *is-number* 0)
    (setf *plan-number* 0)
    (setf *goal-number* 0)
    (setf *executable-operations* nil)
    (setf *deleted-arguments* nil)
    (setf *forwards-reasons*
             (if *use-logic*
               (append *forwards-logical-reasons* *forwards-substantive-reasons*)
               *forwards-substantive-reasons*))
    (setf *backwards-reasons*
             (if *use-logic*
               (append *backwards-logical-reasons* *backwards-substantive-reasons*)
               *backwards-substantive-reasons*))
    (initialize-discrimination-net)
    (when (and *display?* *graphics-on*) (make-oscar-window))
    (setf *query-number* (length *fixed-ultimate-epistemic-interests*))
    (dolist (query *fixed-ultimate-epistemic-interests*)
        (setf (answered? query) nil)
        (setf (query-answers query) nil)
        (setf (query-interest query) nil)
        (setf (negative-query-interest query) nil)
        (setf (query-queue-node query) nil))
    (dolist (premise *premises*)
        (when (null (mem3 premise)) (pull premise *premises*) (queue-premise premise)))
    (setf *ultimate-epistemic-interests* *fixed-ultimate-epistemic-interests*)
    (when (and *display?* *graphics-on*)
         (dolist (node (reverse *inference-graph*))
             (draw-n node *og* *nodes-displayed*) (push node *nodes-displayed*)))
   ; (dolist (query *ultimate-epistemic-interests*)
   ;     (reason-backwards-from-query query (query-strength query) 0))
    (if (not (boundp '*display?*)) (setf *display?* nil)))

(defunction initialize-discrimination-net ()
    (setf *top-d-node* (make-d-node :d-node-number (setf *d-node-number* 1)))
    (setf *conditional-node*
             (make-d-node :d-node-number (incf *d-node-number*) :parent-d-node *top-d-node*))
    (setf *undercutter-node*
             (make-d-node :d-node-number (incf *d-node-number*) :parent-d-node *top-d-node*))
    (setf *conjunctive-undercutter-node*
             (make-d-node :d-node-number (incf *d-node-number*) :parent-d-node *undercutter-node*))
    (setf (discrimination-tests *top-d-node*)
             (list (cons '((1) . ->) *conditional-node*)
                     (cons '((1) . @) *undercutter-node*)))
    (setf *discrimination-net*
             (list *top-d-node* *conditional-node* *undercutter-node* *conjunctive-undercutter-node*))
    (setf (discrimination-tests *undercutter-node*)
             (list (cons '((2 1) . &) *conjunctive-undercutter-node*)))
    (compute-forwards-reason-d-nodes)
    (compute-backwards-reason-d-nodes))

(defunction premise-code (P variables)
    (when P
         (setf *quantifier-number* 0)
         (multiple-value-bind (code term-list) (premise-code* P variables nil)
              (values (reverse code) term-list))))

(defunction premise-code* (P variables descriptor)
    (cond ((listp P)
                 (let ((description nil) (elt-num 1) (term-list nil))
                    (cond
                      ;; This handles notational variants.
                      ((or (eq (car p) 'all) (eq (car P) 'some))
                        (setf P
                                 (cons (car P) (subst (list 'q-var (incf *quantifier-number*)) (mem2 P) (cddr P)))))
                      ((and (symbolp (car P))
                                 (not (member (car P) *operators*))
                                 (not (member (car P) '(~ & v -> <-> all some ? @))))
                        (setf term-list (cdr P))
                        (setf P (list (car P)))))
                    (dolist (Q P)
                        (when (not (member Q variables))
                             (let ((Q-descriptor (cons elt-num descriptor)))
                                (cond ((not (listp Q))
                                             (when (not (member Q variables))
                                                  (push (cons (reverse Q-descriptor) Q) description)))
                                            (t 
                                              (multiple-value-bind (d tl) (premise-code* Q variables Q-descriptor)
                                                   (setf term-list (append tl term-list))
                                                   (setf description (append d description))
                                                   )))))
                        (incf elt-num))
                    (values description term-list)))
                ((not (member P variables)) (values (list (cons descriptor P)) nil))))

#| This is like premise-code, but it stops producing code when it comes to the first variable. |#
(defunction reason-code (P variables)
    (when P
         (setf *quantifier-number* 0)
         (reverse (reason-code* P variables nil))))

(defunction reason-code* (P variables descriptor)
    (cond ((listp P)
                 (let ((description nil) (elt-num 1) (stop nil))
                    (cond
                      ;; This handles notational variants.
                      ((or (eq (car p) 'all) (eq (car P) 'some))
                        (setf P
                                 (cons (car P) (subst (list 'q-var (incf *quantifier-number*)) (mem2 P) (cddr P)))))
                      ((and (symbolp (car P))
                                 (not (member (car P) *operators*))
                                 (not (member (car P) '(~ & v -> <-> all some ? @ at throughout))))
                        (setf P (list (car P)))))
                    (block stop-here
                        (dolist (Q P)
                            (cond
                              ((member Q variables)
                                (setf stop t)
                                (return-from stop-here))
                              (t
                                (let ((Q-descriptor (cons elt-num descriptor)))
                                   (cond ((not (listp Q))
                                                (push (cons (reverse Q-descriptor) Q) description))
                                               (t 
                                                 (multiple-value-bind (d st) (reason-code* Q variables Q-descriptor)
                                                      (setf description (append d description))
                                                      (when st (setf stop t) (return-from stop-here))))))))
                            (incf elt-num)))
                    (values description stop)))
                ((not (member P variables)) (values (list (cons descriptor P)) nil))))

(defunction compute-forwards-reason-d-nodes ()
    (dolist (reason *forwards-reasons*)
        (let* ((premise (mem1 (forwards-premises reason)))
                  (profile (reason-code (fp-formula premise) (fp-variables premise)))
                  (ip (store-forwards-reason reason premise profile)))
           (setf (reason-instantiated-premise reason) ip))))

#| This returns the ip at which the premise is stored. |#
(defunction store-forwards-reason (reason premise profile)
    (cond
      (profile (index-forwards-reason reason premise profile *top-d-node*))
      (t (store-forwards-reason-at-d-node reason premise *top-d-node*))))

(defunction store-forwards-reason-at-d-node (reason premise d-node)
    (let ((ip
              (make-instantiated-premise
                :reason reason
                :premise premise
                :remaining-premises (cdr (forwards-premises reason))
                :used-premise-variables (fp-variables premise)
                :d-node d-node
                :number (incf *ip-number*)
                :initial? t)))
       (push ip (d-node-forwards-reasons d-node))
       ip))

(defunction index-forwards-reason (reason premise profile d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node)))
            (new-profile (cdr profile)))
       (cond (dn
                    (cond
                      (new-profile (index-forwards-reason reason premise new-profile dn))
                      (t (store-forwards-reason-at-d-node reason premise dn))))
                   (new-profile
                     (index-forwards-reason-at-new-nodes
                       reason premise d-node new-profile (car profile)))
                   (t
                     (store-forwards-reason-at-new-d-node reason premise d-node (car profile))))))

#| Test is the final member of the formula-profile for the node-formula. |#
(defunction store-forwards-reason-at-new-d-node (reason premise d-node test)
    (let ((dn (make-d-node
                     :d-node-number (incf *d-node-number*)
                     :d-node-description (cons test (d-node-description d-node))
                     :parent-d-node d-node)))
       (push dn *discrimination-net*)
       (push (cons test dn) (discrimination-tests d-node))
       (store-forwards-reason-at-d-node reason premise dn)))

(defunction index-forwards-reason-at-new-nodes
    (reason premise d-node profile test)
    (let ((dn (make-d-node
                     :d-node-number (incf *d-node-number*)
                     :d-node-description (cons test (d-node-description d-node))
                     :parent-d-node d-node)))
       (push (cons test dn) (discrimination-tests d-node))
       (push dn *discrimination-net*)
       (let ((desc (cdr profile)))
          (cond (desc (index-forwards-reason-at-new-nodes reason premise dn desc (car profile)))
                      (t (store-forwards-reason-at-new-d-node reason premise dn (car profile)))))))

(defunction def-instantiator (def vars)
    (eval
      `#'(lambda (binding)
             (let* ((new-binding binding)
                       (new-vars nil)
                       ,@
                       (mapcar
                         #'(lambda (v)
                               `(,v
                                  (let ((v* (assoc ',v binding)))
                                    (cond
                                      (v* (cdr v*))
                                      (t
                                        (setf v* (make-interest-variable))
                                        (push v* new-vars)
                                        (push (cons ',v v*) new-binding)
                                        v*)))))
                         vars))
               (values ,def new-binding new-vars)))))

(defunction set-def-binding (def-instantiator var binding)
    (multiple-value-bind
         (val binding new-vars)
         (funcall def-instantiator binding)
         (values         
           (cons (cons var val) (remove (assoc var binding) binding :test 'equal))
           new-vars (cons (e-assoc var binding) val))))

#| This returns the instantiated-premise. |#
(defunction store-instantiated-premise
    (reason node c-list binding instantiations ip remaining-premises &optional profile)
    ; (setf r reason rp remaining-premises pr profile n node cl c-list b binding in instantiations i ip) ;(break)
    ;; (step (store-instantiated-premise r n cl b in i rp pr))
    (cond
      ((and (forwards-premise-p (car remaining-premises))
                (listp (fp-formula (car remaining-premises)))
                (equal (car (fp-formula (car remaining-premises))) 'define))
        (let* ((var (mem2 (fp-formula (car remaining-premises))))
                  (def-instantiator (fp-instantiator (car remaining-premises)))
                  (new-binding (set-def-binding def-instantiator var binding)))
          (cond ((cdr remaining-premises)
                      (when (funcall** (fp-condition (car remaining-premises)) nil new-binding)
                           (store-instantiated-premise
                             reason node c-list new-binding instantiations ip (cdr remaining-premises))))
                    ((funcall** (fp-condition (car remaining-premises)) nil new-binding)
                      (make-forwards-inference
                          new-binding instantiations
                          (if (clue? (ip-premise ip)) (ip-basis ip) (cons node (ip-basis ip)))
                          (if (clue? (ip-premise ip)) (cons node (ip-clues ip)) (ip-clues ip))
                          0 ip)))))
      (t
        (let ((premise (mem1 remaining-premises)))
          (when (null profile)
               (setf profile (reason-code (funcall (fp-instantiator premise) binding) (fp-variables premise))))
          (cond (profile
                      (index-instantiated-premise
                        reason premise profile node c-list binding instantiations
                        ip *top-d-node* (cdr remaining-premises)))
                    (t (store-instantiated-premise-at-d-node
                          reason premise node c-list binding instantiations
                          ip *top-d-node* (cdr remaining-premises))))))))

#| (mem3 premise) will be a function which, when applied to a formua, returns a binding.
(mem4 premise) will be the list of premise-variables occurring therein. |#
(defunction store-instantiated-premise-at-d-node
    (reason premise node c-list binding instantiations ip0 d-node remaining-premises)
    (when node (setf c-list (node-c-list node)))
    (let* ((ip
                (make-instantiated-premise
                  :reason reason
                  :number (incf *ip-number*)
                  :premise premise
                  :binding binding
                  :basis (if (and ip0 (not (fp-clue? (ip-premise ip0))))
                       (cons node (ip-basis ip0)))
                  :remaining-premises remaining-premises
                  :clues (when ip0
                                 (if (fp-clue? (ip-premise ip0)) (cons node (ip-clues ip0)