home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2272 < prev    next >
Encoding:
Text File  |  1992-12-21  |  1.8 KB  |  43 lines
  1. Newsgroups: comp.lang.prolog
  2. Path: sparky!uunet!paladin.american.edu!news.univie.ac.at!hp4at!mcsun!sunic!sics.se!torkel
  3. From: torkel@sics.se (Torkel Franzen)
  4. Subject: Re: Occurs check
  5. In-Reply-To: pereira@alice.att.com's message of 20 Dec 92 02:05:36 GMT
  6. Message-ID: <TORKEL.92Dec20104928@bast.sics.se>
  7. Sender: news@sics.se
  8. Organization: Swedish Institute of Computer Science, Kista
  9. References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk>
  10.     <24435@alice.att.com> <TORKEL.92Dec17201903@bast.sics.se>
  11.     <24439@alice.att.com> <TORKEL.92Dec18231028@lludd.sics.se>
  12.     <24454@alice.att.com>
  13. Date: Sun, 20 Dec 1992 09:49:28 GMT
  14. Lines: 27
  15.  
  16. In article <24454@alice.att.com> pereira@alice.att.com (Fernando Pereira)
  17.  writes:
  18.  
  19.    >I agree. Adding the first-order theory of rational trees to the left of the
  20.    >|- is precisely restricting the class of models under consideration
  21.    >from arbitrary first-order models to rational tree models.
  22.  
  23.    This is not so, since the class of rational tree models cannot be
  24. characterized by any set of first order axioms, any more than the finite
  25. tree models.
  26.  
  27.    >In any case, one needs to be *very* clear about what one
  28.    >is assuming to the left of the |-. 
  29.  
  30.   In a more perspicuous description of Prolog-style Horn clause programming,
  31. I think it's a good idea to separate the constraint system from the
  32. resolution mechanism. Thus Prolog (in the simplified version here considered),
  33. whatever the constraint system used, delivers answers to a question A(x)
  34. of the form C(x,y), where C(x,y) is a conjunction of constraints, and
  35. it always holds that
  36.  
  37.     (1)                     C(x,y) -> A(x)
  38.  
  39. is a logical consequence of the program, read as a set of Horn clauses. Of
  40. course (1) does not imply that there is an x such that A(x); for this to
  41. follow, the constraint theory must be used.
  42.  
  43.