-*- Mode:Text; -*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename:   resolution.pseudo
;;; ========================================================================
;;; The RESOLUTION INFERENCE RULE
;;; Described in every AI textbook. Author: Robinson J. "The generalized
;;; Resolution Principle", in Machine Intelligence 3, Elzevier, NY 1968
;;;-------------------------------------------------------------------------

FUNCTION Full-Binary-Resolution WITH PARAMETERS Clause1, Clause2 RETURNS Clauses,
        where Clause1 and Clause2 are clauses, and Clauses is a list of clauses,
        each a distinct Resolvent of Clause1 and Clause2.


        Resolvents will denote all the resolvents of the given clauses.
        Initially Resolvents is null.

        1. Head1 and Tail1 denote lists whose concatenation at 
           all times is Clause1. Lit1 is the first literal of Tail1.
           Initially Head1 is null and Tail1 is Clause1. In each 
           iteration the first literal of Tail1 is moved to Head1.
           Iterations terminate when Tail1 becomes null.
           At that time we have determined all the possible resolvents
           of the given clauses. In each iteration we execute
           steps 2. and 3.

        2. Head2 and Tail2 denote lists whose concatenation at 
           all times is Clause2. Lit2 is the first literal of Tail2.
           Initially Head2 is null and Tail2 is Clause2.
           Iterations terminate when Tail2 becomes null.
           In each iteration we execute step 3.

        3. If Lit1 and Lit2 are of opposite signs (i.e. one is an atom and the other is
           the negation of an atom), AND they have a Most General Unifier MGU THEN:

               Apply MGU to Head1, Tail1, Head2, Tail2 and collect all the 
               distinct literals found in these lists. This list is the (binary) resolvent
               corresponding to Lit1 and Lit2 for Clause1 and Clause2.
               Add this resolvent to Resolvents.