🚀 go-pugleaf

In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:

JJ> In article <4804@equinox.unr.edu> mjb@dws020.unr.edu (Mike Brown) writes:
>I am looking for programs that will do proofs like:
>			Prove: Q            \
>	1 P then Q	Premis               > The problem
>	2 P		Premis              /
>	3 Q             1, 2, Modus Ponens  >  The program's proof
>
>(The proofs do get more involved)
>
>Is there a program out there that will do these proofs?

JJ> I saw two responses to this post, recommending Otter and HOL.  I think they
JJ> made it clear that they were probably not what Mike Brown was looking for.
JJ> The Otter and HOL versions of this very simple proof don't look a whole lot
JJ> like Mike's very clear presentation.  I've read the book about Otter and 
JJ> learned/used a little of HOL; they are both powerful research systems, with
JJ> all that entails.

JJ> I think what the original post was asking for was a simple natural
JJ> deduction prover for propositional logic, where the problem
JJ> statements and proofs look much as they do in a logic textbook.
JJ> Do such things exist?  The nearest thing I have read about is
JJ> "Muffin: A Proof Assistant", a chapter by Richard C. Moore in
JJ> Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT,
JJ> Prentice Hall International, 1990. I recall the chapter saying
JJ> something about Muffin being made available.  I wonder if anyone
JJ> is using it.

Andrews' system, ack I can't remember its name right now, allws you to
construct proofs in exactly the standard natural deduction
presentation of the original poster's example.  Contact Peter Andrews
at CMU.  Of course, the underlying logic of this prover is typed
higher order logic, and is significantly more powerful (and hence
harder to understand) than the simple example would suggest.

Another system that comes to mind is MacLogic developed by Roy Dychoff
at St. Andrews University (rd@cs.st-and.ac.uk).  I am not sure of the
availability, but this is the sort of system I would choose for
teaching natural deduction to neophytes.

-- Dave