home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2067 < prev    next >
Encoding:
Internet Message Format  |  1992-11-17  |  2.7 KB
  1. Path: sparky!uunet!charon.amdahl.com!pacbell.com!sgiblab!darwin.sura.net!jvnc.net!netnews.upenn.edu!news.cc.swarthmore.edu!plummer
  2. From: plummer@cs.swarthmore.edu (David Barker-Plummer)
  3. Newsgroups: sci.logic
  4. Subject: Re: Programs for simple logic proofs:  where are they?
  5. Message-ID: <PLUMMER.92Nov16180704@nutmeg.cs.swarthmore.edu>
  6. Date: 16 Nov 92 23:07:04 GMT
  7. References: <4804@equinox.unr.edu> <1992Nov16.183210.9769@beaver.cs.washington.edu>
  8. Sender: news@cc.swarthmore.edu (USENET News System)
  9. Organization: Swarthmore College, Swarthmore, PA
  10. Lines: 43
  11. In-Reply-To: jon@cs.washington.edu's message of Mon, 16 Nov 92 18:32:10 GMT
  12. Nntp-Posting-Host: nutmeg.cs.swarthmore.edu
  13.  
  14. In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:
  15.  
  16. JJ> In article <4804@equinox.unr.edu> mjb@dws020.unr.edu (Mike Brown) writes:
  17. >I am looking for programs that will do proofs like:
  18. >            Prove: Q            \
  19. >    1 P then Q    Premis               > The problem
  20. >    2 P        Premis              /
  21. >    3 Q             1, 2, Modus Ponens  >  The program's proof
  22. >
  23. >(The proofs do get more involved)
  24. >
  25. >Is there a program out there that will do these proofs?
  26.  
  27. JJ> I saw two responses to this post, recommending Otter and HOL.  I think they
  28. JJ> made it clear that they were probably not what Mike Brown was looking for.
  29. JJ> The Otter and HOL versions of this very simple proof don't look a whole lot
  30. JJ> like Mike's very clear presentation.  I've read the book about Otter and 
  31. JJ> learned/used a little of HOL; they are both powerful research systems, with
  32. JJ> all that entails.
  33.  
  34. JJ> I think what the original post was asking for was a simple natural
  35. JJ> deduction prover for propositional logic, where the problem
  36. JJ> statements and proofs look much as they do in a logic textbook.
  37. JJ> Do such things exist?  The nearest thing I have read about is
  38. JJ> "Muffin: A Proof Assistant", a chapter by Richard C. Moore in
  39. JJ> Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT,
  40. JJ> Prentice Hall International, 1990. I recall the chapter saying
  41. JJ> something about Muffin being made available.  I wonder if anyone
  42. JJ> is using it.
  43.  
  44. Andrews' system, ack I can't remember its name right now, allws you to
  45. construct proofs in exactly the standard natural deduction
  46. presentation of the original poster's example.  Contact Peter Andrews
  47. at CMU.  Of course, the underlying logic of this prover is typed
  48. higher order logic, and is significantly more powerful (and hence
  49. harder to understand) than the simple example would suggest.
  50.  
  51. Another system that comes to mind is MacLogic developed by Roy Dychoff
  52. at St. Andrews University (rd@cs.st-and.ac.uk).  I am not sure of the
  53. availability, but this is the sort of system I would choose for
  54. teaching natural deduction to neophytes.
  55.  
  56. -- Dave
  57.