Hi Josef,
| you can get a very detailed and easily checkable output from Prover9 by
| using its Ivy proof objects (they are so simple that I even wrote a Mizar
| import for it :-). It used to be an option to Otter, but it seems that
| Bill now has a special tool for it: prooftrans
| http://www.cs.unm.edu/~mccune/prover9/manual/2008-04A/prooftrans.html .
| Search for IVY Proofs on that page.
Yes, in fact that's just what I'm doing:
let retcode = Sys.command
(prover9 ^ " -f " ^ filename_in ^ " | prooftrans ivy >" ^ filename_out) in
I agree that the proof format is simple, but I've never seen any
explicit documentation beyond a brief paragraph on the Web page above.
That's why I just reverse-engineered it from examples. The obvious
alternative would be to read the source code for Ivy, which is what
Bill McCune suggested when I asked him.
I didn't know about your Mizar importer; is it available? How did you
figure out the proof format?
John.
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
