🚀 go-pugleaf

mjb@dws014.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)
Isn't this just what a theorem prover does? You could try for example
Otter which is available in ANL.

----- OTTER 2.2, July 1991 -----
The job began on cs, Thu Nov 12 12:32:19 1992
The command was "otter".

set(binary_res).
set(factor).
assign(stats_level,1).

list(usable).
1 [] -P | Q.
2 [] P.
end_of_list.

list(sos).
3 [] -Q.
end_of_list.

given clause #1: (wt=1) 3 [] -Q.
** KEPT: 4 [binary,3,1] -P.

----> UNIT CONFLICT at   0.01 sec ----> 5 [binary,4,2] .

Level of proof is 1, length is 1.

---------------- PROOF ----------------

1 [] -P | Q.
2 [] P.
3 [] -Q.
4 [binary,3,1] -P.
5 [binary,4,2] .

------------ end of proof -------------

So You just insert premises in axioms and deny the conclusion, theorem
prover then finds a contradiction. You can find the software
from 140.221.10.1 = anagram.mcs.anl.gov.

>Mike Brown, mjb@cs.unr.edu    "I am the scratch monkey"

In article <4804@equinox.unr.edu>, mjb@dws014.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)
|> 
|> I have looked around, but can't find a program for this.
|> (I tried archie searches for many keywords and didn't find a program)
|> 
|> Is there a program out there that will do these proofs?
|> 
|> Thanks
|> --
|> Mike Brown, mjb@cs.unr.edu    "I am the scratch monkey"

You can do this in the HOL theorem prover (several ways).

* 1: Backward Proof.

$ hol


===============================================================================
         HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
===============================================================================

#set_goal (["P ==> Q"; "P:bool"], "Q:bool");;
"Q"
    [ "P" ]
    [ "P ==> Q" ]

() : void

#e (MP_TAC (ASSUME "P:bool"));;
OK..
"P ==> Q"
    [ "P" ]
    [ "P ==> Q" ]

() : void

#e (ACCEPT_TAC (ASSUME "P ==> Q"));;
OK..
goal proved
. |- P ==> Q
.. |- Q

Previous subproof:
goal proved
() : void

#quit ();;
Bye.
$

* 2: Forward Proof

$ hol


===============================================================================
         HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
===============================================================================

#top_print print_all_thm;;
- : (thm -> void)

#let th1 = ASSUME "P ==> Q";;
th1 = P ==> Q |- P ==> Q

#let th2 = ASSUME "P:bool";;
th2 = P |- P

#let th3 = MP th1 th2;;
th3 = P ==> Q, P |- Q

#quit ();;
Bye.
$

* 3: Let HOL do a backward proof for you.

$ hol


===============================================================================
         HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
===============================================================================

#set_goal (["P ==> Q"; "P:bool"], "Q:bool");;
"Q"
    [ "P" ]
    [ "P ==> Q" ]

() : void

#e RES_TAC;;
OK..
goal proved
.. |- Q

Previous subproof:
goal proved
() : void

#quit ();;
Bye.
$

===============================================================================
Jim Grundy               
University of Cambridge | Phone: +44 223 334760            | This space has
Computer Laboratory     | Fax:   +44 223 334678            | been intentionally
New Museums Site        | Telex: CAMSPLG 81240             | left blank for
Pembroke Street         | email: jg@cl.cam.ac.uk           | formatting
Cambridge  CB2 3QG      |                                  | purposes.
UNITED KINGDOM          |                                  |
===============================================================================

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

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

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

In <IMG.92Nov17114848@hope.aisb.ed.ac.uk> img@aisb.ed.ac.uk (Ian Green) writes:


>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})

As I recall there are several programs that do FOL proofs in a natural
deduction system for the Mac and for IBM-clones.  The ones I'm
thinking of aren't theorem provers, but are more like proof checkers.
I know that Tarski's World (by Barwise and Etchemendy) is available both
for the macintosh and for windows.  If that's the sort of thing you're looking
for then there are several others also (tho I can't at the moment recall the
titles).  Someone was demo'ing an IBMish program at the last APA conference
I attended.

If that's the sort of thing you're looking for then you might ask on
philos-l.  I seem to recall that a list of such programs circulated there not
too long ago.

jim hardy

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