Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
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
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.
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and