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).
Josef, that's great, and Mizar is fine. Can you show me your 300 lines of Mizar code, and tell me how to run it on Vampire? Why not even make it shorter by taking out Gupta's theorem etc which Vampire won't prove in one line? I see there's prover9 stuff in the Hol Light distribution, e.g. hol_light/Examples/prover9.ml. I think you're pointing to something I need to explain in my geometry paper, which we might call the difference between ATPs and Mizar. Now ATP means Automated theorem prover? So Mizar is not an ATP, but as it only checks quite detailed proofs? I want to say that miz3 can be used as an ATP, unlike Mizar, but miz3 isn't a very efficient ATP (taking maybe 3 hours to prove my simple result Line01infinity2_THM which is just a set-theoretic restatement of the uniqueness part of axiom I1, 2 points uniquely determine a line), and vampire or prover9 is a much more efficient ATP. -- Best, Bill ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
