*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Josef Urban <josef.urban at gmail.com>*Date*: Mon, 30 Apr 2012 11:30:50 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201204300355.q3U3tgBd020699@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <201204300355.q3U3tgBd020699@poisson.math.northwestern.edu>

Hi Bill, On Mon, Apr 30, 2012 at 5:55 AM, Bill Richter <richter at math.northwestern.edu> wrote: > Josef, as you're a real Mizar expert, I'll be grateful if you look at > http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar Superficially it looked OK. But there are better experts than me, and you can get reviews and suggestions if you submit the article to MML. > 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. I just saw the extensive discussion on the hol list, and I don't think I can add much. Particularly John knows really a lot. One recent comparison talk by Freek is at www.cs.ru.nl/~freek/talks/lsfa.pdf . > > Could you just get me started on Isabelle? Why me? :-) There are so many Isabelle experts here. Best, Josef > 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

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

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

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

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] A course based on Isabelle/HOL and some feedback...
- 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