*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sat, 28 Apr 2012 15:58:09 -0500

Hi, I'm a mathematician writing a rigorous axiomatic geometry paper http://www.math.northwestern.edu/~richter/hilbert.pdf using Hilbert's axioms. I want to cite geometry proofs nicely coded and checked by proof-checker like Isabelle. I've written Mizar code http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar and I want to port it to Isabelle, which Freek Wiedijk seems to suggest is an improvement. Makarius has been helping me, and he said I should ask here about formalizations of geometry. My feeling, which could be mistaken, is that Coq and HOL Light are primarily theorem-provers (procedural) and require considerable tweaking to allow folks to type in readable axiomatic geometry (declarative) proofs, but that Isabelle is both procedural and declarative. My Mizar code is a largely a port of Julien Narboux's Coq pseudo-code http://dpt-info.u-strasbg.fr/~narboux/tarski.html. I partially prove the theorem of the 1983 book Metamathematische Methoden in der Geometrie by Schwabhäuser, Szmielew, and Tarski, that Tarski's (extremely weak!) plane geometry axioms imply Hilbert's axioms. I get about as far as Narboux, with Gupta's amazing proof which implies Hilbert's axiom I1 that two points determine a line. I don't think my Mizar code is that great, but it's a lot more readable than Julien's Coq pseudo-code. No doubt some Mizar experts could improve my code, but I'm putting them off as a last resort, because Mizar seems unsuitable as a language to use in a high school math class. So I'd appreciate your Isabelle help, including the easiest way run Isabelle programs. Do I really need Proof General? I'll also accept geometry help! I haven't seen Schwabhäuser's book, and I can't see how to go any farther with Tarski's axioms. I'm basically missing Hilbert's Pasch Betweenness axiom (Tarski's axiom is about 1/3 of it) and Hilbert's angle construction axiom. -- Best, Bill

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Ramana Kumar

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Josef Urban

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tim (McKenzie) Makarios

- Previous by Date: [isabelle] fwd:
- Next by Date: Re: [isabelle] size_changes raises Option and Bind
- Previous by Thread: [isabelle] fwd:
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list