home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2071 < prev    next >
Encoding:
Text File  |  1992-11-17  |  1.9 KB  |  45 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!haven.umd.edu!darwin.sura.net!zaphod.mps.ohio-state.edu!sol.ctr.columbia.edu!usenet.ucs.indiana.edu!silver.ucs.indiana.edu!jhhardy
  3. From: jhhardy@silver.ucs.indiana.edu (J. Hardy)
  4. Subject: Re: Programs for simple logic proofs: where are they?
  5. Message-ID: <Bxv4xy.A7y@usenet.ucs.indiana.edu>
  6. Sender: news@usenet.ucs.indiana.edu (USENET News System)
  7. Nntp-Posting-Host: silver.ucs.indiana.edu
  8. Organization: Indiana University
  9. References: <4804@equinox.unr.edu> <1992Nov16.183210.9769@beaver.cs.washington.edu>     <PLUMMER.92Nov16180704@nutmeg.cs.swarthmore.edu> <IMG.92Nov17114848@hope.aisb.ed.ac.uk>
  10. Date: Tue, 17 Nov 1992 13:46:46 GMT
  11. Lines: 32
  12.  
  13. In <IMG.92Nov17114848@hope.aisb.ed.ac.uk> img@aisb.ed.ac.uk (Ian Green) writes:
  14.  
  15.  
  16. >If you're looking for an interactive system, you might try FOL or
  17. >its derivative, GETFOL.  Contact Fausto Giunchiglia, at fausto@irst.it or
  18. >fausto@dist.unige.it for more info.  Weyhrauch80 describes FOL.
  19.  
  20. >    -ian
  21.  
  22. >@article(Weyhrauch80,
  23. >        Author = {Weyhrauch, Richard W.},
  24. >         Title = {Prolegomena to a Theory of Mechanized Formal Reasoning},
  25. >          Year = {1980},
  26. >       Journal = AI,
  27. >        Volume = {13},
  28. >         Pages = {133--170})
  29.  
  30. As I recall there are several programs that do FOL proofs in a natural
  31. deduction system for the Mac and for IBM-clones.  The ones I'm
  32. thinking of aren't theorem provers, but are more like proof checkers.
  33. I know that Tarski's World (by Barwise and Etchemendy) is available both
  34. for the macintosh and for windows.  If that's the sort of thing you're looking
  35. for then there are several others also (tho I can't at the moment recall the
  36. titles).  Someone was demo'ing an IBMish program at the last APA conference
  37. I attended.
  38.  
  39. If that's the sort of thing you're looking for then you might ask on
  40. philos-l.  I seem to recall that a list of such programs circulated there not
  41. too long ago.
  42.  
  43. jim hardy
  44.  
  45.