Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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





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