Re: [isabelle] Advertise your work on the mailing list



On Tue, 26 Oct 2010 04:55:48 Jasmin Christian Blanchette wrote:
> Now it's your turn!

I'm working on establishing that "Euclid's Axiom" in Tarski's 
axiomatization of the plane is independent of the other axioms.  
I've already provided a (real, Cartesian) model for all of 
Tarski's axioms, thus establishing that they are consistent 
(relative to Isabelle/HOL).

My independence proof involves building the Beltrami-Klein model 
of the hyperbolic plane and then establishing that Euclid's Axiom 
is false in that model, but all the other axioms are true.

Timothy
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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