I've just been following Narboux's development to the end of the eight
chapther (concerning Orthogonality), that is actually the same scheme
pursued by Tarski in the Metamathematische Methoden in der Geometrie.
Unfortunately this first part is mainly focused on the development of the
concept of orthogonality, that requires many easy but tedious proofs. Many
of theme concern the middle point and otherwise obvious geometrical
properties.
I've never worked before with miz3, but I'd be glad to try.
Best regards,
Lorenzo Mannini
2012/7/5 Bill Richter <[email protected]>
> Lorenzo, thanks for posting your Tarski-HOL Light.hl, an impressive
> 2392 lines of code! I'm really getting a lot out of sets.ml, of which
> your advisor Marco Maggesi has the latest copyright.
>
> I'm not good enough at HOL Light to read your code. Can you explain
> what you proved, and maybe something about how you used HOL Light?
> I'm curious about whether you could rewrite your code using miz3, as I
> do. Julien Narboux posted this on the isabelle newsgroup:
>
> I appreciate your work, your proofs seem to be really more readable
> than Coq proofs. Of course my LCF style proofs are not meant to be
> readable. In fact, I believe that these proofs about Tarski's
> axioms are really low level and it is hard to have intuition about
> the proofs because there are basic facts which are hard to prove
> (for instance existence of the midpoint arrives only at chapter 7
> !) and therefore it is not really the kind of proof one wants to
> show in high-school, that is why I did not try to produce readable
> proofs.
>
> I think Julien did a great job in his code, and I know very little
> about Tarski axiomatic geometry that I did not learn from Julien. But
> I don't understand his position here, as I found it a real pleasure to
> code up (first Mizar and then) miz3 proofs of what I know
> http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
>
> I could not prove Hilbert's full Pasch axiom from Tarski's axioms. Do
> you know how to do this? Julien had not done this, so I couldn't port
> his proof. I see Julien has rewritten his web page
> http://dpt-info.u-strasbg.fr/~narboux/tarski.html
> but I can't figure out if he's proved it yet.
>
> --
> Best,
> Bill
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
