The agenda control

The Lisp definition of the basic agenda control looks as follows (abbreviated where convenient):

(defun prove (goal)
  (let ((goal-pred (predicate (clause-head goal)))
        (start-item (make-start-item goal)))
     
    (add-task-to-agenda start-item
                        (compute-priority)
                        *agenda*)
    
    
    (do ((task (get-highest-priority-task *agenda*)
               (get-highest-priority-task *agenda*)))
        
        ((null task) (if (consp *result*) T))

    (if (add-item task) ;; only adds item if not blocked;
      (let ((result (get-answer goal-pred task)))
            ;; check initial item set
          (if result
              (progn
                (setf (item-ignore result) T) 
              ;; ``simulates'' removal of found answer from item set
                (push result *result*)
                (if *all-p* ;; non-interactive mode
                    (process-one task)
                  (progn 
                    (print-result (lemma-clause result)) 
                    ;; used fegramed to show result
                    (if (yes-or-no-p 
                         "~&Should we continue looking for solutions?  ")
                        ;; Prolog-like interactive mode
                        (process-one task)
                      (return T)))))
           ;; if currently no answer has been found
           (process-one task)))))))



(defun process-one (item)
   (if (item-unit item)
      (passive-completion item)
    (or (active-completion item))
       (progn
         (prediction item)
         (scanning item))))