home *** CD-ROM | disk | FTP | other *** search
/ back2roots/padua / padua.7z / padua / lang / gofer223.lha / demos / prolog / PureEngine < prev    next >
Encoding:
Text File  |  1991-11-19  |  1.4 KB  |  40 lines
  1. --
  2. -- The Pure Prolog inference engine (using explicit prooftrees)
  3. -- Mark P. Jones November 1990, modified for Gofer 20th July 1991
  4. --
  5. -- uses Gofer version 2.20
  6. --
  7.  
  8. version = "tree based" 
  9.  
  10. --- Calculation of solutions:
  11.  
  12. -- Each node in a prooftree corresponds to:
  13. -- either: a solution to the current goal, represented by Done s, where s
  14. --         is the required substitution
  15. -- or:     a choice between a number of subtrees ts, each corresponding to a
  16. --         proof of a subgoal of the current goal, represented by Choice ts.
  17. --         The proof tree corresponding to an unsolvable goal is Choice [] 
  18.  
  19. data Prooftree = Done Subst  |  Choice [Prooftree]
  20.  
  21. -- prooftree uses the rules of Prolog to construct a suitable proof tree for
  22. --           a specified goal
  23. prooftree   :: Database -> Int -> Subst -> [Term] -> Prooftree
  24. prooftree db = pt
  25.  where pt           :: Int -> Subst -> [Term] -> Prooftree
  26.        pt n s []     = Done s
  27.        pt n s (g:gs) = Choice [ pt (n+1) (u@@s) (map (apply u) (tp++gs))
  28.                               | (tm:-tp)<-renClauses db n g, u<-unify g tm ]
  29.  
  30. -- search performs a depth-first search of a proof tree, producing the list
  31. --        of solution substitutions as they are encountered.
  32. search              :: Prooftree -> [Subst]
  33. search (Done s)      = [s]
  34. search (Choice pts)  = [ s | pt <- pts, s <- search pt ]
  35.  
  36. prove    :: Database -> [Term] -> [Subst]
  37. prove db  = search . prooftree db 1 nullSubst
  38.  
  39. --- End of PureEngine.hs
  40.