home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2275 < prev    next >
Encoding:
Internet Message Format  |  1992-12-21  |  1.6 KB
  1. Path: sparky!uunet!zaphod.mps.ohio-state.edu!saimiri.primate.wisc.edu!ames!haven.umd.edu!darwin.sura.net!spool.mu.edu!enterpoop.mit.edu!eru.mt.luth.se!lunic!sunic!sics.se!torkel
  2. From: torkel@sics.se (Torkel Franzen)
  3. Newsgroups: comp.lang.prolog
  4. Subject: Re: Occurs check
  5. Message-ID: <TORKEL.92Dec21064735@bast.sics.se>
  6. Date: 21 Dec 92 05:47:35 GMT
  7. References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk>
  8.     <24435@alice.att.com> <TORKEL.92Dec17201903@bast.sics.se>
  9.     <24439@alice.att.com> <TORKEL.92Dec18231028@lludd.sics.se>
  10.     <24454@alice.att.com> <TORKEL.92Dec20104928@bast.sics.se>
  11.     <
  12. Sender: news@sics.se
  13. Organization: Swedish Institute of Computer Science, Kista
  14. Lines: 16
  15. In-Reply-To: pereira@alice.att.com's message of 20 Dec 92 22:53:14 GMT
  16.  
  17. In article <24458@alice.att.com> pereira@alice.att.com (Fernando Pereira)
  18.  writes:
  19.  
  20.    >It cannot be characterized by any *finite* set of first-order formulas.
  21.  
  22.   Finiteness is not relevant here. It is a matter of what can be
  23. expressed in first order logic. By compactness, any set of first order
  24. formulas which has a model with the Herbrand universe
  25. {0,s(0),s(s(0)),..} as its domain will have countable models
  26. containing elements different from (the interpretations of) the terms
  27. 0,s(0), ec. Therefore it is not correct to say that adding the
  28. (complete) first order identity theory of finite trees to the left of
  29. |- is precisely restricting the class of models under consideration
  30. from arbitrary first order models to finite tree models.  Similarly
  31. for rational trees. Such a restriction cannot be achieved in first
  32. order logic.
  33.