;;; -*- Mode:Lisp; Package: User; Syntax:Common-Lisp; Base:10;-*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename:   clausal-alg.cl
;;; ========================================================================
;;; CLAUSIFICATION ALGORITHM
;;; It is derived from  Genesereth+Nilsson: Logical Foundations of Artificial
;;; Intelligence, pp63-66
;;; Code to put a prefix formula, possibly with quantifiers, etc.
;;; into clausal form, i.e. as a list of clauses, where each clause is a
;;; list of literals [an atom or its negation].
;;; NOTE: The given formula must be grammatically correct. It may contain
;;; free variables, in which case they will be assumed to be universally 
;;; quantified.
;;; THE LANGUAGE:
;;;   Variables are symbols starting with a question mark, for example ?x21.
;;;   The logical connectives are:
;;;       ~   (not)
;;;       &   (and)
;;;       or
;;;       =>  (if .. then)
;;;      <=>  (iff)
;;;  The quantifiers are:
;;;      ALL
;;;      EXIST
;;;  An example of conversion is from:
;;;      (all ?x (exist ?y (<=> (p ?x a) (q a ?y))))
;;;  to:
;;;      (((~ (p ?x198)) (q a (skolem197 ?x198))) 
;;;       ((~ (q a (skolem197 ?x199))) (p ?x199 a)))
;;; NOTE: This code can be used as is (no additional code is required).
;;;--------------------------------------------------------------------

(defun convert-to-clause-form (expr)
  ;; Converts expr to clause form
  ;; Inputs: The expression expr
  ;; Outputs: A list of clauses obtained from expr.
  ;; NOTE: This function could have been written as a single assignment.
  ;; It has been written as a sequence of assignments to stress the 
  ;; successive transformations.
  
  (setq expr (unbound-to-universal expr))   ; It universally quantifies all the
                                            ; variables that are not bound in expr
  (setq expr (eliminate-implies expr))            ; Eliminate => and <=>
  (setq expr (reduce-scope-of-not expr))    ; The scope of ~ is an atom
  (setq expr (unique-quant-variables expr)) ; Make sure all quantified 
                                            ; variables are distinct
  (setq expr (eliminate-existentials expr)) ; Use Skolem functions to 
                                            ; eliminate existential quantifiers
  (setq expr (eliminate-universals expr))   ; Eliminate universal quantifiers
  (setq expr (distributive expr))           ; Do not leave & within scope of or
  (setq expr (form-clauses expr))           ; Create clauses
  (setq expr (standardize-apart expr)))     ; Make sure that distinct clauses do
                                            ; not share variables

