;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; This unification procedure returns an association list, each of whose
;;; elements is a dotted pair consisting of a variable name and a formula
;;; which is to be substituted for it.  This returned value represents the
;;; MGU of the two formulas passed as arguments to it.  If the two
;;; formulas do not unify, the return value is the atom 'no.
;;; (Note that a return value of nil, the empty list, just means that
;;; the two formulas unify and no variable bindings are required for this.
;;; This occurs if and only if (equal pat1 pat2) returns t.)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun unify (pat1 pat2)
  (subunify pat1 pat2 nil))

(defun subunify (pat1 pat2 theta)
  (cond
    ((equal pat1 pat2) theta)
    ((is-var pat1) (setq theta (var-unify pat1 pat2 theta)))
    ((is-var pat2) (setq theta (var-unify pat2 pat1 theta)))
    ((or (atom pat1) (atom pat2) (/= (length pat1) (length pat2))) 'no)
    (t
      (do ((rest1 pat1 (cdr rest1))       ; loop through lists together
	   (rest2 pat2 (cdr rest2)))
					  ; return if done or attempt failed
	  ((or (null rest1) (eql theta 'no)) theta)
         
	  (setq theta (subunify (car rest1) (car rest2) theta))))))

(defun var-unify (var pat theta)
   (let ((match (assoc var theta)))
	(cond
	  (match (subunify (cdr match) pat theta))
	  ((eql var pat) theta)
	  ((occurs-in var (varsubst pat theta)) 'no)
	  (t (cons (cons var pat)
		   theta)))))
;		   (varsubst theta (list (cons var pat))))))))

(defun occurs-in (a l)
 ; returns t if the atom a occurs anywhere in l
  (cond ((atom l) nil)
	((eql a (car l)) t)
	(t (or (occurs-in a (car l)) (occurs-in a (cdr l))))))

(defun is-var (formula)	   ; test whether formula is symbol beginning with "?"
  (and (atom formula)
       (string= "?" (string formula) :end2 1)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; This function accepts as arguments a skolemized predicate calculus
;;; formula and an association list specifying a set of substitutions to
;;; perform, as is returned by "unify".  It returns the corresponding
;;; formula with the substitutions performed.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun varsubst (form subst-alist)
  (cond ((null subst-alist) form)
	(t (varsubst (subst (cdar subst-alist)
			    (caar subst-alist)
			    form)
		     (cdr subst-alist)))
	))