home *** CD-ROM | disk | FTP | other *** search
/ Simtel MSDOS 1992 June / SIMTEL_0692.cdr / msdos / ddjmag / ddj8604.arc / BROWN.LSP < prev    next >
Encoding:
Text File  |  1986-04-30  |  7.1 KB  |  255 lines
  1. ; File: BRIE.LIB
  2.  
  3. (PUTD 'DEFUN '(NLAMBDA (NAM$ EXP$) (PUTD NAM$ EXP$) NAM$))
  4.  
  5.  
  6.  
  7. (DEFUN * (NLAMBDA X
  8.   NIL ))
  9.  
  10. (DEFUN CONCAT (LAMBDA (P Q)
  11.   (* concatonate 2 lists together *)
  12.   ((NULL P) Q)
  13.   (CONS (CAR P) (CONCAT (CDR P) Q)) ))
  14.  
  15. (DEFUN PURGE (LAMBDA (L)
  16.   (* purge a list of duplicate members *)
  17.   ((NULL L) NIL)
  18.   ((MEMBER (CAR L) (CDR L))
  19.     (PURGE (CDR L)) )
  20.   (CONS (CAR L) (PURGE (CDR L))) ))
  21.  
  22. (DEFUN JOIN (LAMBDA (L M)
  23.   (* form the set union of 2 lists *)
  24.   (PURGE (CONCAT L M)) ))
  25.  
  26. (DEFUN MEET (LAMBDA (L M)
  27.   (* form the set intersection of 2 lists *)
  28.   (PURGE (COMMON L M)) ))
  29.  
  30. (DEFUN COMMON (LAMBDA (L M)
  31.   (* form the set intersection of 2 lists with possible
  32.       duplicate entries *)
  33.   ((NULL L) NIL)
  34.   ((MEMBER (CAR L) M)
  35.     (CONS (CAR L) (COMMON (CDR L) M)) )
  36.   (COMMON (CDR L) M) ))
  37.  
  38. (DEFUN DEF (LAMBDA (V E)
  39.   (* determine whether the variable V is defined in the
  40.       environment E *)
  41.   ((NULL E) NIL)
  42.   ((EQUAL V (CAAR E)) T)
  43.   (DEF V (CDR E)) ))
  44.  
  45. (DEFUN IMM (LAMBDA (V E)
  46.   (* return the immeadiate successor of the variable V in the
  47.       environment E *)
  48.   ((NULL E) NIL)
  49.   ((EQUAL V (CAAR E))
  50.     (CDAR E) )
  51.   (IMM V (CDR E)) ))
  52.  
  53. (DEFUN ULT (LAMBDA (V E)
  54.   (* return the ultimate successor of the variable V in the
  55.       environment E *)
  56.   ((DEF V E)
  57.     (ULT (IMM V E) E) )
  58.   V ))
  59.  
  60. (DEFUN PAIRP (LAMBDA (P)
  61.   (* determine if P is a pair (not an atom) *)
  62.   ((ATOM P) NIL)
  63.   T ))
  64.  
  65. (DEFUN VARIABLEP (LAMBDA (V)
  66.   (* determine if V is a variable *)
  67.   (EQ (CAR (UNPACK V)) '*) ))
  68.  
  69. (DEFUN RECREAL (LAMBDA (F E)
  70.   (* return the recursive realization of a formula F in the
  71.       environment E which amounts to instantiating all variables
  72.       from the environment *)
  73.   ((PAIRP F)
  74.     (CONS (RECREAL (CAR F) E) (RECREAL (CDR F) E)) )
  75.   ((DEF F E)
  76.     (RECREAL (ULT F E) E) )
  77.   F ))
  78.  
  79. (DEFUN OCCURS (LAMBDA (V X E)
  80.   (* see if the variable V occurs in the term X under the
  81.       environment E *)
  82.   ((VARIABLEP X)
  83.     ((DEF X E)
  84.       (OCCURS V (IMM X E) E) )
  85.     ((EQ V X) T) )
  86.   ((ATOM X) NIL)
  87.   ((OCCURS V (CAR X) E) T)
  88.   (OCCURS V (CDR X) E) ))
  89.  
  90. (DEFUN UNIFY (LAMBDA (A B E)
  91.   (* unify 2 expressions (A and B) in the environment E by
  92.       extending E to the most general unifier of A and B and
  93.       returning that environment *)
  94.   ((EQ E 'IMPOSSIBLE)
  95.     'IMPOSSIBLE )
  96.   (EQUATE (ULT A E) (ULT B E) E) ))
  97.  
  98. (DEFUN EQUATE (LAMBDA (A B E)
  99.   (* auxilliary routine to UNIFY so that the flow of control
  100.       ping-pongs recursivly between UNIFY and EQUATE to
  101.       construct the most general unifier of A and B *)
  102.   ((EQUAL A B) E)
  103.   ((VARIABLEP A)
  104.     ((OCCURS A B E)
  105.       'IMPOSSIBLE )
  106.     (CONS (CONS A B) E) )
  107.   ((VARIABLEP B)
  108.     ((OCCURS B A E)
  109.       'IMPOSSIBLE )
  110.     (CONS (CONS B A) E) )
  111.   ((ATOM A)
  112.     'IMPOSSIBLE )
  113.   ((ATOM B)
  114.     'IMPOSSIBLE )
  115.   (UNIFY (CDR A) (CDR B) (UNIFY (CAR A) (CAR B) E)) ))
  116.  
  117. (DEFUN VARS (LAMBDA (X)
  118.   (* return a list of all the variables found in the expression
  119.       X *)
  120.   ((NULL X) NIL)
  121.   ((VARIABLEP X) X)
  122.   ((ATOM X) NIL)
  123.   (CONCAT (VARS (CAR X)) (VARS (CDR X))) ))
  124.  
  125. (DEFUN VARIANT (LAMBDA (Q E D)
  126.   (* returns a variant of D such that all variables are distinct
  127.       from those of Q in the environment E *)
  128.   (RECREAL D (MAKENV (VARS Q) (VARS E) (VARS D))) ))
  129.  
  130. (DEFUN MAKENV (LAMBDA (Q E D)
  131.   (* make an environment such that the instantiation of D in
  132.       this environment will have no variables in common with the
  133.       instantiation of Q in E *)
  134.   (MAKENV1 (MEET D (JOIN Q E)) (JOIN (JOIN Q E) D)) ))
  135.  
  136. (DEFUN MAKENV1 (LAMBDA (P Q V)
  137.   (* does the dirty work for MAKENV and VARIANT by generating an
  138.       environment that sticks asterisks onto the front of all
  139.       variable names in Q that also occur in P (V is a local
  140.       temporary variable) *)
  141.   ((NULL P) NIL)
  142.   ((ATOM P)
  143.     (SETQ V P)
  144.     (LOOP
  145.       ((NOT (MEMBER V Q)))
  146.       (SETQ V (PACK (CONS '* (UNPACK V)))) )
  147.     (CONS P V) )
  148.   (CONS (MAKENV1 (CAR P) Q) (MAKENV1 (CDR P) Q)) ))
  149.  
  150. (DEFUN GETLIT (LAMBDA (CL N)
  151.   (* get the Nth litteral in the clause CL and return it both as
  152.       the functions value and in the free variable LITG along
  153.       with its sign in the free variable SIGNG *)
  154.   (SETQ LITG (CAR (NTH CL N)))
  155.   (SETQ SIGNG (NOT (EQ (CAR LITG) '~)))
  156.   ((NOT (NULL SIGNG)) LITG)
  157.   (CADR LITG) ))
  158.  
  159. (DEFUN FRONT (LAMBDA (C N)
  160.   (* return all elements in the clause C in front of element N
  161.       *)
  162.   ((NULL C) NIL)
  163.   ((ZEROP N) NIL)
  164.   ((EQ N 1) NIL)
  165.   (CONS (CAR C) (FRONT (CDR C) (SUB1 N))) ))
  166.  
  167. (DEFUN BACK (LAMBDA (C N)
  168.   (* return all elements in clause C in back of element N *)
  169.   (NTH C (ADD1 N)) ))
  170.  
  171. (DEFUN FACTOR (LAMBDA (C P1 N1 S1 P2 N2 S2 ENV)
  172.   (* returns a factored version of the clause C *)
  173.   (SETQ ENV 'IMPOSSIBLE)
  174.   (SETQ N1 0)
  175.   (LOOP
  176.     (SETQ N1 (ADD1 N1))
  177.     ((GREATERP N1 (LENGTH C))
  178.       'IMPOSSIBLE )
  179.     (GETLIT C N1)
  180.     (SETQ P1 LITG)
  181.     (SETQ S1 SIGNG)
  182.     (SETQ N2 N1)
  183.     ( ((LOOP
  184.           (SETQ N2 (ADD1 N2))
  185.           ((GREATERP N2 (LENGTH C)))
  186.           (GETLIT C N2)
  187.           (SETQ P2 LITG)
  188.           (SETQ S2 SIGNG)
  189.           ( ((EQ S1 S2)
  190.               (SETQ ENV (UNIFY P1 P2)) ) )
  191.           ((NOT (EQ ENV 'IMPOSSIBLE))
  192.             (SETQ C (RECREAL C ENV))
  193.             (SETQ C (APPEND (FRONT C N1) (BACK C N1))) ) )) )
  194.     ((NOT (EQ ENV 'IMPOSSIBLE))) )
  195.   ((NOT (EQ ENV 'IMPOSSIBLE)) C)
  196.   'IMPOSSIBLE ))
  197.  
  198. (DEFUN BINRES (LAMBDA (CL1 N1 CL2 N2 ENV LIT1 SGN1 LIT2 SGN2 L1
  199.     L2 LITG SIGNG)
  200.   (* compute the binary resolvent of clause CL1 litteral number
  201.       N1 with clause CL2 litteral number N2 and return the
  202.       instantiated resolvent *)
  203.   (SETQ CL2 (VARIANT CL1 ENV CL2))
  204.   (SETQ LIT1 (GETLIT CL1 N1))
  205.   (SETQ L1 LITG)
  206.   (SETQ SGN1 SIGNG)
  207.   (SETQ LIT2 (GETLIT CL2 N2))
  208.   (SETQ L2 LITG)
  209.   (SETQ SGN2 SIGNG)
  210.   ((EQ SGN1 SGN2) NIL)
  211.   (SETQ ENV (UNIFY LIT1 LIT2 ENV))
  212.   ((EQ ENV 'IMPOSSIBLE)
  213.     'IMPOSSIBLE )
  214.   (RECREAL (APPEND (FRONT CL1 N1) (BACK CL1 N1) (FRONT CL2 N2)
  215.       (BACK CL2 N2)) ENV) ))
  216.  
  217. (DEFUN PARAMOD (LAMBDA (FROM INTO PF F PI I SEL SUB ENV SWAP PM)
  218.   (* return the paramodulant of the FROM clause into the INTO
  219.       clause *)
  220.   (SETQ INTO (VARIANT FROM NIL INTO))
  221.   (SETQ PM 'IMPOSSIBLE)
  222.   (SETQ PF 0)
  223.   (LOOP
  224.     (SETQ PF (ADD1 PF))
  225.     (SETQ F (CAR (NTH FROM PF)))
  226.     ((NULL F))
  227.     ((EQ (CAR F) '=)
  228.       (SETQ SEL (CADR F))
  229.       (SETQ SUB (CADDR F))
  230.       (SETQ PI 0)
  231.       (LOOP
  232.         (SETQ PI (ADD1 PI))
  233.         (SETQ I (CAR (NTH INTO PI)))
  234.         ((NULL I))
  235.         (SETQ ENV (UNIFY SEL I))
  236.         ( ((EQ ENV 'IMPOSSIBLE)
  237.             (SETQ ENV (UNIFY SUB I))
  238.             (SETQ SUB SEL) ) )
  239.         ((NOT (EQ ENV 'IMPOSSIBLE))
  240.           (SETQ FROM (RECREAL FROM ENV))
  241.           (SETQ INTO (RECREAL INTO ENV))
  242.           ( ((NOT (NULL SWAP))
  243.               (SETQ SUB SEL) ) )
  244.           (SETQ INTO (APPEND (FRONT INTO PI) (LIST SUB) (BACK
  245.               INTO PI)))
  246.           (SETQ FROM (APPEND (FRONT FROM PF) (BACK FROM PF)))
  247.           (SETQ PM (APPEND FROM INTO)) ) ) )
  248.     ((NOT (EQ PM 'IMPOSSIBLE))) )
  249.   PM ))
  250.  
  251. (RDS)
  252.  FROM PF) (BACK FROM PF)))
  253.           (SETQ PM (APPEND FROM INTO)) ) ) )
  254.     ((NOT (EQ PM 'IMPOSSIBLE))) )
  255.   PM