(DEFINE-FILE-INFO READTABLE "interlisp" PACKAGE "USER")

(IL:FILECREATED "26-Apr-88 09:21:16" IL:{DSK}<LISPFILES>LOGIC>LOGIC.;3
 29694  

      IL:changes IL:to%:  (IL:FUNCTIONS CREATE-BACKGROUND-THEORY)

      IL:previous IL:date%: "14-Mar-88 10:19:39" IL:{DSK}<LISPFILES>LOGIC>LOGIC.;2)


(IL:* "
Copyright (c) 1988 by Roberto Ghislanzoni.  All rights reserved.
")

(IL:PRETTYCOMPRINT IL:LOGICCOMS)

(IL:RPAQQ IL:LOGICCOMS
 
          ((IL:FUNCTIONS ADD-OR-LEVEL ALL ALL-PREDICATES ALL-PREDS ALL-SAS ALL-SEMANTIC-ATTACHMENTS 
                  AND-LEVEL ANTEC ANY ATOMIC-FORMULAP ATTACH CLAUSES-OR CLEAR-AND-LEVEL CONJ CONSEQ 
                  CONSEQP CREATE-BACKGROUND-THEORY CREATE-THEORY DELETE-OR-NODE 
                  DELETE-OR-NODE-WITH-CUT DIRECTLY-IMPLEMENTED FAILEDP FIND-CLAUSES FORMULA-OR 
                  GET-AND-NODE-THEORIES GET-CUT GET-OR-NODE-THEORIES GET-THEORY IMPLICATIONP 
                  IS-THERE-CUT LIST-ALL-THEORIES LOAD-THEORY LOGIC-ADD LOGIC-ASSERT LOGIC-DELETE 
                  LOGIC-PROVE MAKE-AND-NODE MAKE-OR-NODE MAKE-TREE MERGE-INTERNAL MERGE-THEORIES 
                  NEW-TREE NULL-AND-LEVELP NULL-OR-LEVELP NULL-TREEP OR-LEVELS PREDICATE PROVE 
                  RENAME-CUT SAVE-THEORY SEMANTIC-ATTACHMENT-P SHOW-DEFINITION SHOW-THEORY SOLVE 
                  SUBSTITUTE-LEVEL THEORYP UNIF-ENV-OR UNIFICATION-ENV UPDATE-ENV UPDATE-LEVEL 
                  UPDATE-TREE)
           (IL:VARS *PRINT-PRETTY*)
           (IL:P (IL:FILESLOAD UNIFIER))))

(DEFUN ADD-OR-LEVEL
 (WFF CLAUSES TREE &OPTIONAL CUTNAME) 
          
          (IL:* IL:;; 

          "Adds a new or-node to the list of the nodes. The new node is put in front of the old ones")

 [COND
    ((NULL CLAUSES)
     TREE)
    (T (LET* ((LEVEL (AND-LEVEL TREE))
              (NEW-OR-NODE (MAKE-OR-NODE WFF CLAUSES (CONJ LEVEL)
                                  (UNIFICATION-ENV LEVEL)
                                  (GET-AND-NODE-THEORIES LEVEL)
                                  CUTNAME)))
             (MAKE-TREE LEVEL (APPEND (LIST NEW-OR-NODE)
                                     (OR-LEVELS TREE])


(DEFUN ALL
 (VARS CONJ THS) [PROG (RESULTING-TREE (TREE (MAKE-TREE (MAKE-AND-NODE
                                                                   CONJ NIL
                                                                   (APPEND (LIST '*BACKGROUND-THEORY*
                                                                                 )
                                                                          THS))
                                                              NIL))
                                        COLLECTED-RESULTS NEXT-OR)
                             HERE
                                 (SETF RESULTING-TREE (LOGIC-PROVE TREE))
                                 (COND
                                    ((NULL RESULTING-TREE)
                                     (RETURN COLLECTED-RESULTS))
                                    (T [SETF COLLECTED-RESULTS
                                             (APPEND COLLECTED-RESULTS
                                                    (LIST (LOOKUP VARS (UNIFICATION-ENV (AND-LEVEL
                                                                                         
                                                                                       RESULTING-TREE
                                                                                         ]
                                       (SETF NEXT-OR (FIRST (OR-LEVELS RESULTING-TREE)))
                                       (SETF TREE (SOLVE (NEW-TREE RESULTING-TREE NEXT-OR)
                                                         (FORMULA-OR NEXT-OR)
                                                         (CLAUSES-OR NEXT-OR)))
                                       (GO HERE])


(DEFUN ALL-PREDICATES
 (THEORY-NAME) (ALL-PREDS (GET-THEORY THEORY-NAME)))


(DEFUN ALL-PREDS
 (THEORY) 
          
          (IL:* IL:;; "The presence of VAL in the AND body is necessary because it is correct to test if the predicates has not  been erased: in such a case its value is NIL")

 (PROG (PRNAMES)
   LABEL
       (MAPHASH #'[LAMBDA (KEY VAL)
                         (AND (NOT (SEMANTIC-ATTACHMENT-P VAL))
                              VAL
                              (SETF PRNAMES (APPEND PRNAMES (LIST KEY] THEORY)
       (RETURN PRNAMES)))


(DEFUN ALL-SAS
 (THEORY) (PROG (SANAMES)
                          LABEL
                              (MAPHASH #'[LAMBDA (KEY VAL)
                                                (AND (SEMANTIC-ATTACHMENT-P VAL)
                                                     VAL
                                                     (SETF SANAMES (APPEND SANAMES (LIST KEY] THEORY)
                              (RETURN SANAMES)))


(DEFUN ALL-SEMANTIC-ATTACHMENTS
 (THEORY-NAME) (ALL-SAS (GET-THEORY THEORY-NAME)))


(DEFMACRO AND-LEVEL
 (TREE) `(CAR ,TREE))


(DEFMACRO ANTEC
 (WFF) `(CDDR ,WFF))


(DEFUN ANY
 (HOW-MANY VARS CONJ THS) [PROG (RESULTING-TREE
                                           (COUNTER 0)
                                           (TREE (MAKE-TREE (MAKE-AND-NODE CONJ NIL
                                                                   (APPEND (LIST '*BACKGROUND-THEORY*
                                                                                 )
                                                                          THS))
                                                        NIL))
                                           COLLECTED-RESULTS NEXT-OR)
                                      HERE
                                          (SETF RESULTING-TREE (LOGIC-PROVE TREE))
                                          (COND
                                             ((OR (NULL RESULTING-TREE)
                                                  (EQ COUNTER HOW-MANY))
                                              (RETURN COLLECTED-RESULTS))
                                             (T [SETF COLLECTED-RESULTS
                                                      (APPEND COLLECTED-RESULTS
                                                             (LIST (LOOKUP VARS (UNIFICATION-ENV
                                                                                 (AND-LEVEL 
                                                                                       RESULTING-TREE
                                                                                        ]
                                                (SETF NEXT-OR (FIRST (OR-LEVELS RESULTING-TREE)))
                                                (SETF TREE (SOLVE (NEW-TREE RESULTING-TREE NEXT-OR)
                                                                  (FORMULA-OR NEXT-OR)
                                                                  (CLAUSES-OR NEXT-OR)))
                                                (INCF COUNTER)
                                                (GO HERE])


(DEFMACRO ATOMIC-FORMULAP
 (WFF) `[AND (LISTP ,WFF)
                                      (NULL (SECOND ,WFF])


(DEFUN ATTACH
 (SA-NAME DEFINITION THEORY-NAME &OPTIONAL WINDOW) (SETF (GETHASH SA-NAME
                                                                             (GET-THEORY THEORY-NAME 
                                                                                    WINDOW))
                                                                      (CONS 'SA DEFINITION))
                                                                'ATTACHED)


(DEFMACRO CLAUSES-OR
 (OR-NODE) `(SECOND ,OR-NODE))


(DEFUN CLEAR-AND-LEVEL
 (TREE) (PROGN (SETF (CAR TREE)
                                           NIL)
                                     TREE))


(DEFMACRO CONJ
 (AND-LEVEL) `(CAR ,AND-LEVEL))


(DEFUN CONSEQ
 (WFF) (CAR WFF))


(DEFMACRO CONSEQP
 (C) `[AND (LISTP ,C)
                            (SYMBOLP (CAR ,C])


(DEFUN CREATE-BACKGROUND-THEORY
 NIL [PROGN (IN-PACKAGE 'USER)
                                           (CREATE-THEORY '*BACKGROUND-THEORY*)
                                           (WITH-OPEN-FILE (FILE (MERGE-PATHNAMES (MAKE-PATHNAME
                                                                                   :NAME
                                                                                   'MAIN :TYPE
                                                                                   'LGC))
                                                                 :DIRECTION :INPUT)
                                                  (PROG (NAME)
                                                    LABEL
                                                        (AND (EQ (SETF NAME (READ FILE))
                                                                 'THEORY-END)
                                                             (RETURN))
                                                        (LOGIC-ASSERT NAME (CONS '
                                                                                 DIRECTLY-IMPLEMENTED
                                                                                 (READ FILE))
                                                               '*BACKGROUND-THEORY*)
                                                        (GO LABEL])


(DEFUN CREATE-THEORY
 (THEORY-NAME) (SETF (GET 'THEORY THEORY-NAME)
                                         (MAKE-HASH-TABLE))
                                   THEORY-NAME)


(DEFUN DELETE-OR-NODE
 (TAGNODE NODES) (DELETE TAGNODE NODES :TEST #'EQUAL :COUNT 1))


(DEFUN DELETE-OR-NODE-WITH-CUT
 (CUTNAME OR-LEVELS) 
          
          (IL:* IL:;; "This function is called every time a cut is proven: all the alternatives for that clause MUST be erased. Remember that every cut has a unique identifier")

 [PROG ((NODES OR-LEVELS))
   LABEL
       (COND
          ((NULL NODES)
           OR-LEVELS)
          ((EQ (GET-CUT (CAR NODES))
               CUTNAME)
           (RETURN (DELETE-OR-NODE (CAR NODES)
                          OR-LEVELS)))
          (T (SETF NODES (CDR NODES))
             (GO LABEL])


(DEFMACRO DIRECTLY-IMPLEMENTED
 (CLAUSES) `(EQ (CAR ,CLAUSES)
                                              'DIRECTLY-IMPLEMENTED))


(DEFMACRO FAILEDP
 (ENV) `(EQ ,ENV 'FAILED))


(DEFUN FIND-CLAUSES
 (PREDICATE-NAME THEORY-NAMES &OPTIONAL WINDOW)
   [PROG NIL
     LABEL
         (COND
            ((NULL THEORY-NAMES)
             (RETURN NIL))
            (T (LET* ((TH (FIRST THEORY-NAMES))
                      (CLAUSES (BINDING PREDICATE-NAME TH WINDOW)))
                     (COND
                        ((NULL CLAUSES)
                         (SETF THEORY-NAMES (CDR THEORY-NAMES))
                         (GO LABEL))
                        (T (RETURN CLAUSES])


(DEFMACRO FORMULA-OR
 (OR-LEVEL) `(CAR ,OR-LEVEL))


(DEFMACRO GET-AND-NODE-THEORIES
 (AND-NODE) `(THIRD ,AND-NODE))


(DEFMACRO GET-CUT
 (OR-NODE) `(SIXTH ,OR-NODE))


(DEFMACRO GET-OR-NODE-THEORIES
 (OR-NODE) `(FIFTH ,OR-NODE))


(DEFMACRO GET-THEORY
 (THEORY-NAME &OPTIONAL WINDOW) `(OR (AND ,WINDOW (GET-THEORY-INTERNAL
                                                                       ,THEORY-NAME
                                                                       ,WINDOW))
                                                         (GET 'THEORY ,THEORY-NAME)))


(DEFMACRO IMPLICATIONP
 (WFF) `[LET [(SEPARATOR (SECOND ,WFF]
                                   (AND (EQ SEPARATOR ':-)
                                        (NOT (NULL (CDDR ,WFF])


(DEFUN IS-THERE-CUT
 (CONJS) [OR (MEMBER '! CONJS)
                                (PROG ((ELTS CONJS))
                                  LABEL
                                      (COND
                                         ((NULL ELTS)
                                          NIL)
                                         ((AND (SYMBOLP (CAR ELTS))
                                               (EQ (CHAR-CODE (CHAR (SYMBOL-NAME (CAR ELTS))
                                                                    0))
                                                   33))
                                          (RETURN T))
                                         (T (SETF ELTS (CDR ELTS))
                                            (GO LABEL])


(DEFUN LIST-ALL-THEORIES
 (&OPTIONAL WINDOW) [OR (AND WINDOW (LIST-ALL-THEORIES-INTERNAL WINDOW))
                                                (DO ((LL (SYMBOL-PLIST 'THEORY)
                                                         (CDDR LL))
                                                     (RESULT NIL))
                                                    ((NULL LL)
                                                     RESULT)
                                                    (SETF RESULT (APPEND RESULT (LIST (CAR LL])


(DEFUN LOAD-THEORY
 (THEORY-NAME &OPTIONAL WINDOW)
   [LET [(THEORY-FILE (MERGE-PATHNAMES (MAKE-PATHNAME :NAME THEORY-NAME :TYPE 'LGC]
        (OR (AND WINDOW (LOAD-DEVEL-THEORY WINDOW THEORY-NAME))
            (OR [AND (PROBE-FILE THEORY-FILE)
                     (WITH-OPEN-FILE (FILE THEORY-FILE :DIRECTION :INPUT)
                            (PROG (THEORY-NAME PRED-NUMBER SAS-NUMBER)
                                  (SETF THEORY-NAME (READ FILE))
                                  (CREATE-THEORY THEORY-NAME)
                                  (SETF SAS-NUMBER (READ FILE))
                                  (DO ((SAS SAS-NUMBER (DECF SAS)))
                                      ((EQ SAS 0)
                                       NIL)
                                      (SETF (GETHASH (READ FILE)
                                                   (GET 'THEORY THEORY-NAME))
                                            (READ FILE)))
                                  (SETF PRED-NUMBER (READ FILE))
                                  (DO ((PREDS PRED-NUMBER (DECF PREDS)))
                                      ((EQ PREDS 0)
                                       NIL)
                                      (SETF (GETHASH (READ FILE)
                                                   (GET 'THEORY THEORY-NAME))
                                            (READ FILE)))
                                  (RETURN 'LOADED]
                (FORMAT T "Theory not found"])


(DEFUN LOGIC-ADD
 (PRED CLAUSES THEORY &OPTIONAL WINDOW) (PROGN (SETF (GETHASH PRED (GET-THEORY THEORY 
                                                                                          WINDOW))
                                                                     (APPEND (GETHASH PRED
                                                                                    (GET-THEORY
                                                                                     THEORY WINDOW))
                                                                            CLAUSES))
                                                               'ADDED))


(DEFUN LOGIC-ASSERT
 (PREDICATE-NAME CLAUSES THEORY-NAME &OPTIONAL WINDOW) (SETF (GETHASH 
                                                                                       PREDICATE-NAME
                                                                                       (GET-THEORY
                                                                                        THEORY-NAME 
                                                                                        WINDOW))
                                                                                CLAUSES)
                                                                          'ASSERTED)


(DEFUN LOGIC-DELETE
 (PRED-OR-SA THEORY-NAME &OPTIONAL WINDOW) (PROGN (SETF (GETHASH PRED-OR-SA
                                                                                  (GET-THEORY 
                                                                                         THEORY-NAME 
                                                                                         WINDOW))
                                                                           NIL)
                                                                     'DELETED))


(DEFUN LOGIC-PROVE
 (TREE &OPTIONAL WINDOW)
   [PROG NIL
     JUMP
         (COND
            ((NULL-TREEP TREE)
             (RETURN NIL))
            [(NULL-AND-LEVELP TREE)
             (LET [(NEXT-OR (FIRST (OR-LEVELS TREE]
          
          (IL:* IL:;; 

          "Gets the next or-node: we have now no strategy for choosing it; maybe later...")


                  (COND
                     ((NULL NEXT-OR)
                      (SETF TREE (LIST NIL NIL))
                      (GO JUMP))
                     (T (SETF TREE (SOLVE (NEW-TREE TREE NEXT-OR)
                                          (FORMULA-OR NEXT-OR)
                                          (CLAUSES-OR NEXT-OR)
                                          NIL WINDOW))
                        (GO JUMP]
            (T (LET ((NEXT-LEVEL (AND-LEVEL TREE)))
                    (COND
                       ((NULL (CONJ NEXT-LEVEL))
                        (RETURN TREE))
                       (T (LET* [(TO-PROVE (FIRST (CONJ NEXT-LEVEL)))
                                 (THS (GET-AND-NODE-THEORIES NEXT-LEVEL))
                                 (CLAUSES (FIND-CLAUSES (PREDICATE TO-PROVE)
                                                 THS WINDOW))
                                 (CUT? (IS-THERE-CUT (REST (CONJ NEXT-LEVEL]
                                (SETF TREE (SOLVE (UPDATE-TREE (UPDATE-LEVEL NEXT-LEVEL TO-PROVE)
                                                         TREE)
                                                  TO-PROVE CLAUSES CUT? WINDOW))
                                (GO JUMP])


(DEFUN MAKE-AND-NODE
 (CONJ UNIF-ENV THEORIES) (LIST CONJ UNIF-ENV THEORIES))


(DEFUN MAKE-OR-NODE
 (WFF CLAUSES BORDER UNIF-ENV THEORIES &OPTIONAL CUTNAME) (LIST WFF CLAUSES BORDER 
                                                                                   UNIF-ENV THEORIES 
                                                                                   CUTNAME))


(DEFUN MAKE-TREE
 (AND-LEVEL OR-LEVELS) (LIST AND-LEVEL OR-LEVELS))


(DEFUN MERGE-INTERNAL
 (NEW-THEORY-NAME THEORIES &OPTIONAL WINDOW)
   [PROGN (IL:* IL:;; "Merges the specified theories in to a new-brand theory")


          (LET ((ACTUAL-THEORY (GET-THEORY NEW-THEORY-NAME WINDOW)))
               (DO ((THS THEORIES (CDR THS)))
                   ((NULL THS)
                    'MERGED)
                   (AND (THEORYP (CAR THS)
                               WINDOW)
                        (MAPHASH #'(LAMBDA (KEY VAL)
                                          (AND VAL (SETF (GETHASH KEY ACTUAL-THEORY)
                                                         VAL))) (GET-THEORY (CAR THS)
                                                                       WINDOW])


(DEFUN MERGE-THEORIES
 (NEW-THEORY-NAME &REST LIST-OF-THEORIES) (PROGN (CREATE-THEORY NEW-THEORY-NAME)
                                                                      (MERGE-INTERNAL NEW-THEORY-NAME 
                                                                             LIST-OF-THEORIES)
                                                                      'MERGED))


(DEFUN NEW-TREE
 (TREE OR-NODE) (MAKE-TREE (MAKE-AND-NODE (THIRD OR-NODE)
                                                 (UNIF-ENV-OR OR-NODE)
                                                 (GET-OR-NODE-THEORIES OR-NODE))
                                      (DELETE-OR-NODE OR-NODE (OR-LEVELS TREE))))


(DEFMACRO NULL-AND-LEVELP
 (TREE) `(NULL (CAR ,TREE)))


(DEFMACRO NULL-OR-LEVELP
 (TREE) `(NULL (SECOND ,TREE)))


(DEFMACRO NULL-TREEP
 (TREE) `(AND (NULL-AND-LEVELP ,TREE)
                                  (NULL-OR-LEVELP ,TREE)))


(DEFMACRO OR-LEVELS
 (TREE) `(SECOND ,TREE))


(DEFUN PREDICATE
 (WFF) (COND
                          ((LISTP WFF)
                           (CAR WFF))
                          (T WFF)))


(DEFUN PROVE
 (CONJ THS) (LET [(RESULT (LOGIC-PROVE (MAKE-TREE (MAKE-AND-NODE
                                                               CONJ NIL (APPEND (LIST '
                                                                                  *BACKGROUND-THEORY*
                                                                                      )
                                                                               THS))
                                                          NIL]
                             (COND
                                ((NULL RESULT)
                                 NIL)
                                (T T))))


(DEFUN RENAME-CUT
 (ANTECS) 
          
          (IL:* IL:;; "This function returns a CONS with CAR as the renamed cut and CDR as the list of antecs with the cut renamed")

 [DO ((TEMPVAR ANTECS (CDR TEMPVAR))
      (RESULTS NIL)
      (CUT-RENAMED NIL))
     ((NULL TEMPVAR)
      (CONS CUT-RENAMED RESULTS))
     (COND
        [(EQ (CAR TEMPVAR)
             '!)
         (SETF CUT-RENAMED (GENSYM "!"))
         (SETF RESULTS (APPEND RESULTS (LIST CUT-RENAMED]
        (T (SETF RESULTS (APPEND RESULTS (LIST (CAR TEMPVAR])


(DEFUN SAVE-THEORY
 (THEORY-NAME &OPTIONAL WINDOW)
   [LET ((THEORY (GET-THEORY THEORY-NAME WINDOW)))
        (COND
           ((NOT (THEORYP THEORY))
            'ERROR)
           (T (WITH-OPEN-FILE (FILE (MERGE-PATHNAMES (MAKE-PATHNAME :NAME THEORY-NAME :TYPE
                                                            'LGC))
                                    :DIRECTION :OUTPUT :IF-EXISTS :NEW-VERSION :IF-DOES-NOT-EXIST 
                                    :CREATE)
                     (LET ((PREDS (ALL-PREDS THEORY))
                           (SAS (ALL-SAS THEORY)))
                          (PROGN (FORMAT FILE "~S~%%" THEORY-NAME)
                                 (FORMAT FILE "~D~%%" (LENGTH SAS))
                                 (DO ((SA-NAME SAS (CDR SA-NAME)))
                                     ((NULL SA-NAME)
                                      NIL)
                                     (FORMAT FILE "~S ~S ~%%" (CAR SA-NAME)
                                            (GETHASH (CAR SA-NAME)
                                                   THEORY)))
                                 (FORMAT FILE "~D~%%" (LENGTH PREDS))
                                 (DO ((PRED-NAME PREDS (CDR PRED-NAME)))
                                     ((NULL PRED-NAME)
                                      NIL)
                                     (FORMAT FILE "~S ~S ~%%" (CAR PRED-NAME)
                                            (GETHASH (CAR PRED-NAME)
                                                   THEORY)))
                                 'SAVED])


(DEFMACRO SEMANTIC-ATTACHMENT-P
 (SA) `(EQ (CAR ,SA)
                                          'SA))


(DEFUN SHOW-DEFINITION
 (ELEMENT THEORY-NAME &OPTIONAL WINDOW)
   [FORMAT (OR (AND WINDOW *TRACE-OUTPUT*)
               T)
          "~S~%%"
          (PROG [(DEF (GETHASH ELEMENT (GET-THEORY THEORY-NAME WINDOW]
                (OR (AND (SEMANTIC-ATTACHMENT-P DEF)
                         (RETURN (CDR DEF)))
                    (RETURN DEF])


(DEFUN SHOW-THEORY
 (THEORY-NAME &OPTIONAL VERBOSE WINDOW)
   [LET* ((THEORY (GET-THEORY THEORY-NAME))
          (PREDICATES (ALL-PREDS THEORY))
          (SAS (ALL-SAS THEORY))
          (STREAM (OR (AND WINDOW *TRACE-OUTPUT*)
                      T)))
         [OR (AND SAS (PROGN (FORMAT STREAM "Semantic attachments: ~%%")
                             [DO ((PP SAS (CDR PP)))
                                 ((NULL PP)
                                  NIL)
                                 (PROGN (FORMAT T "~%%~S ~%% " (CAR PP))
                                        (AND VERBOSE (FORMAT T "Definition: ~S ~%%"
                                                            (CDR (GETHASH (CAR PP)
                                                                        THEORY))
                                                            " "]
                             (FORMAT STREAM "~%% ~%%"]
         (OR (AND PREDICATES (PROGN (FORMAT STREAM "Predicates: ~%%")
                                    [DO ((PP PREDICATES (CDR PP)))
                                        ((NULL PP)
                                         NIL)
                                        (PROGN (FORMAT T "~%%~S ~%%" (CAR PP))
                                               (AND VERBOSE (FORMAT STREAM "Clauses: ~S ~%%"
                                                                   (GETHASH (CAR PP)
                                                                          THEORY)
                                                                   " "]
                                    (FORMAT STREAM "~%% ~%%"])


(DEFUN SOLVE
 (TREE FORMULA CLAUSES &OPTIONAL CUT WINDOW)
   [PROG NIL
     JUMP
         (AND WINDOW (SOLVE-DEBUGGER TREE FORMULA CLAUSES WINDOW))
         (COND
            ((NULL CLAUSES)                                  (IL:* IL:; "demo is failed")


             (RETURN (CLEAR-AND-LEVEL TREE)))
            ((DIRECTLY-IMPLEMENTED CLAUSES)                  (IL:* IL:; 

                                                             "clauses from the main theory")


             (RETURN (FUNCALL (CDR CLAUSES)
                            TREE FORMULA CLAUSES WINDOW)))
            [(SEMANTIC-ATTACHMENT-P CLAUSES)                 (IL:* IL:; 

                                                            "Semantic attachment defined by the user")


             (LET [(EXPANDED-FORMULA (LOOKUP FORMULA (UNIFICATION-ENV (AND-LEVEL TREE]
                  (COND
                     ((APPLY (CDR CLAUSES)
                             (CDR EXPANDED-FORMULA))
                      (RETURN TREE))
                     (T (RETURN (CLEAR-AND-LEVEL TREE]
            (T (LET* ((CANDIDATE (FIRST CLAUSES))
                      (ASSERT (RENAME CANDIDATE))
                      (NEWENV (UNIFY FORMULA (CONSEQ ASSERT)
                                     (UNIFICATION-ENV (AND-LEVEL TREE))
                                     WINDOW)))
                     (COND
                        ((FAILEDP NEWENV)
                         (SETF CLAUSES (REST CLAUSES))
                         (GO JUMP))
                        [(ATOMIC-FORMULAP ASSERT)
          
          (IL:* IL:;; "If a cut has been discovered in the previous procedure, it is necessary not to instantiate alternatives for the clause in a or-level")


                         (RETURN (UPDATE-ENV NEWENV (OR (AND CUT TREE)
                                                        (ADD-OR-LEVEL FORMULA (REST CLAUSES)
                                                               TREE]
                        ((IMPLICATIONP ASSERT)
          
          (IL:* IL:;; "If there is a cut, it is necessary to mark the alternatives for that clause; if the cut will be proved, then these alternatives will be eliminated  ")


                         (RETURN (COND
                                    [(IS-THERE-CUT (ANTEC ASSERT))
                                     (LET* ((RENAMED-STRUCTURE (RENAME-CUT (ANTEC ASSERT)))
                                            (RENAMED-CUT (CAR RENAMED-STRUCTURE))
                                            (RENAMED-ASSERT (CDR RENAMED-STRUCTURE)))
                                           (SUBSTITUTE-LEVEL NEWENV RENAMED-ASSERT
                                                  (ADD-OR-LEVEL FORMULA (REST CLAUSES)
                                                         TREE RENAMED-CUT]
                                    (T (SUBSTITUTE-LEVEL NEWENV (ANTEC ASSERT)
                                              (ADD-OR-LEVEL FORMULA (REST CLAUSES)
                                                     TREE])


(DEFUN SUBSTITUTE-LEVEL
 (ENV ANTECS TREE) (PROGN [RPLACA TREE (MAKE-AND-NODE
                                                               (APPEND ANTECS (CONJ (AND-LEVEL TREE))
                                                                      )
                                                               ENV
                                                               (GET-AND-NODE-THEORIES (AND-LEVEL
                                                                                       TREE]
                                                 TREE))


(DEFMACRO THEORYP
 (THEORY &OPTIONAL WINDOW) `(OR (AND (GET-THEORY ,THEORY ,WINDOW)
                                                      T)
                                                 (HASH-TABLE-P ,THEORY)))


(DEFMACRO UNIF-ENV-OR
 (OR-NODE) `(FOURTH ,OR-NODE))


(DEFMACRO UNIFICATION-ENV
 (AND-NODE) `(SECOND ,AND-NODE))


(DEFUN UPDATE-ENV
 (ENV TREE) (SETF (SECOND (AND-LEVEL TREE))
                                   ENV)
                             TREE)


(DEFUN UPDATE-LEVEL
 (LEVEL FORMULA) (MAKE-AND-NODE (CDR (CONJ LEVEL))
                                           (UNIFICATION-ENV LEVEL)
                                           (GET-AND-NODE-THEORIES LEVEL)))


(DEFUN UPDATE-TREE
 (LEVEL TREE) (MAKE-TREE LEVEL (OR-LEVELS TREE)))


(IL:RPAQQ *PRINT-PRETTY*
 T)
(IL:FILESLOAD UNIFIER)
(IL:PUTPROPS IL:LOGIC IL:COPYRIGHT ("Roberto Ghislanzoni" 1988))
(IL:DECLARE%: IL:DONTCOPY
  (IL:FILEMAP (NIL)))
IL:STOP