Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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 





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