home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2069 < prev    next >
Encoding:
Internet Message Format  |  1992-11-17  |  3.3 KB
  1. Path: sparky!uunet!zaphod.mps.ohio-state.edu!magnus.acs.ohio-state.edu!usenet.ins.cwru.edu!agate!doc.ic.ac.uk!uknet!edcastle!aisb!aisb!img
  2. From: img@aisb.ed.ac.uk (Ian Green)
  3. Newsgroups: sci.logic
  4. Subject: Re: Programs for simple logic proofs:  where are they?
  5. Message-ID: <IMG.92Nov17114848@hope.aisb.ed.ac.uk>
  6. Date: 17 Nov 92 11:48:48 GMT
  7. References: <4804@equinox.unr.edu> <1992Nov16.183210.9769@beaver.cs.washington.edu>
  8.     <PLUMMER.92Nov16180704@nutmeg.cs.swarthmore.edu>
  9. Sender: news@aisb.ed.ac.uk (Network News Administrator)
  10. Organization: Department of Artificial Intelligence, University of Edinburgh
  11. Lines: 60
  12. In-Reply-To: plummer@cs.swarthmore.edu's message of 16 Nov 92 23:07:04 GMT
  13.  
  14.  
  15. If you're looking for an interactive system, you might try FOL or
  16. its derivative, GETFOL.  Contact Fausto Giunchiglia, at fausto@irst.it or
  17. fausto@dist.unige.it for more info.  Weyhrauch80 describes FOL.
  18.  
  19.     -ian
  20.  
  21. @article(Weyhrauch80,
  22.         Author = {Weyhrauch, Richard W.},
  23.          Title = {Prolegomena to a Theory of Mechanized Formal Reasoning},
  24.           Year = {1980},
  25.        Journal = AI,
  26.         Volume = {13},
  27.          Pages = {133--170})
  28.  
  29. thread:
  30. On 16 Nov 92 23:07:04 GMT, plummer@cs.swarthmore.edu (David Barker-Plummer) said:
  31. > In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:
  32.  
  33. >JJ> In article <4804@equinox.unr.edu> mjb@dws020.unr.edu (Mike Brown) writes:
  34. >>I am looking for programs that will do proofs like:
  35. >>            Prove: Q            \
  36. >>    1 P then Q    Premis               > The problem
  37. >>    2 P        Premis              /
  38. >>    3 Q             1, 2, Modus Ponens  >  The program's proof
  39. >>
  40. >>(The proofs do get more involved)
  41. >>
  42. >>Is there a program out there that will do these proofs?
  43.  
  44. >JJ> I saw two responses to this post, recommending Otter and HOL.  I think they
  45. >JJ> made it clear that they were probably not what Mike Brown was looking for.
  46. >JJ> The Otter and HOL versions of this very simple proof don't look a whole lot
  47. >JJ> like Mike's very clear presentation.  I've read the book about Otter and 
  48. >JJ> learned/used a little of HOL; they are both powerful research systems, with
  49. >JJ> all that entails.
  50.  
  51. >JJ> I think what the original post was asking for was a simple natural
  52. >JJ> deduction prover for propositional logic, where the problem
  53. >JJ> statements and proofs look much as they do in a logic textbook.
  54. >JJ> Do such things exist?  The nearest thing I have read about is
  55. >JJ> "Muffin: A Proof Assistant", a chapter by Richard C. Moore in
  56. >JJ> Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT,
  57. >JJ> Prentice Hall International, 1990. I recall the chapter saying
  58. >JJ> something about Muffin being made available.  I wonder if anyone
  59. >JJ> is using it.
  60.  
  61. > Andrews' system, ack I can't remember its name right now, allws you to
  62. > construct proofs in exactly the standard natural deduction
  63. > presentation of the original poster's example.  Contact Peter Andrews
  64. > at CMU.  Of course, the underlying logic of this prover is typed
  65. > higher order logic, and is significantly more powerful (and hence
  66. > harder to understand) than the simple example would suggest.
  67.  
  68. > Another system that comes to mind is MacLogic developed by Roy Dychoff
  69. > at St. Andrews University (rd@cs.st-and.ac.uk).  I am not sure of the
  70. > availability, but this is the sort of system I would choose for
  71. > teaching natural deduction to neophytes.
  72.  
  73. > -- Dave
  74.