🚀 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"