🚀 go-pugleaf

In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:
>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?
>
>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.
>

Muffin developed into "mural", a WIMP interface proof assistant for
natural deduction proofs (i.e. proofs much like the example above).
As a proof assistant, it leaves the user to decide that Modus Ponens
is the rule to apply (although there are various forms of assistance
for the choice).  Full details are in "mural: a formal development
support system" by C.B.Jones et al, Springer 1991.  ISBN 3-540-19651-X.

mural is generally available at modest cost.  It is a large SmallTalk
image, so can only be supplied to people with an appropriate SmallTalk
license (hence no FTP).  For details, contact richard@cs.man.ac.uk
(non-educational users) or br@inf.rl.ac.uk (universities and similar
bodies).

Tim Clement