🚀 go-pugleaf

If you're looking for an interactive system, you might try FOL or
its derivative, GETFOL.  Contact Fausto Giunchiglia, at fausto@irst.it or
fausto@dist.unige.it for more info.  Weyhrauch80 describes FOL.

	-ian

@article(Weyhrauch80,
        Author = {Weyhrauch, Richard W.},
         Title = {Prolegomena to a Theory of Mechanized Formal Reasoning},
          Year = {1980},
       Journal = AI,
        Volume = {13},
         Pages = {133--170})

thread:
On 16 Nov 92 23:07:04 GMT, plummer@cs.swarthmore.edu (David Barker-Plummer) said:
> 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