;;; -*- Mode:Lisp; Package:User; Syntax:Common-Lisp; Base:10;-*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename:   resolution-alg.cl
;;; ========================================================================
;;; The (BINARY) RESOLUTION INFERENCE RULE
;;; We are given two clauses, say C1 and C2. In C1 we find a literal L1
;;; and in C2 we find a literal L2 such that:
;;;    1. Either L1 is a positive literal and L2 is a negative literal or
;;;       viceversa L1 is negative and L2 is positive, and
;;;    2. L1 and L2, if neglecting the negation of one of them, can be unified
;;;       by a substitution S.
;;; Then from C1 and C2 we can infer the clause C obtained as follows:
;;;    1. Remove L1 from C1, call C1' the result.
;;;    2. Remove L2 from C2, call C2' the result.
;;;    3. Apply the substitution S to C1' and C2', obtaining respectively
;;;       C1'' and C2''
;;;    4. Then C consists of all the distinct literals that appear in either
;;;       C1'' or C2''.
;;; C is called a Resolvent of C1 and C2. 
;;; 
;;; Given two clauses, we may derive from them 0 or more resolvents.
;;; For example, the clauses
;;;  ((hates ?x ?y) (loves ?x ?y)) and ((hates ?z ?w) (~ (likes ?z ?w)))
;;; have no resolvents.
;;; For example, the clauses
;;;  ( a b (~ c)) and ((~ a) (~ b) d) 
;;; have the two resolvents
;;;  (b (~ c) (~ b) d) and (a (~ c) (~ a) d)
;;; NOTE: This code can be used after loading the algorithm code associated 
;;; to the Unification Module.
;;;-------------------------------------------------------------------------
;;;-------------------------------------------------------------------------

;; We use the functions Unify and Replace-Variables defined in the file "unify-alg.cl"
(load "unify-alg.cl")

(defun full-binary-resolution (clause1 clause2)
  ;; Given two clauses [i.e., two lists of literals], returns the binary 
  ;; resolvents of these two clauses. If the null resolvent is found,
  ;; it means that we have a contradiction. The function returns with
  ;; the resolvents found up to now.
  ;; For example, given the clauses
  ;;         ((~ (rich ?x)) (eligible ?x))
  ;; and
  ;;         ( (~ (play-golf ?y)) (rich ?y))
  ;; it returns
  ;;         ( ((eligible ?y) (~ (play-golf ?y))) )
  ;; 
  ;; For each literal of clause1
  (do ((head1 nil (cons (first tail1) head1))
       (tail1 clause1 (rest tail1))
       resolvents
       a-list
       lit1 
       lit2
       mgi
       (neg-count1 0 0)
       a-resolvent)
      ((null tail1) resolvents)
    ;; Set lit1 to the first atom of tail1 and neg-count1 to 1 if
    ;; the first literal was negative.
      (setq lit1 (first tail1))
      (when (consp lit1) 
        (when (eq '~ (first lit1))
          (setq neg-count1 1)
          (setq lit1 (second lit1))))
    ;; For each literal of clause2
      (do ((head2 nil (cons (first tail2) head2))
           (tail2 clause2 (rest tail2))
           (neg-count2 0 0))
          ((null tail2))
        ;; Set lit2 to the first atom of tail2 and neg-count2 to 1 if
        ;; the first literal was negative.
        (setq lit2 (first tail2))
        (when (consp lit2) 
          (when (eq  '~ (first lit2))
            (setq neg-count2 1)
            (setq lit2 (second lit2))))
        (when (= 1 (+ neg-count1 neg-count2))
          ;; Only one of lit1 and lit2 was negative
          (multiple-value-setq (a-list mgi)(unify lit1  lit2 nil))
          (when mgi                        ; The literals were unified
            (setq a-resolvent
              (if (null a-list)
                  (append (reverse head1) (rest tail1) 
                          (reverse head2) (rest tail2))
                (replace-variables
                 (append (reverse head1) (rest tail1) 
                         (reverse head2) (rest tail2))
                 a-list)))
            (setq a-resolvent (remove-duplicates a-resolvent :test #'equalp))
            (setq resolvents (cons a-resolvent resolvents))
            (if (null a-resolvent)
                (return-from full-binary-resolution resolvents)))))))