home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / sci / math / symbolic / 3552 < prev    next >
Encoding:
Internet Message Format  |  1993-01-28  |  2.1 KB
  1. Path: sparky!uunet!ogicse!news.u.washington.edu!raven.alaska.edu!news.acns.nwu.edu!uicvm.uic.edu!u54294
  2. From: U54294@uicvm.uic.edu
  3. Newsgroups: sci.math.symbolic
  4. Subject: Re: Automatic Theorem Proving?
  5. Message-ID: <93027.185552U54294@uicvm.uic.edu>
  6. Date: 28 Jan 93 00:55:52 GMT
  7. Article-I.D.: uicvm.93027.185552U54294
  8. References: <1k3q28INN82l@signal.dra.hmg.gb>
  9. Organization: University of Illinois at Chicago
  10. Lines: 30
  11.  
  12. In article <1k3q28INN82l@signal.dra.hmg.gb>, heading@ccint1.rsre.mod.uk (Anthony
  13. J.R. Heading) says:
  14. >
  15. >I want to write a computer algebra/theorem proving system, basically
  16. >as a learning exercise and a testbed for any new ideas I might have.
  17. >I guess, though, that this has been done a million times in the past,
  18. >so I want to find out about important existing systems.
  19. >
  20. >Thanks
  21. >Anthony Heading
  22. >
  23. The title "Automated Reasoning" by Ewing, Overbeek, Lusk, Boyle (did I
  24. forget anyone?) just came out in an expanded second edition. It includes
  25. a diskette containing the Otter 2.2 theorem proving system. The text is
  26. something of a tutorial, but you can easily skip to the more "formal"
  27. chapters if you prefer. There is also a reference chapter on Otter and
  28. a chapter on Prolog as a theorem proving system.
  29. The disk contains source, documentation and executables for DOS. Other
  30. versions are available for Unix. I believe that the publisher is
  31. Prentice-Hall. All the authors are at Argonne National Labs here in the
  32. beautiful Chicago area. You can contact otter@mcs.anl.gov for further
  33. information on Otter. If you can't locate the book, get ahold of me and
  34. I'll provide a fuller citation. The tome's at home.
  35. +----------------------------------+------------------------------------+
  36. |                                  | I have noted in a Manchester       |
  37. |   Nick Geovanis                  | newspaper that I have proved might |
  38. |   U54294@uicvm.uic.edu  <--BEST  | is right and therefore that every  |
  39. |   GEONI02@hera.cai.com           | cheating tradesman is also right.  |
  40. |                                  |      -- Darwin to Lyell, 1860      |
  41. +-----------------------------------------------------------------------+
  42.