> | Julien Narboux, who used Coq to prove Tarksi theorems, said something > | like that, and I just don't understand. It took me 300 lines to > | (porting Julien) prove Gupta's amazing theorem that 2 points determine > | a line. I found it exhilarating, not painful. My problem is math: I > | don't know how to prove the rest of Hilbert's axioms. I don't know > | how to prove the full Pasch axiom (Tarski's axiom is 1/3 of that). > > This reminds me of something Andrzej Trybulec said about automated > theorem provers: why should we let the machine deprive us of the > pleasure of proving things?
I just tried this, and it turns out that Vampire (fitting name) would fully deprive us of this pleasure in all but five theorems in Bill's article :-). This could make a cheap way how to get a fast gratification when translating to HOL Light: first only translate the theorems (not the proofs), and call the HOL Light's Prover9 or MESON tactic with the list of theorems used in the Mizar proof. If you tell me (best by examples) how to map the Mizar symbols and terms to concrete HOL Light syntax, I can probably automate that. 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
