Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Jeremy, if you or anyone else wants to talk about Euclid off-line, I'd
be happy to talk.  As I try to explain in my paper, I love the Elements
http://www.math.northwestern.edu/~richter/hilbert.pdf
It's very creative and forms the basis of non-Euclidean geometry.

Thanks, Chris, that's very helpful.  I'll look for the red wavy error
lines in jedit.  I'll look at /src/HOL/ex/.  I've looked at
tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good.
Thanks for explaining simp, blast etc, although I don't really know
what you mean.  Is there somewhere an FOL example, with a long
(perhaps indigestible) single step "rule" method proof, which is
shortened with simp, and then shortened even more with blast & auto?

   (In courses it is often done that students are only allowed to use
   certain rules in order to proof a statement, since the automatic
   tools would outright solve many typical examples.)

Wow!  Can you point me to any of these courses?  That sounds like what
I need to know.  As I posted earlier, I'm mostly trying to cite some
good code for my geometry paper above (which I'll then submit).  I
don't have to write the code myself, although I did
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
Examples of real classroom situations where students hand in Isabelle
proofs would be fantastic!  Dunno about Europe, but US public schools
are really gungho about computer applications.

-- 
Best,
Bill 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.