🚀 go-pugleaf

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          |                                  |
===============================================================================