[isabelle] A Mechanical Verification of the Independence of Tarski's Euclidean Axiom



At the end of June, I deposited with my university library the final
version of my MSc thesis, A Mechanical Verification of the Independence
of Tarski's Euclidean Axiom.  Because this mechanical verification was
performed using Isabelle (and because I've mentioned it previously on
this list) I thought people here might be interested in a link to it:
http://researcharchive.vuw.ac.nz/handle/10063/2315
The full text of the thesis is freely downloadable, as well as
supplementary files, which include all my .thy files.

As explained in the thesis, I ended up using Isabelle 2009--2, but I do
intend to update the files to work with the latest version of Isabelle,
and then submit at least some of them to AFP.

Because of busyness leading up to the deposit of my thesis, and a
four-week overseas trip in July, there are a lot of messages sent to
this list that I haven't read (763 right now), but I think I've read all
the ones containing the word "geometry".  I might try to catch up over
time, but in the meantime, I mightn't be fully up to date, and if you
want to draw something to my attention, it's probably best to CC it to
me, rather than assuming I'll see what you post to the list.

Tim
<><

Attachment: signature.asc
Description: OpenPGP digital signature



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