Thanks, Konrad! Are you and Michael interested in adding more introductory material to your HOL4 Logic manual, e.g. along the lines of the excellent intro material Michael just posted? If so, I might have useful feedback. Or do you want to keep your manual in its present form? When I hit your link http://www.cl.cam.ac.uk/ftp/hvg/papers/HOLPaper.ps.gz I only get p 26, the end of the bib. I tried reading the hol88 docs that John recommended, and I'm not sure I found the right stuff (just outline.dvi & paper.dvi), but it seemed short. Would you compare the Logic manual to the hol88 docs?
Here's a dumb HOL question. I keep failing to find where someone says, "In HOL we can do most of the set theory mathematicians generally do". And maybe I'm all wrong! Maybe HOL is a different way to formalize math not primarily based on set theory! Thierry Coquand's article Cris found for me http://plato.stanford.edu/entries/type-theory/ How can we explain the notion of sets in term of types? There is an elegant solution, due to A. Miquel, which complements previous works by P. Aczel (1978) and which has also the advantage of explaining non necessarily well-founded sets a la Finsler. One simply interprets a set as a pointed graph (where the arrow in the graph represents the membership relation). [...] I couldn't follow it, but I know your Logic manual doesn't mention either Miquel or Aczel, and I'm guessing that what Thierry is talking about here isn't central to HOL. Or are you just saying that you wish MESON proved more things more quickly? (In which case, why not use the prover9 interface, which I think HOL-Light provides. Maybe you'll get lucky!) That's a good idea, prover9, which I haven't figured out, but I think prover9 is more like Vampire than miz3. It would be great to use prover9 to further Josef's experiment, see how many of my geometry proof prover9 can prove in one line. It's miz3 than I want to be faster, and MESON does most of the work, I think, of miz3. If you would download my code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz run it, look at the proofs, I think you'll be surprised at how long the proofs take to run compared to how obvious the inferences I'm making are. I have 67 6-digit MESON "solved at" numbers. You might enjoy reading my proofs anyway! John & Michael seemed to say that I'm having equational reasoning problems, not to be fixed by improving MESON. A different question: why can't one code up declarative proofs like mine in HOL4? I think John thinks it isn't hard to do a bare-bones job, and perhaps even did that in his purple book. Miz3 is an accomplishment primarily, I think, because of the caching that Freek wrote (so the 2nd time the proof goes MUCH faster) and because you can mix declarative & procedural proof styles. Plus miz3 held up very well under my torture-testing. -- 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
