home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2061 < prev    next >
Encoding:
Text File  |  1992-11-16  |  2.0 KB  |  44 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!gumby!destroyer!cs.ubc.ca!uw-beaver!jon
  3. From: jon@cs.washington.edu (Jon Jacky)
  4. Subject: Re: Programs for simple logic proofs:  where are they?
  5. Message-ID: <1992Nov16.183210.9769@beaver.cs.washington.edu>
  6. Summary: Otter and HOL are very nice, but probably not what the poster wanted
  7. Keywords: Natural deduction, automatic theorem proving, Otter, HOL, Muffin
  8. Sender: news@beaver.cs.washington.edu (USENET News System)
  9. Organization: Computer Science & Engineering, U. of Washington, Seattle
  10. References: <4804@equinox.unr.edu>
  11. Date: Mon, 16 Nov 92 18:32:10 GMT
  12. Lines: 30
  13.  
  14. In article <4804@equinox.unr.edu> mjb@dws020.unr.edu (Mike Brown) writes:
  15. >I am looking for programs that will do proofs like:
  16. >            Prove: Q            \
  17. >    1 P then Q    Premis               > The problem
  18. >    2 P        Premis              /
  19. >    3 Q             1, 2, Modus Ponens  >  The program's proof
  20. >
  21. >(The proofs do get more involved)
  22. >
  23. >Is there a program out there that will do these proofs?
  24.  
  25. I saw two responses to this post, recommending Otter and HOL.  I think they
  26. made it clear that they were probably not what Mike Brown was looking for.
  27. The Otter and HOL versions of this very simple proof don't look a whole lot
  28. like Mike's very clear presentation.  I've read the book about Otter and 
  29. learned/used a little of HOL; they are both powerful research systems, with
  30. all that entails.
  31.  
  32. I think what the original post was asking for was a simple natural deduction
  33. prover for propositional logic, where the problem statements and proofs look
  34. much as they do in a logic textbook.   Do such things exist?  The nearest thing
  35. I have read about is "Muffin: A Proof Assistant", a chapter by Richard C. Moore
  36. in Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT, Prentice
  37. Hall International, 1990. I recall the chapter saying something about Muffin
  38. being made available.   I wonder if anyone is using it.
  39.  
  40. - Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA
  41.  
  42.  
  43.  
  44.