I'm sorry, this is the public link to my formalization:
http://dl.dropbox.com/u/27199680/Tarski%20-%20HOL%20Light/Tarski-HOL%20Light.hl
Lorenzo Mannini
---------- Forwarded message ----------
From: Lorenzo Mannini <[email protected]>
Date: 2012/7/4
Subject: Re: hol-info Digest, Vol 73, Issue 28
To: [email protected]
As I wrote some months ago, I've been developping my own formalization of
Tarski's system of geometry in HOL Light, following Narboux's example in
Coq (http://dpt-info.u-strasbg.fr/~narboux/tarski.html). I've reached the
eight chapter - concerning orthogonality - focusing mainly on "getting the
job done".
This has been my master thesis, under Marco Maggesi's superivision, and my
first formalization experience.
That said, I'll join my code, in case someone may find it useful.
Best Regards,
Lorenzo Mannini
------------------------------------------------------------------------------
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
