On 19/07/12 13:04, Bill Richter wrote: > Michael, thank you very much, and I did not know of John's paper > http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html > which I will read carefully. I didn't quite understand you:
> I couldn't figure out what your `illusion' was. I think miz3 is much > less powerful than HOL Light is generally. I'd like to say precisely > how miz3 is more powerful than straight FOL, which would be very > tedious I believe to write proofs in. But Tom Hales is formalizing > his Kepler conjecture proof in HOL Light and other powerful proof > assistants. Tom wouldn't consider only using miz3, right? How would you define "powerful"? Though it might be tedious (perhaps extremely so) to do some things, I don't think there's anything preventing Tom Hales from doing all of the Kepler conjecture in structured miz3 proofs. > Ultimately, I'm afraid there is no precise way of explaining what > Mizar/miz3 are capable of for your paper. You can only point to > experience, and say that the system behind "by" seems to allow > reasonable leaps of inference. > I'll take your word for it,an Freek seems to agree, but I'm not > satisfied. I know what I use miz3 for, and it's simple. Basically > "by" substitutes all the variables I have into all the results in my > "by" list and in a very simple-minded way puts together a proof of my > assertion. Plus "by" can do certain proofs by contradictions "by" is ultimately calling meson, a first-order proof procedure. Ignoring possible additional simplification that might happen first, meson is then looking for a first-order proof of your goal, using implication chaining and instantiation, and doing so to an arbitrary depth. In this sense, miz3 *isn't* any more powerful than "straight FOL". (Given which, what in your experience makes you say that it is?) Like all other first order systems (e.g., Vampire), all you can say is that it will prove some goals and won't prove others (and assuming soundness, it won't prove anything that isn't actually true). Indeed, if you were using Isabelle, you could link the equivalent of "by" directly to Vampire or some other modern first order prover and probably find that you could make rather larger jumps than previously. Contrariwise, there is some handling of higher-order features in meson, and all of those first-order steps are really happening in HOL, not FOL. That's why I said the "ground truth" really is HOL, not FOL. One guess I have is that what you find appealing about HOL is not so much the logical reasoning, but rather the fact that the types and terms give you an appealing expressiveness without requiring very tedious type annotations. That's a credit to simple type theory and not much to do with the proof-power of "by". Michael ------------------------------------------------------------------------------ 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
