Thanks for replying and the code, John. I'll send you a bug reports on mizar modes in 3.0.9, and a bug report on the latest HOL Light as well. Right now I've been taking Freek's advice to try to learn Isabelle. It's been rough, and I'm ready for HOL Light again.
| Your geometry links don't seem to jibe well with my paper above. Well, there are lots of degrees of freedom over how to axiomatize geometry, what level of automation you want and what your overall goals are in mechanization and formalization. But in any case, I just wanted to indicate how you might get started if you do want to use HOL Light. John, I argued with folks on the isabelle newsgroup as well about Euclid and Hilbert. It'd be nice to settle this argument. I say that Euclid's work is well worth studying, very creative, and the basis of non-Euclidean geometry. But you can't code up Euclid proofs! Euclid's axioms aren't strong enough to prove much. With Hilbert's axioms, you can prove all of Euclid's propositions. Proof assistants like HOL Light will show all those Hilbert proofs are correct, and there's an interesting possibility of teaching a geometry course where students code up their rigorous axiomatic Hilbert proofs. Anyone interested in this need to read Greenberg's book, or Hartshorne's or my paper http://www.math.northwestern.edu/~richter/hilbert.pdf Scott, Fleuriot & Meikle are instead using proof assistants like HOL Light to read Hilbert's book FoG. That's a worthy task, as FoG is very hard to read. But that's like reading a literal translation of Euclid, where you find this incomprehensible statement of Prop I.7: ``On the same straight-line, two other straight-lines equal, respectively, to two (given) straight-lines (which meet) cannot be constructed (meeting) at a different point on the same side (of the straight-line), but having the same ends as the given straight-lines.'' It says if two circles intersect in two points, then the intersection points are on opposite sides of the line connecting the centers of the two circles :) See Heath, p 259--260, or p 16 of my paper. When we talk of Euclid, we mean Euclid, Proclus, Pappus, and all the other Euclid scholars up to Heath. We don't mean just Euclid. Similarly, when we talk of Hilbert, we have to talk about Hartshorne, Greenberg etc. We can't just read Hilbert's FoG in ``Greek.'' -- 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