(defun unbound-to-universal (expr)
  ;; expr is a formula where some variables may be unbound.
  ;; Universally bound them.
  ;;REMINDER: 'labels' is a way of declaring local functions.
  (labels ((find-unbound (e &optional bound &aux unbound)
           ;; Returns the variables that occur in e and are not in bound
             (cond ((varp e) (unless (member e bound)
                               (list e)))
                   ((atom e) nil)
                   ((member (first e) '(all exist))
                    (setq bound (cons (second e) bound))
                    (find-unbound (third e) bound))
                   (t
                    (dolist (a (rest e))
                      (setq unbound (append (find-unbound a bound) unbound)))
                    unbound))))
    (dolist (v (find-unbound expr))
      (setq expr (list 'all v expr))))
    expr)
                    
(defun eliminate-implies (e &aux f1 f2)
  ;; Eliminates implications => and <=> from the input expression e
  (cond ((atom e)
         e)
        ((eq (first e) '=>)
         (list 'or (list '~ (eliminate-implies (second e))) 
               (eliminate-implies (third e))))
        ((eq (first e) '<=>)
         (setq f1 (eliminate-implies (second e)))
         (setq f2 (eliminate-implies (third e)))
         (list '& 
               (list 'or (list '~ f1) f2)
               (list 'or (list '~ f2) f1)))
        (t (mapcar #'eliminate-implies e))))

(defun reduce-scope-of-not (e &aux f1)
  ;; Reduces the scope of not in form e to a single atomic formula
  (cond ((atom e) 
         e)
        ((not (eq (first e) '~))
         (mapcar #'reduce-scope-of-not e))
        (t ;; e starts with ~
         (setq f1 (second e))
         (cond ((atom f1) 
                e)
               ((eq (first f1) '~) 
                (reduce-scope-of-not (second f1)))
               ((eq (first f1) 'or)
                (list '& (reduce-scope-of-not (list '~ (second f1)))
                         (reduce-scope-of-not (list '~ (third f1)))))
               ((eq (first f1) '&)
                (list 'or (reduce-scope-of-not (list '~ (second f1)))
                         (reduce-scope-of-not (list '~ (third f1)))))
               ((eq (first f1) 'all)
                (list 'exist (second f1) (reduce-scope-of-not (list '~ (third f1)))))
               ((eq (first f1) 'exist)
                (list 'all (second f1) (reduce-scope-of-not (list '~ (third f1)))))
               (t
                e)))))

(defun unique-quant-variables (e)
  ;; It makes sure that in e each quantifier operates on a distinct variable
  (cond ((atom e)
         e)
        ((member (first e) '(all exist))
         (cons (first e) (subst (new-var) (second e) 
                                (unique-quant-variables (rest e)))))
        (t
         (mapcar #'unique-quant-variables e))))

(defun eliminate-existentials (e &optional vars)
  ;; Eliminates existential quantifiers from e. Then each occurrence of the
  ;; existentially quantified variable y which is dependent on the 
  ;; universal variables vars x1 x2 .. is replaced by a term of the form
  ;;    (SKOLEM x1 x2 ..)
  (labels ((make-skolem-func (uargs)
           ;; Returns a Skolem function of uargs or a constant if no arguments
           (if (null uargs)
               (gentemp "SKOLEM")
             (cons (gentemp "SKOLEM") uargs))))
        (cond ((atom e)
               e)
              ((eq (first e) 'all)
               (list (first e) (second e) 
                    (eliminate-existentials (third e) (cons (second e) vars))))
              ((eq (first e) 'exist)
               (subst (make-skolem-func (reverse vars)) 
                      (second e) (eliminate-existentials (third e) vars)))
              (t
               (mapcar #'(lambda (f) (eliminate-existentials f vars)) e)))))

(defun eliminate-universals (e)
  ;; It returns m where m is obtained by eliminating the
  ;; universal quantifiers in e.
  (cond ((atom e) 
         e)
        ((eq (first e) 'all)
         (eliminate-universals (third e)))
        (t 
         (mapcar #'eliminate-universals e))))
  
(defun distributive (e &aux l r)
  ;; Applies distributivity to all forms like 
  ;; (or a (& b c)) or like (or (& a b) c)
  ;; i.e. we get conjunctions of disjuncts, a conjunctive form. 
  ;; After this transformation no & will be within the scope of an or.
  (cond ((atom e)
         e)
        ((eq (first e) '~)
         e)       ;; e is an atom 
        ((eq (first e) '&)
         (list '& (distributive (second e)) (distributive (third e))))
        ((eq (first e) 'or)
         (setq l (distributive (second e)))
         (setq r (distributive (third e)))
         (cond ((and (consp l) (eq (first l) '&))
                (list '& (distributive (list 'or (second l) r))
                         (distributive (list 'or (third l) r))))
               ((and (consp r) (eq (first r) '&))
                (list '& (distributive (list 'or l (second r)))
                         (distributive (list 'or l (third r)))))
               (t
                (list 'or l r))))
        (t e)))   ;; e is an atom
  
(defun form-clauses (e)
  ;; e is in conjunctive form. Eliminate all & and or and return a list
  ;; of lists of literals.
  (labels ((squash-and (f) ;; if f starts with &, it returns a list
                       ;; of its conjuncts; otherwise it returns (f)
              (if (and (consp f) (eq (first f) '&))
                  (append (squash-and (second f)) (squash-and (third f)))
                (list (squash-or f))))
           (squash-or (f)  ;; if f starts with or, it returns a list
                           ;; of its disjuncts; otherwise it returns (f)
              (if (and (consp f) (eq (first f) 'or))
                  (append (squash-or (second f)) (squash-or (third f)))
                (list f))))
          (squash-and e)))

(defun standardize-apart (e)
  ;; It makes sure that distinct clauses use distinct variables.
  (labels ((find-variables (e)
            ;; Returns as a list all the variables in e
            (cond ((varp e) (list e))
                  ((atom e) nil)
                  (t 
                   (remove-duplicates 
                    (append (find-variables (first e))
                            (find-variables (rest e))))))))
          (mapcar #'(lambda (c)
                      (dolist (v (find-variables c))
                        (setq c (subst (new-var) v c)))
                      c)
                  e)))


(defun varp (x)
  ;; To check to see if something is a variable, just check to see if the
  ;; first character is a "?".
  ;; For example, (varp '?A) => T,  (varp "Ann") => nil.
  (and (symbolp x)
       (char= (char (symbol-name x) 0) '#\?)))

(defun new-var ()
  ;; It returns a new variable symbol.
  (gentemp "?X"))