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))))