-*- Mode:Text; -*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename:   clausal.pseudo
;;; ========================================================================
;;; The CLAUSIFICATION ALGORITHM 
;;; It is derived from Genesereth-Nilsson: Logical Foundations of AI, pp63-66
;;;-------------------------------------------------------------------------

FUNCTION Convert-to-Clause-Form  WITH PARAMETERS expr RETURNS clauses,
        where expr is a formula written in prefix form, with quantifiers and
        connectives, and clauses is an equivalent list of clauses.

        1. Universally quantify all the free variables occurring in expr.

        2. Eliminate the "=>" and "<=>" connectives by using the transformations:
                E1  => E2   becomes ((~ E1) OR E2)
                E1 <=> E2   becomes ((~ E1) OR E2) & ((~ E2) OR E1)

        3. Reduce the scope of "~" to a single atom by using the transfrmations :
                (~ (E1 OR E2))   becomes ((~ E1) & (~ E2))
                (~ (E1 & E2))   becomes ((~ E1) OR (~ E2))
                (~ (ALL ?X E))   becomes (EXIST ?X (~ E))
                (~ (EXIST ?X E)) becomes (ALL ?X (~ E))

        4. Make sure that each quantifier operates on distinct variables.
           For example 
                (ALL ?X ((P ?X) OR (EXIST ?X (Q ?X))))
           becomes
                (ALL ?X ((P ?X) OR (EXIST ?Y (Q ?Y))))

        5. Eliminate existential quantifiers by using Skolem functions.
           We proceeed as follows, for each variable ?X which is existentially
           quantified we determine all the universal quantifiers that bound it
           and the corresponding universal variables, say, ?Y1 .. ?Yn.
           Then we replace each occurrence of ?X by (SKOLEMi ?Y1 .. ?Yn), where SKOLEMi
           is a new function symbol.
           For example
                (ALL ?Y1 ((P ?Y1) & (ALL ?Y2 ((Q ?Y1 ?Y2) OR (EXIST ?X (R ?X))))))
           becomes
                (ALL ?Y1 (& (P ?Y1) (ALL ?Y2 (OR (Q ?Y1 ?Y2) (R (SKOLEM23 ?Y1 ?Y2))))))

        6. Eliminate universal quantifiers by just dropping them.

        7. Make sure that no '&' occurs within the scope of an 'OR' by using the
           transformations:
                ((E1 & E2) OR E3) becomes ((E1 OR E3) & (E2 OR E3))
                (E1 OR (E2 & E3)) becomes ((E1 OR E2) & (E1 OR E3))

        8. Form clauses by eliminating '&' and 'OR'.
           This is accomplished by applying the transformations:
                ((E2 OR .. OR En) OR ..) becomes (E2 OR .. OR En OR..)
                ((E2 & .. & En) & .. ) becomes (E2 & .. & En & ..)
           followed by the transformations:
                (E1 OR .. OR En) becomes (E1 .. En)
                (E1 & .. & En) becomes (E1 .. En)

        9. Standardize apart the variables occurring in distinct clauses.
           For example
                ( ((P ?X A) (~ Q ?Y))  ((~ (P B ?Y))) )
           becomes
                ( ((P ?X A) (~ Q ?Y))  ((~ (P B ?Z))) )