A Horn clause resolution theorem prover in Lisp

;;; A Horn-Clause Resolution Theorem Prover in Lisp:
;;; February 24th 2017 - March 16th 2017:   v. 1.0 -- initial release
;;;
;;; v. 1.01  March 18th 2017  -- remove state variable *goals* from show-proof, now functional
;;; ---
;;; [Update: (March 21st 2017): RTP release 1.1 is now available. See:
; http://interweave-consulting.blogspot.co.uk/2017/03/improved-resolution-theorem-prover-rtp.html
;;; ---
;;; Based on code from From Peter Norvig's book: Chapter 11
;;; "Paradigms of Artificial Intelligence Programming" - initially.
;;;
;;; Unification, Prolog, Resolution, inference control strategies
;;; generation of all proofs, extraction of proofs.
;;;
;;; Posted here:
;
; http://interweave-consulting.blogspot.co.uk/2017/03/a-horn-clause-resolution-theorem-prover.html
;;;
;;;  For documentation see here (you really need to read this first!):
;
; http://interweave-consulting.blogspot.co.uk/2017/03/description-theorem-prover-in-lisp.html
;;;
; (load  "C:\\Users\\HP Owner\\Google Drive\\Lisp\\Prog-RTP\\RTP.lisp")
;
;;; ----------------------------------------------------------------------
;;;
;;; Part 1: Unification
;;;
;;;  unify works on literals: eg (LIKES SALLY RENNER), (LIKES SALLY ?WHO)
;;;
;;;  --- Bindings: a list of dotted pairs created by unify: like this ---
;;;
;;;   ((?WHO . SALLY) (#:?X1113 . SALLY))

(defconstant +fail+ nil "Indicates unification failure")

(defconstant +no-bindings+ '((t . t))
"Indicates pat-match success but with no variables.")

(defun variable-p (x)    ; Symbol -> Bool
  "Is x a variable, a symbol beginning with '?'"
  (and (symbolp x) (equal (char (symbol-name x) 0) #\? )))

(defun get-binding (var bindings)
  "Find a (variable . value) pair in a binding list."
  (assoc var bindings))

(defun binding-val (binding)
  "Get the value part of a single binding."
  (cdr binding))

(defun lookup (var bindings)
  "Get the value part (for var) from a binding list."
  (binding-val (get-binding var bindings) ))

(defun extend-bindings (var val bindings)
  "Add a (var . value) pair to a binding list, remove (t . t)"
  (cons (cons var val) (if (equal bindings +no-bindings+) nil bindings)))

; --- Unification -------------------------------------------------------

(defparameter *occurs-check* t "Should we do the occurs check? If yes, t")

(defun unify (term-1 term-2 &optional (bindings +no-bindings+))
;  Lit x Lit -> Bindings
  "See if term-1 and term-2 match with given bindings"
  (cond ((equal bindings '+fail+) '+fail+)
        ((equal term-1 term-2) bindings)
        ((variable-p term-1) (unify-variable term-1 term-2 bindings))
        ((variable-p term-2) (unify-variable term-2 term-1 bindings))
        ((and (consp term-1) (consp term-2))
            (unify (rest term-1) (rest term-2)
                (unify (first term-1) (first term-2) bindings) ) )
        (t '+fail+) ) )

(defun unify-variable (var term bindings)     ; Var x Lit -> Bindings
  "Unify var with term, using (and maybe extending) bindings"
  (cond ((get-binding var bindings)
             (unify (lookup var bindings) term bindings))
        ((and (variable-p term) (get-binding term bindings))
             (unify var (lookup term bindings) bindings))
        ((and *occurs-check* (occurs-check var term bindings))
             '+fail+)
        (t (extend-bindings var term bindings))))

; > (unify '(likes sally renner) '(likes sally ?who)  +no-bindings+)
; ((?WHO . RENNER))

(defun occurs-check (var literal bindings)  ; Var x Lit -> Bool
  "Does var occur anywhere 'inside literal'? Returns t if it does (so fail)"
  (cond ((eq var literal) t)
        ((and (variable-p literal) (get-binding literal bindings))
         (occurs-check var (lookup literal bindings) bindings))
        ((consp literal) (or (occurs-check var (first literal) bindings)
                       (occurs-check var (rest literal) bindings)))
        (t nil)))

(defun unifier (literal literal-1)  ; ; Lit x Lit -> Lit
  "Return something that unifies with both literal and y (or +fail+)"
  (subst-bindings (unify literal literal-1) literal) )

(defun subst-bindings (bindings literal) ; Bindings x Lit ->Lit
  "Substitute the value of variables in bindings into literal,
taking recursively bound variables into account. Also works with clauses."
  (cond ((equal bindings '+fail+) '+fail+ )
        ((equal bindings +no-bindings+) literal)
        ((and (variable-p literal) (get-binding literal bindings))
              (subst-bindings bindings (lookup literal bindings) ))
        ((atom literal) literal)
        ( t (cons (subst-bindings bindings (car literal))
                        (subst-bindings bindings (cdr literal )) ) ) ) )

; --- Replace anonymous variables and rename variables in clause --------

(defun replace-?-vars (exp)
  "Replace any anonymous variable ? within exp with a var of the form ?123"
  (cond ((eq exp '?) (gensym "?"))
        ((atom exp) exp)
        (t (cons (replace-?-vars (first exp))
                 (replace-?-vars (rest exp))) ))  )

(defun rename-variables (x)       ; clause -> clause (with vars renamed)
  "Replace all variables in x with new ones"
  (sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))
                  (variables-in x))
          x))

(defun variables-in (exp)
  "Return a list of all the variables in exp"
  (unique-find-anywhere-if #'variable-p exp))

(defun unique-find-anywhere-if (predicate tree &optional found-so-far)
  "Return a list of leaves of tree satisfying predicate,
    with duplicates removed"
  (if (atom tree)
      (if (funcall predicate tree) (adjoin tree found-so-far) found-so-far)
      (unique-find-anywhere-if predicate (first tree)
                (unique-find-anywhere-if predicate (rest tree) found-so-far)
 )))

;;; ----------------------------------------------------------------------
;;;
;;; Part 2: clauses and extended clauses
;;;
;;; --- Constants, variables and parameters ---

(defconstant <- nil   "pos/neg literals separator")
(defvar *axioms* nil)               ; list of all 'program' clauses
(defvar *goals* nil)                ; list of goal clauses

(defconstant +empty-clause+ t
    "indicates a proof: we resolved to the empty clause")
(defconstant +no-resolvant+ t
    "indicates clauses don't resolve")

; -----------------------------------------------------------------------
; EXAMPLE CLAUSES - WE HAVE AN EXTRA LEVEL OF PARENS FOR <-  .. REMEMBER!
;
; A fact is a clause (a list of literals) which has one (positive) literal
; followed by <- (which has value nil though this is not currently used).
; (defvar *c1* '( (likes horvath moties) <- )    ; a fact clause

; A rule is a clause (a list) which is a (positive) literal (the clause head)
; followed by <- and then a list of literals - the body of the clause.
;
; We use <- with value nil as a spacer only for human readability.
; (defvar *c2* '((likes sally ?who) <- ((likes ?who ?y) (likes ?y moties))) ;rule
;
; A goal is a clause (a list) of one or more negative literals.
; First element is <- for human readability.
; (defvar *g* '(<- ((likes ?x renner) (likes ?x rod)) ) )   ; a goal clause
;
; An index is a binary tree of integers, with leaves nil.
; Example: (1 (nil nil)) or (16 (12 (7 (nil nil)) (4 (nil nil)) ) (5 (nil nil)) )
; Each leading integer is the current clause number;
; the two immediate children are the two parent clauses .. and so on.
; Initial goals and axioms have no parents, thus nil.
;
; An extended clause is a triple: index,  clause then (if a goal) binding.
; Implemented as a list like this: (index clause binding). Example:
;
; (defvar *icb* '((13 (4 (nil nil)) (2 (nil nil)))             ; Index
;                      (<- ((likes ?x renner) (amusing ?x)))   ; Clause
;                               ((T . T))))                    ; Binding
;
; I don't use constructors/projectors for extended clauses:
; just remember their structure as triples.

; --- Clause constructors and projectors ---

(defun mk-fact-clause (literal)              ; Lit -> fact clause
   (list literal '<-))

(defun mk-rule-clause (literal literal-list) ; Lit x Lit-list ->rule clause
   (list literal '<- literal-list))

(defun mk-goal-clause (literal-list)         ; Lit-list -> goal clause
   (list '<- literal-list))

; --- test data (Mote in God's Eye): axioms and goal ---

(defvar *c1* (mk-fact-clause '(member ?item (?item . ?rest ))))
(defvar *c2* (mk-rule-clause '(member ?item (? . ?rest)) '((member ?item ?rest))))
(defvar *c3* (mk-fact-clause '(likes rod horvath)))
(defvar *c4* (mk-fact-clause '(likes sally renner)))
(defvar *c5* (mk-fact-clause '(likes sally rod)))
(defvar *c6* (mk-fact-clause '(likes hardy renner)))
(defvar *c7* (mk-fact-clause '(likes hardy rod)))
(defvar *c8* (mk-fact-clause '(amusing hardy)))
(defvar *c9* (mk-fact-clause '(likes horvath moties)))
(defvar *c10* (mk-rule-clause '(likes sally ?x) '((likes ?x moties)) ) )
(defvar *c11* (mk-rule-clause '(likes rod ?x) '((likes ?x renner) (likes ?x rod))))
(defvar *c12* (mk-rule-clause '(likes ?x ?y) '((amusing ?y) (likes rod ?y)) ) )
(defvar *c13* (mk-fact-clause '(likes ?x ?x)))

(defvar *g1* (mk-goal-clause '((likes sally ?who))))
(defvar *g2* (mk-goal-clause '((member sally (rod renner horvath sally . moties)))))

(setf *axioms* (list *c1* *c2* *c3* *c4* *c5* *c6* *c7* *c8*
                 *c9* *c10* *c11* *c12* *c13*))

(setf *goals* (list *g1*))

; -----Datatype operators for clauses -----------------------------------

(defun is-fact-clause (clause)
   (and (= (length clause) 2) (equal (cadr clause) '<-)) )

(defun is-rule-clause (clause)
   (and (= (length clause) 3) (equal (cadr clause) '<-)) )

(defun is-goal-clause (clause)
   (and (= (length clause) 2) (equal (car clause) '<-)) )

(defun axiom-head-literal (clause)           ; Clause -> Lit (remove <-)
    (if (or (is-fact-clause clause) (is-rule-clause clause))
        (first clause)
        "error - not a fact or rule clause" ) )

(defun axiom-body-literal-list (clause)      ; Clause -> Lit-list (remove <-)
    (if (is-rule-clause clause) (third clause) nil))

(defun goal-literal-list (goal-clause)    ; Clause -> Lit-list (remove <-)
    (if (is-goal-clause goal-clause)
            (second goal-clause)
            "error - not goal clause"))

(defun pred (literal) (car literal))    ; Lit -> Symbol (predicate)

; ----------------------------------------------------------------------
#|
; get-clauses: Pred-symbol x Clause-list -> Clause-list where head matches
; This is an optimisation not currently used.

(defun get-clauses (p cl)
  "Get those clauses (facts and rules) from cl (the kb) which match
   the (goal) predicate, and which are therefore candidates for unification"
  (remove-if-not #'(lambda (c) (equalp p (pred (axiom-head-literal c)))) cl) )
|#

; initialise-databases: Clause-list x Clause-list -> Extended-Clause versions
; note - args are clause lists (from user), not extended clauses

(defun initialise-databases (goal-list axiom-list)  
   "Takes the goal and the program and creates extended clause list versions"
  (let* ((index     (list 0 (list nil nil)))
         (ia-list   (mk-extended-clauses index axiom-list nil))
         (new-index (list (apply #'max (mapcar #'caar ia-list))(list nil nil)))
         (igb-list  (mk-extended-clauses new-index goal-list +no-bindings+)))
      (list igb-list ia-list) ) )

(defun mk-extended-clauses (index clause-list bindings) ; -> ig(b)-list
  (cond ((null clause-list) nil)
         (bindings (let ((index1 (incr-index index)) )
                     (cons (list index1 (car clause-list) bindings)  ; goal list
                        (mk-extended-clauses index1 (cdr clause-list) bindings))))
         (t     (let ((index1 (incr-index index)) )
                   (cons (list index1 (car clause-list))           ; axiom list
                      (mk-extended-clauses index1 (cdr clause-list) bindings))))))

(defun incr-index (i) (list (+ (car i) 1) (cadr i)) ) ; Just ups the first number

;   (incr-index '(19 ((17 ((14 (nil nil)) (10 (nil nil))))
;   (20 ((17 ((14 (nil nil)) (10 (nil nil)))

;;; ----------------------------------------------------------------------
;;;
;;;   Part 3: the theorem prover
;;;
;;;  ---  Binary Resolution
;;;
;;;   L1 <= M1,M2,M3      <= L1,G2
;;;   --------------------------------------------   L1 is resolved upon giving binding b
;;;          <= G2,M1,M2,M3                         The binding b is applied to the new goals
;;;

;  binary-resolve: Goal x Axiom x Bindings -> new-Goal x Bindings (after substs)
;  note that these are all clauses, not extended clauses

(defun binary-resolve (goal axiom1 b1)
  "goal =  a goal clause (previously extracted from extended-goal-list)
    axiom = a fact or rule clause (extracted from the extended-axiom-list)  
    b1 =    bindings stored with the goal clause"
  (let* ((axiom                (rename-variables axiom1)) ;rename vars in axiom
         (axiom-head-lit       (axiom-head-literal axiom))       ; remove '<-
         (axiom-body-lit-list  (axiom-body-literal-list axiom))  ; remove '<-
         (goal-lit-list        (goal-literal-list goal))         ; remove '<-
         (head-goal-lit        (car goal-lit-list))
         (other-goal-lits      (cdr goal-lit-list))
         (b                    (unify axiom-head-lit head-goal-lit b1)) )
    (cond ((equal b '+fail+)
           (list '+no-resolvant+ '+fail+))
          ( t (if (and (null axiom-body-lit-list) (null other-goal-lits))
                  (list '+empty-clause+ b)
                (list (mk-goal-clause
                       (mapcar #'(lambda (literal)
                                   (subst-bindings b literal))
                               (append other-goal-lits axiom-body-lit-list) ))
                      b))))) )

; Example:
;  (binary-resolve  *g1*  *c12* +no-bindings+)
;  ((<- ((AMUSING ?WHO) (LIKES ROD ?WHO))) ((#:?Y871 . ?WHO) (#:?X870 . SALLY)))

;  one-step-prove:  Nat x ext-goal-list x axioms -> ext-goal-list
(defun one-step-prove (max-i igb-list ia-list)
  "Takes max index so far,  extended goal list,
   returns new extended goal list, (no +fail+s)"
  (let* ((igb       (car igb-list))   ; igb = extended goal clause, head of list
         (g-index   (first igb))      ; extract the goal clause index
         (goal      (second igb))     ; extract the goal clause itself
         (b1        (third igb))      ; extract the previously stored binding
         (a-indexes (mapcar #'first  ia-list))   ; list of indexes of axioms
         (a-list    (mapcar #'second ia-list))   ; list of axiom clauses
         (new-gb-list (mapcar #'(lambda (x) (binary-resolve goal x b1)) a-list)) )
    (mk-new-igb-list max-i g-index a-indexes new-gb-list) ) )

; Example:
; A detailed walkthrough of one-step-prove starting with the arguments ----

(defvar *igb-list-ia-list* (initialise-databases *goals* *axioms*))
(defvar *igb-list* (car *igb-list-ia-list*))
(defvar *ia-list* (cadr *igb-list-ia-list*))


;    *igb-list*                                           ; extended goals
; (((14 (nil nil)) (<- ((LIKES SALLY ?WHO))) ((T . T))))
;
;     (pprint *ia-list*)                                  ; extended axioms
#|
(((1 (NIL NIL)) ((MEMBER ?ITEM (?ITEM . ?REST)) <-))
 ((2 (NIL NIL)) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
 ((3 (NIL NIL)) ((LIKES ROD HORVATH) <-))
 ((4 (NIL NIL)) ((LIKES SALLY RENNER) <-))
 ((5 (NIL NIL)) ((LIKES SALLY ROD) <-))
 ((6 (NIL NIL)) ((LIKES HARDY RENNER) <-))
 ((7 (NIL NIL)) ((LIKES HARDY ROD) <-))
 ((8 (NIL NIL)) ((AMUSING HARDY) <-))
 ((9 (NIL NIL)) ((LIKES HORVATH MOTIES) <-))
 ((10 (NIL NIL)) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
 ((11 (NIL NIL)) ((LIKES ROD ?X) <- ((LIKES ?X RENNER) (LIKES ?X ROD))))
 ((12 (NIL NIL)) ((LIKES ?X ?Y) <- ((AMUSING ?Y) (LIKES ROD ?Y))))
 ((13 (NIL NIL)) ((LIKES ?X ?X) <-)))
|#
;
;    (setf igb (car *igb-list*))    ; curr extended goal clause
; ((14 (NIL NIL)) (<- ((LIKES SALLY ?WHO))) ((T . T)))
;
;    (setf g-index (first igb))
; (14 (NIL NIL))
;
;    (setf goal (second igb))
; (<- ((LIKES SALLY ?WHO)))
;
;    (setf b1 (third igb))
; ((T . T))
;
;    (pprint (setf a-indexes (mapcar #'first  *ia-list*)) )
#|
((1 (NIL NIL))
 (2 (NIL NIL))
 (3 (NIL NIL))
 (4 (NIL NIL))
 (5 (NIL NIL))
 (6 (NIL NIL))
 (7 (NIL NIL))
 (8 (NIL NIL))
 (9 (NIL NIL))
 (10 (NIL NIL))
 (11 (NIL NIL))
 (12 (NIL NIL))
 (13 (NIL NIL)))
|#
;
;    (pprint (setf a-list (mapcar #'second *ia-list*)))
#|
(((MEMBER ?ITEM (?ITEM . ?REST)) <-)
 ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST)))
 ((LIKES ROD HORVATH) <-)
 ((LIKES SALLY RENNER) <-)
 ((LIKES SALLY ROD) <-)
 ((LIKES HARDY RENNER) <-)
 ((LIKES HARDY ROD) <-)
 ((AMUSING HARDY) <-)
 ((LIKES HORVATH MOTIES) <-)
 ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
 ((LIKES ROD ?X) <- ((LIKES ?X RENNER) (LIKES ?X ROD)))
 ((LIKES ?X ?Y) <- ((AMUSING ?Y) (LIKES ROD ?Y)))
 ((LIKES ?X ?X) <-))
|#
;
; - one-step-prove maps binary-resolve across axioms -> resolvants (if any):
;
; (pprint (setf new-gb-list (mapcar #'(lambda (x) (binary-resolve goal x b1)) a-list)))
;
#|
((+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+EMPTY-CLAUSE+ ((?WHO . RENNER)))
 (+EMPTY-CLAUSE+ ((?WHO . ROD)))
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 ((<- (#)) ((#:?X1003 . ?WHO)))
 (+NO-RESOLVANT+ +FAIL+)
 ((<- (# #)) ((#:?Y1006 . ?WHO) (#:?X1005 . SALLY)))
 (+EMPTY-CLAUSE+ ((?WHO . SALLY) (#:?X1007 . SALLY))))
|#

; and finally we remove the +FAIL+ values and update the clause indexes for the
; genuine new clauses - to return the list of additional igb clauses.
;
; That's the job of mk-new-igb-list.
;
;   (setf new-igb-list1 (mk-new-igb-list 14 g-index a-indexes new-gb-list) ))
;   (mapcar #'pprint new-igb-list1)
#|
((15 ((14 (NIL NIL)) (4 (NIL NIL)))) +EMPTY-CLAUSE+
     ((?WHO . RENNER)))
((16 ((14 (NIL NIL)) (5 (NIL NIL)))) +EMPTY-CLAUSE+
     ((?WHO . ROD)))
((17 ((14 (NIL NIL)) (10 (NIL NIL)))) (<- ((LIKES ?WHO MOTIES)))
     ((#:?X1003 . ?WHO)))
((18 ((14 (NIL NIL)) (12 (NIL NIL)))) (<- ((AMUSING ?WHO) (LIKES ROD ?WHO)))
     ((#:?Y1006 . ?WHO) (#:?X1005 . SALLY)))
((19 ((14 (NIL NIL)) (13 (NIL NIL)))) +EMPTY-CLAUSE+
      ((?WHO . SALLY) (#:?X1007 . SALLY)))


|#
;
; mk-new-igb-list: max-index x g-index x a-indexes x new-gb-list -> igb-list
; Read as 'make additional igb extended clauses' - to be added to the pot
; Takes the new resolvants from the latest goal and creates additional igb
; extended clauses to be added to the overall igb-list.

; mk-new-igb-list arguments:
; max-i is just a number, the highest clause number yet allocated, eg 7
; a-index: eg (3 (nil nil))
; g-index: eg  (15 ((3 (nil nil)) (2 (nil nil))))
; a-indexes: eg ((1 (nil nil)) (2 (nil nil)) ...  (n (nil nil)) )
; new-gb-list: eg ((+no-resolvant+ +fail+) (goal b1) (+empty-clause+ b2) ..)
; the task here is to remove +fail+s and update the indexes.

(defun mk-new-igb-list (max-i g-index a-indexes new-gb-list)
  (if (null new-gb-list)
      nil
    (let* ((a-index        (car a-indexes))  ;(i (nil nil)) index for axiom
           (a-rest-indexes (cdr a-indexes))  ;remaining axiom indexes
           (gb             (car new-gb-list))
           (gb-rest        (cdr new-gb-list))
           (g              (first  gb))  
           (b              (second gb)) )
      (cond ((equal b '+fail+)
                (mk-new-igb-list max-i g-index a-rest-indexes gb-rest))
            (t  (let ((new-index (list (+ max-i 1) (list g-index a-index))))
                  (cons (list new-index g b)
                        (mk-new-igb-list (+ max-i 1) g-index
                                          a-rest-indexes gb-rest))))))))


;   (pprint (setf new-igb-list (one-step-prove 14 *igb-list* *ia-list*)))
;
; [Same result as from (mapcar #'pprint new-igb-list1) above].

;;; -- Now we look to the top-level loop which iterates until termination --

(defvar *1step* t)  ; If t stops proof loop each iteration and
;                          prints archived-proofs & goals

(defun empty-clause-p (igb-clause)              ;  -> Bool
   (equal '+empty-clause+ (second igb-clause)))

(defun prove1 (archived-goals archived-proofs igb-list ia-list depth)
 ; -> archived-proofs
  "'prove1' iterates, finally returning archived-goals and archived-proofs
   for subsequent proof extraction"
  (if (or (zerop depth) (null igb-list))
      (if *1step* (progn (terpri)
                         (princ "Done: archived-goals = ")
                         (pprint archived-goals) (terpri)
                         (princ "Archived-proofs = ")
                         (pprint archived-proofs) (terpri)
                         (list archived-goals archived-proofs))
                   (list archived-goals archived-proofs))
    (let* ((max-i (apply #'max (mapcar 'caar (append archived-proofs igb-list))))
           (new-igb-list1     (one-step-prove max-i igb-list ia-list))
           (new-empty-clauses (remove-if-not #'empty-clause-p new-igb-list1))
           (new-igb-list      (remove-if #'empty-clause-p new-igb-list1))
           (archived-goals1   (cons (car igb-list) archived-goals))
           (archived-proofs1  (append new-empty-clauses archived-proofs))
           (igb-list1         (cdr igb-list))
           (next-igb-list     (append igb-list1 new-igb-list)) )
           ; depth first: reverse append order for breadth first
       (if *1step* (progn (terpri)
                          (princ "Depth = ") (princ depth)
                          (princ ". Archived-goals1 = ")
                          (pprint archived-goals1) (terpri) (terpri)
                          (princ "Archived-proofs1 = ")
                          (pprint archived-proofs1) (terpri) (terpri)
                          (princ "next-igb-list = ")
                          (pprint next-igb-list)  (terpri)
                          (princ "type return: ") (terpri)
                          (read-char) (princ "-----") ))
      (prove1 archived-goals1 archived-proofs1
                  next-igb-list ia-list (- depth 1)))))

(defun prove (goals axioms depth) ;goals and axioms are input clause-lists
  "prove turns initial clauses into extended-clauses then calls prove1.
   Returns a 2 member list of extended clauses:(archived-goals archived-proofs)"
   (let* ((igb-ia (initialise-databases goals axioms))
          (igb-list (first igb-ia))
          (ia-list (second igb-ia))
          (initial-archived-goals  nil)
          (initial-archived-proofs nil) )
     (prove1 initial-archived-goals initial-archived-proofs igb-list ia-list depth)))

; 'archived-proofs' is a list of igb extended clauses
; (setf *archived-proofs* (prove *goals* *axioms* 4))
;
; --- Transform archived-proofs into a readable collection of proofs --
; Note that 'archived-goals-and-proofs' =  a two-member list:
;     (archived-goals archived-proofs)
; is returned by 'prove'.

(defun show-all-proofs (archived-goals-and-proofs ia-list goals)
  (let* ((archived-goals  (first  archived-goals-and-proofs))
         (archived-proofs (second archived-goals-and-proofs))
         (all-igbs  (append archived-goals archived-proofs ia-list))
         (proofs (mapcar #'(lambda (x) (show-proof x all-igbs goals))
                              archived-proofs)))
     (reverse proofs)))

(defun show-proof (empty-igb all-igbs top-level-goals)
 "empty-igb is the root of the proof tree we construct here"
       (let* ((index     (first empty-igb))
              (answer    (subst-bindings (third empty-igb) top-level-goals))
              (proof     (mk-proof-list index all-igbs)) )
          (list answer (reverse proof))) )

(defun mk-proof-list (i all-igbs)
  "Traverses index i as a tree pulling out the matching clauses"
   (if (null i)
        nil
      (let* ((current-igb-# (first i))
             (current-igb (get-igb-by-n current-igb-# all-igbs))
             (current-clause (second current-igb))
             (left-ancestor  (first (second i)))
             (right-ancestor (second (second i)))
             (tg (list (car i) (first (first (second i)))
                               (first (second (second i))))))
         (cons (list tg current-clause)
               (append (mk-proof-list left-ancestor  all-igbs)
                       (mk-proof-list right-ancestor all-igbs) ))) ) )

(defun get-igb-by-n (n igb-list)  ; nat x igb-list -> igb
  " example (n=3) returns ((3 (nil nil)) ((LIKES ROD HORVATH) <-)) "
   (find-if #'(lambda (igb) (= n (caar igb))) igb-list))


;;; ----------------------------------------------------------------------
;;;
;;;  Part 4:  TEST DATA

#|

With goal: (setf *goals* (list *g1*))

   ((<- ((LIKES SALLY ?WHO))))

   (defvar *igb-list-ia-list* (initialise-databases *goals* *axioms*))
   (defvar *igb-list* (car *igb-list-ia-list*))  ; ext. goal clause(s)
   (defvar *ia-list* (cadr *igb-list-ia-list*))  ; ext. axiom clauses

; The above three assignments were eval'ed above so already bound.
; Prove itself calls 'initialise-databases' to set up extended clauses

 (setf archived-goals-and-proofs (prove *goals* *axioms* 6))   ; depth 6 here

(pprint (setf all-proofs (show-all-proofs archived-goals-and-proofs *ia-list* *goals*)))

Result: (with a few added line-breaks)

((((<- ((LIKES SALLY SALLY))))
  (((13 NIL NIL) ((LIKES ?X ?X) <-))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((19 14 13) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY ROD))))
  (((5 NIL NIL) ((LIKES SALLY ROD) <-))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((16 14 5) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY RENNER))))
  (((4 NIL NIL) ((LIKES SALLY RENNER) <-))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((15 14 4) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY MOTIES))))
  (((13 NIL NIL) ((LIKES ?X ?X) <-))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((17 14 10) (<- ((LIKES ?WHO MOTIES))))
   ((24 17 13) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY HORVATH))))
  (((9 NIL NIL) ((LIKES HORVATH MOTIES) <-))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((17 14 10) (<- ((LIKES ?WHO MOTIES))))
   ((20 17 9) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY SALLY))))
  (((13 NIL NIL) ((LIKES ?X ?X) <-))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((17 14 10) (<- ((LIKES ?WHO MOTIES))))
   ((21 17 10) (<- ((LIKES MOTIES MOTIES))))
   ((27 21 13) +EMPTY-CLAUSE+))))

; -------------------------------------------------------------------------

With goal: (setf *goals* (list *g2*))

   ((<- ((MEMBER SALLY (ROD RENNER HORVATH SALLY . MOTIES)))))


(pprint (setf all-proofs (show-all-proofs archived-goals-and-proofs *ia-list* *goals*)))

((((<- ((MEMBER SALLY (ROD RENNER HORVATH SALLY . MOTIES)))))
  (((1 NIL NIL) ((MEMBER ?ITEM (?ITEM . ?REST)) <-))
   ((2 NIL NIL) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
   ((2 NIL NIL) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
   ((2 NIL NIL) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
   ((14 NIL NIL) (<- ((MEMBER SALLY (ROD RENNER HORVATH SALLY . MOTIES)))))
   ((15 14 2) (<- ((MEMBER SALLY (RENNER HORVATH SALLY . MOTIES)))))
   ((16 15 2) (<- ((MEMBER SALLY (HORVATH SALLY . MOTIES)))))
   ((17 16 2) (<- ((MEMBER SALLY (SALLY . MOTIES)))))
   ((18 17 1) +EMPTY-CLAUSE+))))

|#

; --------------------------- End of program -------------------------------