;;; -*- Package: User; Syntax: Common-Lisp; Mode: Lisp; Base: 10 -*-
;;; File converted on 28-Oct-87 14:27:32 from source LOGIC
;;; Original source {DSK}<LISPFILES>LOGIC>LOGIC.;3 created 26-Apr-88 09:10:49
; Copyright (c) 1988 by Roberto Ghislanzoni. All rights reserved.
(DEFUN ADD-OR-LEVEL (WFF CLAUSES TREE &OPTIONAL CUTNAME)
;; 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)
;; 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) (IL:BQUOTE (CAR (IL:\\\, TREE))))
(DEFMACRO ANTEC (WFF) (IL:BQUOTE (CDDR (IL:\\\, 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)
(IL:BQUOTE (AND (LISTP (IL:\\\, WFF))
(NULL (SECOND (IL:\\\, 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) (IL:BQUOTE (SECOND (IL:\\\, OR-NODE))))
(DEFUN CLEAR-AND-LEVEL (TREE) (PROGN (SETF (CAR TREE)
NIL)
TREE))
(DEFMACRO CONJ (AND-LEVEL) (IL:BQUOTE (CAR (IL:\\\, AND-LEVEL))))
(DEFUN CONSEQ (WFF) (CAR WFF))
(DEFMACRO CONSEQP (C) (IL:BQUOTE (AND (LISTP (IL:\\\, C))
(SYMBOLP (CAR (IL:\\\, 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)
;; 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)
(IL:BQUOTE (EQ (CAR (IL:\\\, CLAUSES))
'DIRECTLY-IMPLEMENTED)))
(DEFMACRO FAILEDP (ENV) (IL:BQUOTE (EQ (IL:\\\, 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) (IL:BQUOTE (CAR (IL:\\\, OR-LEVEL))))
(DEFMACRO GET-AND-NODE-THEORIES (AND-NODE) (IL:BQUOTE
(THIRD (IL:\\\, AND-NODE))))
(DEFMACRO GET-CUT (OR-NODE) (IL:BQUOTE (SIXTH (IL:\\\, OR-NODE))))
(DEFMACRO GET-OR-NODE-THEORIES (OR-NODE) (IL:BQUOTE (FIFTH (IL:\\\,
OR-NODE))))
(DEFMACRO GET-THEORY (THEORY-NAME &OPTIONAL WINDOW)
(IL:BQUOTE (OR (AND (IL:\\\, WINDOW)
(GET-THEORY-INTERNAL (IL:\\\, THEORY-NAME)
(IL:\\\, WINDOW)))
(GET 'THEORY (IL:\\\, THEORY-NAME)))))
(DEFMACRO IMPLICATIONP (WFF)
(IL:BQUOTE (LET ((SEPARATOR (SECOND (IL:\\\, WFF))))
(AND (EQ SEPARATOR ':-)
(NOT (NULL (CDDR (IL:\\\, 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))))
;; 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
;; 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) (IL:BQUOTE (NULL (CAR (IL:\\\, TREE)))
))
(DEFMACRO NULL-OR-LEVELP (TREE) (IL:BQUOTE (NULL (SECOND (IL:\\\,
TREE)))))
(DEFMACRO NULL-TREEP (TREE) (IL:BQUOTE (AND (NULL-AND-LEVELP
(IL:\\\, TREE))
(NULL-OR-LEVELP
(IL:\\\, TREE)))))
(DEFMACRO OR-LEVELS (TREE) (IL:BQUOTE (SECOND (IL:\\\, 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)
;; 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) (IL:BQUOTE
(EQ (CAR (IL:\\\, 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) ; demo is failed
(RETURN (CLEAR-AND-LEVEL TREE)))
((DIRECTLY-IMPLEMENTED CLAUSES); clauses from the main
; theory
(RETURN (FUNCALL (CDR CLAUSES)
TREE FORMULA CLAUSES WINDOW)))
((SEMANTIC-ATTACHMENT-P CLAUSES)
; 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)
;; 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)
;; 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)
(IL:BQUOTE (OR (AND (GET-THEORY (IL:\\\, THEORY)
(IL:\\\, WINDOW))
T)
(HASH-TABLE-P (IL:\\\, THEORY)))))
(DEFMACRO UNIF-ENV-OR (OR-NODE) (IL:BQUOTE (FOURTH (IL:\\\, OR-NODE))))
(DEFMACRO UNIFICATION-ENV (AND-NODE) (IL:BQUOTE (SECOND (IL:\\\,
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:FILESLOAD UNIFIER)