Unifikation mit :-Notation f"ur getypte Variablen

(defun dom-in-sort (dom sort)
  (dom-intersection dom (sortbase-ind sort)))


(defun sortbase-ind (sort)
  (and (sortbase-sortp sort)
       (let ((ind*-list (get-ind*-list
                          (get-sort-list *subsumes-individuals* sort))))
           (cond (ind*-list (cons 'dom (cdr ind*-list)))
                  (t nil)))))

(defun sortbase-sortp (sort)
  (sort-defined sort *subsumes-individuals*))

(defun sort-defined (sort list)
  (and list
       (cond ((equal sort (caar list)) t)
             (t (sort-defined sort (cdr list))))))

(defun sortbase-individualsp (const sort)
  (cond ((member const
                 (get-ind*-list (get-sort-list *subsumes-individuals* sort)))
         const)
        (t nil)))


(defun sortbase-glb (sort1 sort2)
  (let ((subsumes1 (cdr (get-sub*-list
                         (get-sort-list *subsumes-individuals* sort1))))
       (subsumes2 (cdr (get-sub*-list
                         (get-sort-list *subsumes-individuals* sort2)))))
       (glb subsumes1 subsumes2)))

(defun glb (sub-list1 sub-list2)
  (and sub-list1
       (cond ((member (car sub-list1) sub-list2) (car sub-list1))
             (t (glb (cdr sub-list1) sub-list2)))))