John, thank you very much for writing the Tarski geometry miz3 code!
I'll try to code the rest of it up. You improved on my code in one
important way, getting rid of my constant TarskiModel
b,a ≡ a,b by A1, TarskiModel;
hence a,b ≡ a,b by A2, TarskiModel;
and writing it more nicely as
b,a === a,b by 0,A1;
thus a,b === a,b by 0,A2;
I don't mind quantifying over free variables. I prefer to. But these
6 lines in every theorem/proof hurt readability.
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
What if we go to the mile long theorem, so we'd only state these 6
lines once. Or can me make some, uh, global declaration?
I think that's about it. Checking proofs that are already presented
in a precise and explicit axiomatic style is not so difficult. But
there aren't that many domains where we find such proofs. Besides
synthetic geometry, Landau's real number construction was another
particularly favorable example and it's no accident that it was
formalized early, by Jutting in AUTOMATH. But indeed, the mechanics
of basic proof checking is not that hard. You can of course read
all about this and more in my textbook, so you can code it all
yourself and don't need to rely on any fancy prover :-)
Thanks, that's nice, and I should read your book. But of course using
such a simple self-coded basic proof checker defeats my selling point
of propelling my students into the new hot world of proof assistants.
--
Off to code!
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
