Dear Bill,
Two small notes:
HOL Light is not the only HOL. I usually use HOL4 (hol.sf.net), which you
may find easier to install and use (and may even have better docs). (I
often have trouble with campl5 and checkpointing when trying HOL Light.) I
think good arguments can be made for Isabelle/HOL (and possibly also for
Coq) having the best user experience as far as documentation, user
interface, and existing libraries are concerned. But as Makarius suggested,
you should investigate the culture surrounding each option. I can give a
more extensive list of proof assistants if you're interested.
"How do a write down a list of axioms and get HOL to check my axiomatic
proofs?"
The usual approach (at least in the HOL family of provers) is to work with
definitions rather than new axioms.
The idea is that the axioms and inference rules for a general-purpose logic
(HOL) are built into the system, and you model whatever you're interested
in within that logic by defining new types and constants and proving things
about them.
You can end up with something that looks like the axiomatic approach this
way either by deeply embedding your proof system within HOL (e.g. define
datatypes of geometry formulae and proofs and prove things like |- Provable
someFormula as theorems of HOL), or by shallowly embedding your objects of
interest within HOL (e.g. you might define Tarski's betweenness and
congruence relations as relations in HOL, making the definitions match the
axioms governing those relations, then prove stuff about them).
I would usually recommend the latter, but it depends on what you want to be
able to say at the end...
Cheers,
Ramana
On Sun, Apr 22, 2012 at 5:53 AM, 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
