????????????????????????????????????????????????????????????????????????????????
?
?                 FIRST ORDER PREDICATE CALCULUS THEOREM PROVER
?
?        EE-562 - ARTIFICIAL INTELLIGENCE - SPRING 1974 - PROF. SAMUAL LEE
?
?                              BUILT BY JACK HARPER
?
?
? THIS SYSTEM IS WRITTEN IN LISP 1.5 FOR THE UNIVAC 1108 AND IMPLEMENTS A
? THEOREM PROVER FOR THE FIRST ORDER PREDICATE CALCULUS. 
?
? THE "RESOLUTION PRINCIPLE" IS USED AS THE BASIC MECHANISM.
?
? FOLLOWING IS AN EXPLANATION OF THE NOTATION, METHODOLOGY, AND ALGORITHMS 
? THAT ARE USED:
?
? THEOREMS IN THE FIRST ORDER PREDICATE CALCULUS THAT ARE TO BE PROVED
? (ATTEMPTED TO BE PROVED?) ARE FIRST TRANSFORMED INTO "SKOLEM STANDARD FORMS":
?
? LET A FORMULA F BE IN PRENEX NORMAL FORM (Q1 X1). ... .(QN XN)M, WHERE M IS IN
? A CONJUNCTIVE NORMAL FORM. LET QR BE AN EXISTENTIAL QUANTIFIER IN THE PREFIX
? (Q1 X1). ... .(QN XN), 1 <= R <= N. IF NO UNIVERSAL QUANTIFIER APPEARS BEFORE
? QR, THEN CHOOSE A NEW CONSTANT C DIFFERENT FROM OTHER CONSTANTS THAT OCCUR IN
? M -- REPLACE ALL XR THAT APPEAR IN M BY C AND DELETE (QR XR) FROM THE PREFIX. 
? IF QS1. ... .QSM ARE ALL THE UNIVERSAL QUANTIFIERS THAT APPEAR BEFORE QR, 
? 1 <= S1 <= S2 <= ... < SM < R, THEN CHOOSE A NEW M-PLACE FUNCTION SYMBOL F 
? THAT IS DIFFERENT FROM THE OTHER FUNCTION SYMBOLS AND REPLACE ALL OF THE XR IN
? M BY F(XS1, XS2, ..., XSM) AND DELETE (QR XR) FROM THE PREFIX. WHEN THIS HAS
? BEEN COMPLETED FOR ALL OF THE EXISTENTIAL QUANTIFIERS IN THE PREFIX, THE
? RESULT WILL BE THE "SKOLEN STANDARD FORM" OF THE FORMULA F.
?
? E.G., (THEREEXISTS X)(FOREACH Y)(FOREACH Z)(THEREEXISTS U)(FOREACH V)
?       (THEREEXISTS W) P(X, Y, Z, U, V, W) =
?
?       (FOREACH Y)(FOREACH Z)(FOREACH V) P(A, Y, Z, F(Y, Z), V, G(Y, Z, V))
?
? A "CLAUSE" IS A DISJUNCTION OF LITERALS. REGARD A SET OF LITERALS TO BE
? SYNONYMOUS WITH A CLAUSE.
?
? E.G., (FOREACH X)(THEREEXISTS Y)(THEREEXISTS Z)
?       ( (-P(X, Y) OR 
?           Q(X, Z)) OR 
?           R(X, Y, Z) )     (WHERE "-" MEANS "NOT")
?
? TRANSFORM THIS TO:
?
?       (FOREACH X)(THEREEXISTS Y)(THEREEXISTS Z)
?       ( (-P(X, Y) OR R(X, Y, Z)) OR 
?         ( Q(X, Z) OR R(X, Y, Z)) )
?
? AND THEN TO:
?
?       (FOREACH X)
?       ( (-P(X, F(X)) OR R(X, F(X), G(X))) OR 
?         ( Q(X, G(X)) OR R(X, F(X), G(X))) )
?
? REPRESENT THE ABOVE WITH THE CLAUSE (IN LISP NOTATION) AS:
?
?       ( (NOT (P X (F X))) 
?         (R X (F X)(G X))
?         (Q X (G X))
?         (R X (F X)(G X)) )
?
? THE THEOREM PROVER OPERATES BY ATTEMPTING TO PROVE THAT THE NEGATION OF THE
? FORMULA IS INCONSISTENT.
?
? A "SUBSTITUTION" IS A FINITE SET OF THE FORM (T1/V1, ..., TN/VN) WHERE EVERY
? VI IS A VARIABLE, EVERY TI IS A TERM DIFFERENT FROM VI, AND NO TWO ELEMENTS
? IN THE SET HAVE THE SAME VARIABLE AFTER THE STROKE SYMBOL.
?
? E.G., THE FOLLOWING SET IS A SUBSTITUTION:
?
?       (A/X, G(Y)/Y, F(G(B))/Z)
?
? OR IN LISP FORM:
?
?       ((A X) ((G Y) Y) (F (G B) Z))
?
? LET THETA = (T1/V1, ..., TN/VN) BE A SUBSTITUTION AND E BE AN EXPRESSION. THEN 
? ETHETA IS AN EXPRESSION OBTAINED FROM E BY REPLACING EACH OCCURENCE OF THE 
? VARIABLE VI, 1 <= I <= N, IN E BY THE TERM TI. ETHETA IS AN "INSTANCE" OF E.
?
? E.G., LET THETA = (A/X, F(B)/Y, C/Z) AND E = P(X, Y, Z), THEN ETHETA =
? P( A, F(B), C).
?
? LET THETA = (T1/X1, ..., TN/XN) AND LAMBDA = (U1/Y1, ..., UM/YM) BE TWO
? SUBSTITUTIONS. THEN THE "COMPOSITION" OF THETA AND LAMBDA IS THE SUBSTITUTION,
? DENOTED BY "THETA.LAMBDA", THAT IS OBTAINED FROM THE SET:
?
?       (T1LAMBDA/X1, ..., TNLAMBDA/XN, U1/Y1, ..., UM/YM)
?
? BY DELETING ANY ELEMENT TJLAMBDA/XJ FOR WHICH TJLAMBDA = XJ AND ANY ELEMENT
? UI/YI SUCH THAT YI IS AMONG (X1, X2, ..., XN)
?
? A SUBSTITUTION THETA IS A "UNIFIER" FOR A SET (E1, ..., EK) IF AND ONLY IF
? E1THETA = E2THETA = ... = EKTHETA. THE SET (E1, ..., EK) IS "UNIFIABLE" IF
? A UNIFIER EXISTS FOR IT.
?
? A UNIFIER G FOR A SET (E1, ..., EK) OF EXPRESSIONS IS A "MOST GENERAL UNIFIER"
? IF AND ONLY IF FOR EACH UNIFIER THETA FOR THE SET THERE IS A SUBSTITUTION L
? SUCH THAT THETA = G.L
?
? E.G., THE SET (P(A Y), P(X, F(B))) IS UNIFIABLE AS THE SUBSTITUTION THETA 
? = (A/X, F(B)/Y) IS A UNIFIER FOR THE SET.
?
? IF TWO OR MORE LITERALS OF A CLAUSE HAVE A MOST GENERAL UNIFIER G, THEN CG
? IS A "FACTOR" OF C.
?
? IF C1 AND C2 ARE TWO CLAUSES WITH NO VARIABLES IN COMMON, THEN IF L1 AND L2
? ARE TWO LITERALS IN C1 AND C2 RESPECTIVELY, THEN IF L1 AND (NOT L2) HAVE A
? MOST GENERAL UNIFIER G, THEN THE CLAUSE ((C1G - L1G) UNION (C2G - L2G)) IS
? THE "BINARY RESOLVENT" OF C1 AND C2.
?
? E.G., LET C1 = ((P X) (Q X)) AND C2 = ((NOT (P A))(R X)) IN LISP NOTATION.
? THEN THE BINARY RESOLVENT OF C1 AND C2 IS ((P X) (NOT (P A)).
?
? A "RESOLVENT" OF CLAUSES C1 AND C2 IS ONE OF THE FOLLOWING BINARY RESOLVENTS:
?
?   (A) A BINARY RESOLVENT OF C1 AND C2.
?
?   (B) A BINARY RESOLVENT OF C1 AND A FACTOR OF C2.
?
?   (C) A BINARY RESOLVENT OF A FACTOR OF C1 AND C2.
?
?   (D) A BINARY RESOLVENT OF A FACTOR OF C1 AND A FACTOR OF C2.
?
? NOTE THE RECURSIVE NATURE OF THE DEFINITION -- AND THE RESULTANT POTENTIAL
? FOR COMBINATORIAL EXPLOSION.
?
? THE "RESOLUTION PRINCIPLE" IS AN INFERENCE RULE THAT GENERATES RESOLVENTS --
? USUALLY HORDES OF RESOLVENTS -- FROM A SET OF CLAUSES. IT IS, HOWEVER,
? CONSIDERABLY MORE EFFICIENT THAN PROOF METHODS THAT EXPAND USING HERBRAND'S
? THEOREM.
?
? THE THEOREM IS PROVED ONCE THE EMPTY CLAUSE (NIL IN LISP PARLANCE) IS
? GENERATED.
?
? FOLLOWING IS A COMPLETE EXAMPLE:
?
? PROBLEM -- PROVE THAT ALTERNATE INTERIOR ANGLES FORMED BY A DIAGONAL OF A
? TRAPEZOID ARE EQUAL.
?
? FIRST STEP IS TO AXIOMATIZE THE THEOREM:
?
?   LET T(X, Y, U, V) MEAN THAT XYUV IS A TRAPEZOID WITH UPPER-LEFT VERTEX X,
?   UPPER-RIGHT VERTEX Y, LOWER-RIGHT VERTEXT U, AND LOWER-LEFT VERTEX V.
?
?   LET P(X, Y, U, V) MEAN THAT THE LINE SEGMENT XY IS PARALLEL TO THE LINE
?   SEGMENT UV.
?
?   LET E(X, Y, Z, U, V, W) MEAN THAT THE ANGLE XYZ IS EQUAL TO THE ANGLE UVW.
?
? THEN THE FOLLOWING AXIOMS EXIST:
?
?   A1: (FOREACH X)(FOREACH Y)(FOREACH U)(FOREACH V)
?       (T(X, Y, U, V) -> P(X, Y, U, V))               -- DEF. OF TRAPEZOID...
?
?   A2: (FOREACH X)(FOREACH Y)(FOREACH U)(FOREACH V)
?       (P(X, Y, U, V) -> E(X, Y, V, U, V, Y))         -- ALTERNATE INTERIOR
?                                                         ANGLES OF PARALLEL
?                                                         LINES ARE EQUAL
?
?   A3: T(A, B, C, D)
?
? FROM THE AXIOMS, WE NEED TO SHOW THAT E(A, B, D, C, D, B) IS TRUE -- I.E.,
? THAT A1 AND A2 AND A3 -> E(A, B, D, C, D, B) IS A VALID FORMULA.
?
? TO PROVE THIS BY REFUTATION, NEGATE THE CONCLUSION AND PROVE THAT
?
?   A1 AND A2 AND A3 AND -E(A, B, D, C, D, B) IS UNSATISFIABLE.
?
? TRANSFORM THE FORMULA INTO A STANDARD FORM:
?
?   S = ( -T(X, Y, U, V) OR P(X, Y, U, V),
?         -P(X, Y, U, V) OR E(X, Y, V, U, V, Y),
?          T(A, B, C, D),
?         -E(A, B, D, C, D, B) )
?
? THE ABOVE STANDARD FORM S IS A SET OF FOUR CLAUSES. NOW USE RESOLUTION:
?
?   (1) -T(X, Y, U, V) OR P(X, Y, U, V)                -- GIVEN
?   
?   (2) -P(X, Y, U, V) OR E(X, Y, V, U, V, Y)          -- GIVEN
?
?   (3) T(A, B, C, D)                                  -- GIVEN
?
?   (4) -E(A, B, D, C, D, B)                           -- GIVEN
?
?   (5) -P(A, B, C, D)                                 -- RESOLVENT OF 2 AND 4
?
?   (6) -T(A, B, C, D)                                 -- RESOLVENT OF 1 AND 5
?
?   (7) NIL                                            -- RESOLVENT OF 3 AND 6
?
? THE EMPTY CLAUSE SHOWS THAT S IS UNSATISFIABLE AND THAT, THEREFORE, THE
? THEOREM IS PROVED.
?
? IT IS CLEAR THAT THE MOST INTERESTING CHARACTERISTIC OF AN AUTOMATED THEOREM
? PROVER IS IT'S ABILITY TO CONTROL THE RESULTANT COMBINATORIAL EXPLOSION. REAL
? PROBLEMS FROM THE REAL WORLD HAVE TENS, HUNDREDS, THOUSANDS, OR MORE CLAUSES
? -- THESE THINGS MULTIPLY LIKE RABBITS.
?
? THE NAME OF THE GAME IS TO PRUNE THE COMBINATORIAL TREE AND LIMIT -- USUALLY
? WITH VARIOUS HEURISTICS -- THE EXPLOSIVE GROWTH. PERHAPS MCCARTHY'S PAPER
? "PROGRAMS WITH COMMON SENSE" MIGHT BE OF USE HERE...
?
? SEE "SYMBOLIC LOGIC AND MECHANICAL THEOREM PROVING" BY CHANG AND LEE FOR MORE
? DETAILS ON VARIOUS HEURISTICS.
?
? NOW FOR SOME LISP (FINALLY!):
?
?   (BRITISHMUSEUM CLAUSES VARLIST)
?
? RETURNS EITHER '(THEOREM IS VALID) OR NIL (OR A STACK OVERFLOW!) IF NOT.
?
? 'CLAUSES' IS A LIST OF CLAUSES AND 'VARLIST' IS THE LIST OF VARIABLES
? (NOT CONSTANTS).
?
? E.G., FOR THE ABOVE TRAPEZOID THEOREM:
?
?   (BRITISHMUSEUM '( ((NOT (T X Y U V)) (P X Y U V))
?                     ((NOT (P X Y U V)) (E X Y V U V Y))
?                     ((T A B C D))
?                     ((NOT (E A B D C D B))))
?                  '(U V X Y))     ? U, V, X, AND Y ARE VARIABLES. A, B, C, AND
?                                  ? D ARE CONSTANTS.
?
?    -> '(THEOREM IS VALID)
?
? THE "BRITISH MUSEUM ALGORITHM" IS A GENERAL APPROACH TO FIND A SOLUTION IN A
? LARGE SEARCH TREE BY CHECKING ALL POSSIBILITIES ONE BY ONE WITH NO PRUNING
? OR INTELLIGENCE AT ALL -- IT IS SIMPLY A BLIND BREADTH FIRST SEARCH OF THE 
? SEARCH SPACE -- WHICH MIGHT (AND USUALLY IS IN FACT) BE REALLY ENORMOUS. IT'S
? WEAKNESS IS COMBINATORIAL EXPLOSION.
?
? PROVING THE ABOVE THEOREM GENERATES A NUMBER OF GARBAGE COLLECTIONS ON THE 
? UNIVAC 1108.
?
? SEVERAL HEURISTIC SEARCH TECHNIQUES EXIST TO TRY TO LIMIT THE EXPLOSION --
? SUBSUMPTION, SEMANTIC RESOLUTION, LOCK RESOLUTION, AND OTHERS.
?
?   (SUBSUMPTION CLAUSES VARLIST)
?
? IMPLEMENTS ONE HEURISTIC -- SUBSUMPTION.
?
? OTHERS ARE NOT DIFFICULT TO IMPLEMENT WITH THE BASE PROVIDED HERE.
?
????????????????????????????????????????????????????????????????????????????????


(DEFINE '(

 (BRITISHMUSEUM (LAMBDA (CLAUSES VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((NULL (SETQ RESULT (BRITISHMUSEUM2 (CAR CLAUSES) 
                                              (CDR CLAUSES) VARLIST)))
              (BRITISHMUSEUM (CDR CLAUSES) VARLIST))
          ((EQ (CAR (REVERSE RESULT)) (QUOTE THEOREM)) 
              (QUOTE (THEOREM IS VALID)))
          (T (APPEND RESULT (BRITISHMUSEUM (CDR CLAUSES) VARLIST))))))

 (BRITISHMUSEUM2 (LAMBDA (CLAUSE CLAUSES VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((NULL (SETQ RESULT (RESOLVE CLAUSE (CAR CLAUSES) VARLIST)))
              (QUOTE (THEOREM)))
          ((EQUAL (PLUS (LENGTH CLAUSE) (LENGTH (CAR CLAUSES))) (LENGTH RESULT))
              (BRITISHMUSEUM2 CLAUSE (CDR CLAUSES) VARLIST))
          (T (CONS RESULT (BRITISHMUSEUM2 CLAUSE (CDR CLAUSES) VARLIST))))))

 (CLASS (LAMBDA (CLAUSES FNAMESS)
    (COND ((NULL FNAMESS) FNAMESS)
          (T (LIST (CLASS2 CLAUSES (CAR FNAMESS))
                   (CLASS CLAUSES (CDR FNAMESS)))))))

 (CLASS2 (LAMBDA (CLAUSES FNAMES)
    (COND ((NULL CLAUSES) CLAUSES)
          ((MEMBER$ FNAMES (CAR CLAUSES))
              (CONS (CAR CLAUSES) (CLASS2 (CDR CLAUSES) FNAMES)))
          (T (CLASS2 (CDR CLAUSES) FNAMES)))))

 (CONTAIN (LAMBDA (ELEMENT ELEMENTS)
    (COND ((NULL ELEMENT) T)
          ((NULL (CONTAIN2 (CAR ELEMENT) ELEMENTS))
              (CONTAIN (CDR ELEMENT) ELEMENTS))
          (T NIL))))

 (CONTAIN2 (LAMBDA (ELEMENT ELEMENTS)
    (COND ((NULL ELEMENTS) T)
          ((EQUAL ELEMENT (CAR ELEMENTS)) NIL)
          (T (CONTAIN2 ELEMENT (CDR ELEMENTS))))))

 (DISAGREE (LAMBDA (CLAUSE1 CLAUSE2)
    (COND ((NULL CLAUSE1) CLAUSE1)
          ((OR (ATOM CLAUSE1)
               (ATOM CLAUSE2))
             (COND ((EQUAL CLAUSE1 CLAUSE2) NIL)
                   (T (LIST CLAUSE1 CLAUSE2))))
          ((EQUAL (CAR CLAUSE1) (CAR CLAUSE2))
             (DISAGREE (CDR CLAUSE1) (CDR CLAUSE2)))
          ((ATOM (CAR CLAUSE1)) (LIST (CAR CLAUSE1) (CAR CLAUSE2)))
          ((ATOM (CAR CLAUSE2)) (LIST (CAR CLAUSE1) (CAR CLAUSE2)))
          (T (DISAGREE (CAR CLAUSE1) (CAR CLAUSE2))))))

 (EXIST (LAMBDA (DIS DISSA VARLIST)
    (COND ((NULL DIS) DIS)
          ((NOT (ATOM (CAR DIS))) (EXIST (CDR DIS) DISSA VARLIST))
          ((NOT (MEMBER (CAR DIS) VARLIST)) (EXIST (CDR DIS) DISSA VARLIST))
          ((NULL (SETQ A (EXIST2 (CAR DIS) DISSA)))
             (EXIST (CDR DIS) DISSA VARLIST))
          (T A))))

 (EXIST2 (LAMBDA (DIS DISSA)
    (COND ((NULL DISSA) DISSA)
          ((EQUAL DIS (CAR DISSA)) (EXIST2  DIS (CDR DISSA)))
          ((MEMBER$ DIS (CAR DISSA)) (EXIST2 DIS (CDR DISSA)))
          (T (LIST (CAR DISSA) DIS)))))

 (FNAME (LAMBDA (CLAUSES)
    (COND ((NULL CLAUSES) CLAUSES)
          ((ATOM (CAR CLAUSES))
              (COND ((EQ (CAR CLAUSES) (QUOTE NOT)) (FNAME (CADR CLAUSES)))
                    (T (CAR CLAUSES))))
          (T (CONS (FNAME (CAR CLAUSES)) (FNAME (CDR CLAUSES)))))))

 (GENERATE (LAMBDA (CLAUSES VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((EQ (CAR (REVERSE (CONS (SETQ RESULT (GENERATE2 (CAR CLAUSES)
                                                           (CDR CLAUSES)
                                                           VARLIST))
                                   NIL)))
               (QUOTE THEOREM)) NIL)
          (T (CONS (RESULT (GENERATE (CDR CLAUSES) VARLIST)))))))

 (GENERATE2 (LAMBDA (CLAUSE CLAUSES VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((EQUAL CLAUSE (CAR CLAUSES))
               (GENERATE2 CLAUSE (CDR CLAUSES) VARLIST))
          ((NULL (SETQ RESULT (RESOLVE CLAUSE (CAR CLAUSES) VARLIST)))
              (QUOTE THEOREM))
          (T (CONS RESULT (GENERATE2 CLAUSE (CDR CLAUSES) VARLIST))))))

 (HASH (LAMBDA (SUPERCLAUSES)
    (COND ((NULL SUPERCLAUSES) SUPERCLAUSES)
          (T (APPEND (CAR SUPERCLAUSES) (HASH (CDR SUPERCLAUSES)))))))

 (HEURISTIC1 (LAMBDA (CLAUSES VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((ATOM CLAUSES) CLAUSES)
          ((NULL (SETQ FNAMES (SHRINK (HASH (FNAME CLAUSES))))) FNAMES)
          (T (HEURISTIC1A (PURITY (CLASS CLAUSES FNAMES)) FNAMES VARLIST)))))

 (HEURISTIC1A (LAMBDA (SUPERCLAUSES FNAMES VARLIST)
    (COND ((NULL (SETQ RESULT (GENERATE SUPERCLAUSES VARLIST))) (QUOTE THEOREM))
          (T (HEURISTIC1A (CLASS (PURITY (SHRINK (HASH RESULT)) FNAMES))
                          FNAMES VARLIST)))))

 (INTERSECTION (LAMBDA (X Y)
    (COND ((NULL X) X)
          ((ATOM (CAR X))
              (COND ((MEMBER$ (CAR X) Y) 
                         (CONS (CAR X) (INTERSECTION (CDR X) Y)))
                    (T (INTERSECTION (CDR X) Y))))
          ((NULL (SETQ Z (INTERSECTION (CAR X) Y))) (INTERSECTION (CDR X) Y))
          ((ATOM Z) (CONS Z (INTERSECTION (CDR X) Y)))
          (T (APPEND Z (INTERSECTION (CDR X) Y))))))

 (MEMBER$ (LAMBDA (AA BB)
    (COND ((NULL BB) BB)
          ((ATOM BB)
              (COND ((EQ AA BB) T)
                    (T NIL)))
          ((ATOM (CAR BB))
              (COND ((EQ AA (CAR BB)) T)
                    (T (MEMBER$ AA (CDR BB)))))
          ((MEMBER$ AA (CAR BB)) T)
          (T (MEMBER$ AA (CDR BB))))))

 (PACK (LAMBDA (ARG)
    (COND ((NULL ARG) ARG)
          ((ATOM ARG) ARG)
          ((NULL (CDR ARG)) ARG)
          ((MEMBER$ (CAR ARG) (CDR ARG)) (PACK (CDR ARG)))
          (T (CONS (CAR ARG) (PACK (CDR ARG)))))))

 (PURITY (LAMBDA (SUPERCLAUSE)
    (COND ((NULL SUPERCLAUSE) SUPERCLAUSE)
          ((NULL (CDAR SUPERCLAUSE)) (PURITY (CDR SUPERCLAUSE)))
          (T (CONS (CAR SUPERCLAUSE) (PURITY (CDR SUPERCLAUSE)))))))

 (REPLACE (LAMBDA(CLAUSE REPS)
    (COND ((NULL REPS) CLAUSE)
          (T (REPLACE (REPLACE$ CLAUSE (CAR REPS)) (CDR REPS))))))

 (REPLACE$ (LAMBDA (CLAUSE REP)
    (COND ((NULL REP) CLAUSE)
          ((NULL CLAUSE) CLAUSE)
          ((ATOM CLAUSE)
              (COND ((EQ CLAUSE (CADR REP)) (CAR REP))
                    (T CLAUSE)))
          (T (CONS (REPLACE$ (CAR CLAUSE) REP)
                   (REPLACE$ (CDR CLAUSE) REP))))))

 (RESBIN (LAMBDA (CLAUSE LITERAL)
    (COND ((NULL CLAUSE) CLAUSE)
          ((EQUAL (CAR CLAUSE) LITERAL) (CDR CLAUSE))
          (T (CONS (CAR CLAUSE) (RESBIN (CDR CLAUSE) LITERAL))))))

 (RESOLVE (LAMBDA (CLAUSE1 CLAUSE2 VARLIST)
    (COND ((NULL CLAUSE1) CLAUSE2)
          ((NULL CLAUSE2) CLAUSE1)
          ((NULL (SETQ INTERMEDIATE (RESPAR CLAUSE1 CLAUSE2))) NIL)
          (T (RESOLVE$ CLAUSE1 CLAUSE2 INTERMEDIATE
                       (SPLITOUT INTERMEDIATE) VARLIST)))))

 (RESOLVE$ (LAMBDA (CLAUSE1 CLAUSE2 RESBINPAR RESBEN VARLIST)
    (COND ((NULL RESBINPAR) (UNION CLAUSE1 CLAUSE2))
          ((EQUAL (CAAR RESBEN) (CADAR RESBEN))
               (RESOLVE$ (RESBIN CLAUSE1 (CAAR RESBINPAR))
                         (RESBIN CLAUSE2 (CADAR RESBINPAR)) (CDR RESBINPAR)
                         (CDR RESBEN) VARLIST))
          ((NULL (SETQ UNIFIER (UNIFY (CAR RESBEN) VARLIST)))
               (RESOLVE$ CLAUSE1 CLAUSE2 (CDR RESBINPAR) (CDR RESBEN) VARLIST))
          (T (RESOLVE$ (RESBIN (REPLACE CLAUSE1 UNIFIER)
                               (REPLACE (CAAR RESBINPAR) UNIFIER))
                       (RESBIN (REPLACE CLAUSE2 UNIFIER)
                               (REPLACE (CADAR RESBINPAR) UNIFIER))
                       (CDR RESBINPAR)
                       (CDR RESBEN) VARLIST)))))

 (RESPAR (LAMBDA (CLAUSE1 CLAUSE2)
    (COND ((NULL CLAUSE1) CLAUSE1)
          ((NULL (SETQ A (RESPAR$ (CAR CLAUSE1) CLAUSE2)))
               (RESPAR (CDR CLAUSE1) CLAUSE2))
          (T (CONS (LIST (CAR CLAUSE1) A)
                   (RESPAR (CDR CLAUSE1) CLAUSE2))))))

 (RESPAR$ (LAMBDA (SUBCLAUSE CLAUSE)
    (COND ((NULL CLAUSE) CLAUSE)
          ((EQ (CAR SUBCLAUSE) (QUOTE NOT))
               (COND ((EQ (CAAR CLAUSE) (QUOTE NOT))
                          (RESPAR$ SUBCLAUSE (CDR CLAUSE)))
                     ((NOT (EQ (CAADR SUBCLAUSE) (CAAR CLAUSE)))
                          (RESPAR$ SUBCLAUSE (CDR CLAUSE)))
                     (T (CAR CLAUSE))))
          ((NOT (EQ (CAAR CLAUSE) (QUOTE NOT)))
               (RESPAR$ SUBCLAUSE (CDR CLAUSE)))
          ((NOT (EQ (CAR SUBCLAUSE) (CAADAR CLAUSE)))
               (RESPAR$ SUBCLAUSE (CDR CLAUSE)))
          (T (CAR CLAUSE)))))

 (SHRINK (LAMBDA (THINGS)
    (COND ((NULL THINGS) THINGS)
          ((MEMBER (CAR THINGS) (CDR THINGS)) (SHRINK (CDR THINGS)))
          (T (CONS (CAR THINGS) (SHRINK (CDR THINGS)))))))


 (SPLITOUT (LAMBDA (RESBINPAR)
    (COND ((NULL RESBINPAR) RESBINPAR)
          ((EQ (CAAAR RESBINPAR) (QUOTE NOT))
              (CONS (APPEND (CONS (CADAAR RESBINPAR) NIL)
                            (CONS (CADAR RESBINPAR) NIL))
                    (SPLITOUT (CDR RESBINPAR))))
          (T (CONS (APPEND (CONS (CAAR RESBINPAR) NIL)
                           (CONS (CADADAR RESBINPAR) NIL))
                   (SPLITOUT (CDR RESBINPAR)))))))

 (SUBSTITUTE (LAMBDA (X Y Z)
    (COND ((NULL Z) Z)
          ((ATOM (CAR Z))
              (COND (( EQ Y (CAR Z)) (CONS X (SUBSTITUTE X Y (CDR Z))))
                    (T (CONS (CAR Z) (SUBSTITUTE X Y (CDR Z))))))
          (T (CONS (SUBSTITUTE X Y (CAR Z)) (SUBSTITUTE X Y (CDR Z)))))))

 (SUBSUME (LAMBDA (CLAUSES CLAUSE VARLIST)
    (COND ((NULL CLAUSE) CLAUSES)
          (T (SUBSUME (SUBSUME2 (RESBIN CLAUSES (CAR CLAUSE)) 
                                (CAR CLAUSE)
                                VARLIST)
                      (CDR CLAUSE)
                      VARLIST)))))

 (SUBSUME2 (LAMBDA (CLAUSES CLAUSE VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((EQUAL CLAUSE (CAR CLAUSE)) (CDR CLAUSES))
          ((NULL (SETQ UNIFIER (UNIFY (LIST CLAUSE (CAR CLAUSES)) VARLIST)))
              (CONS (CAR CLAUSES) (SUBSUME2 (CDR CLAUSES) CLAUSE VARLIST)))
          ((CONTAIN (REPLACE CLAUSE UNIFIER) CLAUSES) (CDR CLAUSES))
          (T (CONS (CAR CLAUSES) (SUBSUME2 (CDR CLAUSES) CLAUSE VARLIST))))))

 (SUBSUMPTION (LAMBDA (CLAUSES VARLIST)
    (SUBSUME CLAUSES CLAUSES VARLIST)))

 (UNIFY (LAMBDA(CLAUSES VARLIST)
    (COND ((NULL CLAUSES) CLAUSES)
          ((ATOM CLAUSES) NIL)
          ((NULL (SETQ AB (UNIFY$ CLAUSES VARLIST))) AB)
          ((EQ AB (QUOTE (NOT-UNIFIABLE))) NIL)
          ((EQ (CAR (REVERSE AB)) (QUOTE NOT-UNIFIABLE)) NIL)
          (T AB))))

 (UNIFY$ (LAMBDA( CLAUSES VARLIST)
     (COND ((NULL CLAUSES) CLAUSES)
           ((NULL (SETQ DIS (DISAGREE (CAR CLAUSES) (CADR CLAUSES)))) NIL)
           ((NULL (SETQ SUB (EXIST DIS DIS VARLIST))) (QUOTE (NOT-UNIFIABLE)))
           (T (CONS SUB (UNIFY$ (REPLACE CLAUSES (CONS SUB NIL)) VARLIST))))))

 (UNION (LAMBDA (X Y)
    (COND ((NULL X) Y)
          ((NULL Y) X)
          ((ATOM (CAR X))
              (COND ((MEMBER$ (CAR X) Y) (UNION (CDR X) Y))
                    (T (CONS (CAR X) (UNION (CDR X) Y)))))
          ((MEMBER (CAR X) Y) (UNION (CDR X) Y))
          (T (CONS (CAR X) (UNION (CDR X) Y))))))

 (UNIQVAR (LAMBDA (CLAUSE1 CLAUSE2 VARLIST)
    (UNIQVAR$ (PACK (INTERSECTION (INTERSECTION CLAUSE1 CLAUSE2) VARLIST))
              CLAUSE1 CLAUSE2 VARLIST)))

 (UNIQVAR$ (LAMBDA (COM CLAUSE1 CLAUSE2 VARLIST)
    (COND ((NULL COM) (LIST CLAUSE1 CLAUSE2 VARLIST))
          ((NULL (SETQ G (GENSYM))) NIL)
          (T (UNIQVAR$ (CDR COM) (SUBSTITUTE G (CAR COM) CLAUSE1 ) CLAUSE2
                                 (APPEND VARLIST (CONS G NIL)))))))


))