Thanks, John! Sorry I don't have my bug reports yet. I'm using Scientific Linux, not Debian, so I can't use Hendrik's package.
While I'm very interested in the idea of formalizing geometry axiomatically, and I'm happy people are doing it in HOL Light, What I'm trying to do is much simpler than what Phil etc are doing. It should be trivial in HOL Light. It shouldn't require the full strength of Freek's ambitious miz3. I just want 2-column high school Geometry proofs. I'll use Hilbert's or Tarski's axioms, which actually give rigorous proofs, but it's still 2-column proofs. Phil is trying to get HOL Light to fix profs from Hilbert's arcane book, that takes a real theorem prover. BTW what do you call HOL Light? Is it a proof assistant, or a theorem prover, or a proof checker? -- 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
