home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2084 < prev    next >
Encoding:
Internet Message Format  |  1992-11-17  |  2.0 KB
  1. Path: sparky!uunet!charon.amdahl.com!pacbell.com!ames!agate!doc.ic.ac.uk!uknet!mucs!timc
  2. From: timc@cs.man.ac.uk (Tim Clement)
  3. Newsgroups: sci.logic
  4. Subject: Re: Programs for simple logic proofs:  where are they?
  5. Keywords: Natural deduction, automatic theorem proving, Otter, HOL, Muffin
  6. Message-ID: <6776@m1.cs.man.ac.uk>
  7. Date: 17 Nov 92 14:18:26 GMT
  8. References: <4804@equinox.unr.edu> <1992Nov16.183210.9769@beaver.cs.washington.edu>
  9. Sender: news@cs.man.ac.uk
  10. Organization: Dept Computer Science, University of Manchester, U.K.
  11. Lines: 33
  12.  
  13. In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:
  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. >The nearest thing
  26. >I have read about is "Muffin: A Proof Assistant", a chapter by Richard C. Moore
  27. >in Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT, Prentice
  28. >Hall International, 1990. I recall the chapter saying something about Muffin
  29. >being made available.   I wonder if anyone is using it.
  30. >
  31.  
  32. Muffin developed into "mural", a WIMP interface proof assistant for
  33. natural deduction proofs (i.e. proofs much like the example above).
  34. As a proof assistant, it leaves the user to decide that Modus Ponens
  35. is the rule to apply (although there are various forms of assistance
  36. for the choice).  Full details are in "mural: a formal development
  37. support system" by C.B.Jones et al, Springer 1991.  ISBN 3-540-19651-X.
  38.  
  39. mural is generally available at modest cost.  It is a large SmallTalk
  40. image, so can only be supplied to people with an appropriate SmallTalk
  41. license (hence no FTP).  For details, contact richard@cs.man.ac.uk
  42. (non-educational users) or br@inf.rl.ac.uk (universities and similar
  43. bodies).
  44.  
  45. Tim Clement
  46.