Lorenzo, thanks for posting your Tarski-HOL Light.hl, an impressive 2392 lines of code! I'm really getting a lot out of sets.ml, of which your advisor Marco Maggesi has the latest copyright.
I'm not good enough at HOL Light to read your code. Can you explain what you proved, and maybe something about how you used HOL Light? I'm curious about whether you could rewrite your code using miz3, as I do. Julien Narboux posted this on the isabelle newsgroup: I appreciate your work, your proofs seem to be really more readable than Coq proofs. Of course my LCF style proofs are not meant to be readable. In fact, I believe that these proofs about Tarski's axioms are really low level and it is hard to have intuition about the proofs because there are basic facts which are hard to prove (for instance existence of the midpoint arrives only at chapter 7 !) and therefore it is not really the kind of proof one wants to show in high-school, that is why I did not try to produce readable proofs. I think Julien did a great job in his code, and I know very little about Tarski axiomatic geometry that I did not learn from Julien. But I don't understand his position here, as I found it a real pleasure to code up (first Mizar and then) miz3 proofs of what I know http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml I could not prove Hilbert's full Pasch axiom from Tarski's axioms. Do you know how to do this? Julien had not done this, so I couldn't port his proof. I see Julien has rewritten his web page http://dpt-info.u-strasbg.fr/~narboux/tarski.html but I can't figure out if he's proved it yet. -- 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
