Hi Bill, > Josef, let me try again. I apologize for not knowing the terminology or > anything about Vampire. Would there be a way to turn my 971 lines of Tarski > code http://www.math.northwestern.edu/~richter/TarskiAxiomGeometryCurry.ml > (which for Freek I made all my predicates official curried HOL functions, in > order to show that holby is weaker than Mizar) into say 150 lines of 1-line > proofs that a top FOL prover would then verify? I think you did something > like, but don't have the 150 line file.
Yes. But I do it now only for Mizar, and I told you the results (the shortening would be about 1400 lines of your Mizar code to some 300, if ATPs could prove everything). We (mostly Cezary Kaliszyk) might have a similar bridge to ATPs for HOL Light quite soon (but don't ask me to try it now :-). If you want to experiment in this direction, Isabelle has currently the most polished bridge to ATPs, ask there. Or you can also try the bridge to Prover9 by John Harrison, which already works in HOL Light (again, don't ask me how, I only saw the code there :-). Best, Josef ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
