Inference rules

The Lisp definitions of the inference rules are all very similar and more or less follow the abstract definitions as used in the previous sections. The schematic structure of an inference rule is as follows:

(defun <inference-rule> (item)
  (let* (<x>
         ;; X := either the selected-element or the clause of the item itself
         <candidates>
         ;; possible candidates
         (coob (make-control-obj *global-fail-context-set*))
         (candidates? nil))
    
    (if (consp candidates)
        (dolist (candidate candidates candidates?)
          (let* ((unify-res (unify-clause x candidate coob))) ; call unifier
            (unless (eq unify-res fail) ;; if MGU exist
              (let ((new-item 
                     (make-item candidate <some-more>)))
                   (add-task-to-agenda new-item
                                       (compute-priority new-item 
                                        :producer <something>) 
                                         *agenda*)
                    (setq candidates? T)))
            (reset-ctrl-obj coob))))))

The set of possible candidates are determined in dependence of the status of the current item (active or passive) and of the specific task the inference rule is defined to fulfill. The unifier performs unification destructively, keeping a set of control objects which can be used to ``reset'' the effects of destructive unification. On each candidate the unifier is applied. If unification does not fail, a corresponding new item is created and added to agenda *agenda*. In our current implementation, each clause of a new item is copied. Thus we only have to keep one control object which has to be reseted after unification takes place (in all cases).

Note that because of the general scheme for inference rules, it might also be possible to define additional inference rules, for example one, that performs some sort of bottom-up prediction. We have actually implemented such rules (for experimental reasons), however, one should be aware of the fact, that this might change the characteristic behaviour of the whole algorithm. For this reason, we do not want to discuss this further possibility.