*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Mon, 30 Apr 2012 15:44:52 +1200*Cc*: richter at math.northwestern.edu*In-reply-to*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120412 Thunderbird/11.0.1

At the end of February, I submitted my Master's thesis, which was about an Isabelle formalization of the independence of the parallels postulate. Specifically, I chose Tarski's axioms, and showed that his Euclidean axiom (Axiom 10 in Metamathematische Methoden in der Geometrie) is independent of the others, by proving that the Klein--Beltrami model of the hyperbolic plane satisfies the rest of Tarski's axioms, but not the Euclidean axiom. As you will have gathered, my work was primarily about models of Tarski's axioms, rather than consequences of them, but if you're interested, ask me off-list, and I can send you a copy of my thesis, or my Isabelle files, or whatever interests you. Please understand, though, that I haven't heard back from the examiners yet, and I think they're entitled to ask me to make changes to my thesis, so what I send you shouldn't be considered to be the final version of my thesis. Tim <>< On 29/04/12 08:58, Bill Richter wrote: > 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. >

**Attachment:
signature.asc**

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

**References**:**[isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] Specifying subtype in a locale
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- 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