*To*: Josef Urban <josef.urban at gmail.com>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sun, 29 Apr 2012 22:55:42 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> (message from Josef Urban on Mon, 30 Apr 2012 00:48:32 +0200)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com>

Josef, as you're a real Mizar expert, I'll be grateful if you look at http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar I'll endure pain to manually transform my 1467 lines of Mizar Tarski geometry proofs to Isabelle (or Coq or HOL Light even). I'm grateful to the Mizar folks for writing a language I could learn and code up my Tarski proofs, not least because I now believe my proofs. But I think Mizar is too clunky a language to recommend high school students to code in. That brings up HOL Light's Mizar mode, as you mentioned, or Freek's miz3, but I couldn't get any of them to run on HOL Light 3.09, nor could I compile the latest version of HOL Light, and Freek suggests often that Isabelle is an improvement over Mizar. Could you just get me started on Isabelle? I finally ran the executable ./Isabelle, and up popped jedit. I'm reading various Isabelle dox, and it's all great, but I haven't found what I want: How do we code up first order logic (FOL) proofs that follow from some FOL axioms? I really think the Isabelle dox ought to explain this. You can't exactly do that in Mizar, I believe, and maybe you can't do it in any of the proof assistants. Mizar is all about set theory (using I think Tarski's FOL set theory axioms), so we have to talk instead about a model of my FOL axioms. That's fine. So we have to define some ``class'' of mathematical objects, which is the sets, functions & relations that define a model. In my case, that's a set S with a 3-ary and 4-ary relation equiv and between satisfying various properties (Tarski's axioms). Now we have to code up proofs about this class i.e. prove theorems about models of Tarski's axioms, which amounts to the FOL proofs we want. This must be explained somewhere in the Isabelle dox. -- Best, Bill

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

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

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

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- 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