Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
Jeremy, I'll look at your paper, but don't want to discuss Euclid with
you or anyone else here unless they understand Hilbert's formal (not
informal) first order axiomatization of plane geometry as explained in
Hartshorne's book: 3 incidence axioms, 4 betweenness axioms, 6
congruence axioms, the parallel postulate and the circle-circle axiom.
With these axioms, you can prove every plane geometry result Euclid
stated, and you ought to be able to code the proofs up nicely in
Isabelle, and maybe even teach a high school or college course where
the students code up their own rigorous axiomatic Hilbert proofs. You
can't code up proofs of Euclid's propositions using Euclid's axioms.
Your paper is relevant to this group if you can code up your
enhanced-Euclid proofs in Isabelle. I couldn't tell from my brief
glance at your paper if this is possible. What do you think?
This archive was generated by a fusion of
Pipermail (Mailman edition) and