I'm not a HOL Light expert (nor a mathematician in fact), but here are a
couple of thoughts:
About axioms: You can assert new axioms using new_axiom (
http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/new_axiom.html). The page
discusses the alternatives too.
Your comments on teaching rigorous axiomatic geometry strike a cord.
Geometry traditionally emphasizes axioms and proofs, so why not formal
proofs these days when we have tools for working with formal proofs?
Perhaps you might be interested in a recent paper that has been pointed
out to me: "A Formal System for Euclid's Elements" (
http://repository.cmu.edu/cgi/viewcontent.cgi?article=1020&context=philosophy).
This looks at using formalization closer to Euclid's own.
Cheers,
Cris
On Sat, Apr 21, 2012 at 9:53 PM, Bill Richter <[email protected]
> wrote:
> I think we should teach rigorous axiomatic geometry in high school
> with the aid of formal proof checkers like HOL Light, promoted by Tom
> Hales's Notices article. I think HOL Light needs better documentation
> before this is possible, and maybe new code, and I'll work on it. I
> need help porting my 1500 lines of Tarski geometry axiom Mizar code
> http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar to
> HOL Light Light. Details:
>
> I wrote a paper (for my 13yo son, who read it carefully) on Hilbert's
> axioms http://www.math.northwestern.edu/~richter/hilbert.pdf as a
> bridge between Moise & Venema's rigorous geometry texts and
> Hartshorne's exciting but not-too-rigorous Euclid/Hilbert book. But
> to make rigorous axiomatic geometry a possibility in high school, I
> think we need to tie it into the formal proof revolution, with the
> spin that kids will learn computer programming skills that will help
> them get jobs in the new field of formally checking software.
>
> I built an old version 3.09 of HOL Light (I failed to build the newest
> with camlp5) and was completely bufuddled by John Harrison's 1000
> pages of dox (tutorial & reference manual). How do a write down a
> list of axioms and get HOL to check my axiomatic proofs? A big part
> of the dox problem, I believe, is explained in John's thesis, which is
> about proving theorems in the real line with the aim of formally
> proving mathematical theorems needed to show the correctness of
> floating point computer processors. That's a long way from axiomatic
> geometry proofs. I'm certainly prepared to like HOL Light, which is
> based on ML, a Scheme-like language. I'm a pretty good Scheme
> programmer, and coached my son to write a nice Racket Sudoku solver on
> http://schemecookbook.org/Cookbook/SudokuSolver.
>
> So I switched to Mizar (which Tom's paper cites), which boasts of it's
> bad dox, and sorta figured it out, and wrote 1500 lines of Mizar code
> trying to prove Hilbert's geometry axioms from Tarski's. I more or
> less coded up Julien Narboux's proofs which he explains in the form of
> Coq code in http://dpt-info.u-strasbg.fr/~narboux/tarski.html My first
> step is port my code to HOL. I tried to use the various Mizar modes,
> but I couldn't run any of them in HOL 3.09, and I also couldn't
> understand how to write up such proofs.
>
> I think I made improvements to Julien's exposition, and my Mizar code
> is much more readable than his Coq code, and also more readable than
> the JHilbert code written by wikiproofs
>
> http://www.wikiproofs.de/w/index.php?title=Interface:Tarski%27s_geometry_axioms
> where I first learned how to use Tarski's axioms. I believe that
> Julien was porting proofs from the 1983 book Metamathematische
> Methoden in der Geometrie by W. Schwabhäuser, W Szmielew, and
> A. Tarski, and he got as far as Gupta's amazing proof of (more or
> less) Hilbert's axiom I1 that two points determine a line. It's
> amazing how weak Tarski's axioms are!
>
> There's no good Mizar documentation, but there are a number of pdf
> files with examples, and that sufficed for me. There seems to be no
> way of saying `` let's derive consequences of these axioms.'' So I
> would have liked to say, let S be a model of Tarski's axioms, i.e. a
> set S with betweenness and equidistance relations satisfying these 9
> axioms. I think in Mizar you can only do that if you first show that
> a model of the axioms actually exist. And of course R^2 is a model,
> but that would take work to show, and I'd have to learn the Mizar of
> the real line, and I didn't do it. Instead I stumbled on the odd
> solution of making the axioms into theorems, and then I cite these
> axiom-theorems in my proofs. It's an OK solution if one starts on
> line 200 (my first actual proof) and only looks upward to find the
> statement of the axioms. Mizar has a particularly annoying feature of
> not allowing TABs or the symbols for implies etc which Isabelle/Isar
> (which I never built or understood) uses. So I wrote some emacs code
> .mizar-isar.el which gets around this. Now I write up my Mizar code
> in Isar fashion, using the forbidden symbols ⇒ ¬ ∨ ∧ ≡ ∀ ∃ ⇔ and not
> worrying about TABs, and then run my function isar->mizar which copies
> this file to joe.miz and rewrites it so Mizar will compile it. I also
> bound the forbidden symbols to keys for easy typing.
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> For Developers, A Lot Can Happen In A Second.
> Boundary is the first to Know...and Tell You.
> Monitor Your Applications in Ultra-Fine Resolution. Try it FREE!
> http://p.sf.net/sfu/Boundary-d2dvs2
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
