🚀 go-pugleaf

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?

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

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

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA