Hi John > | 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
OK, I should have looked at your code first :-). > 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? http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/ott2miz/ott2miz.el?rev=1.18&view=auto But Mizar has only quite high-level steps which probably makes things easier. > How did you figure out the proof format? Probably also just by looking at it, possibly also from the Ivy paper and some Otter documentation. I think I debugged it by running on the whole TPTP couple of years ago. Josef ------------------------------------------------------------------------- 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
