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? BTW I habitually use the term miz3 to refer to the Mizar-like part of miz3, but the real power of miz3 is that it combines Mizar-like proofs with the more powerful procedural HOL Light proofs. I think you said that it would be very difficult to precisely explain what miz3 is doing, as by various complicated strategies, it appears in good cases that in miz3, "by" doesn't prove so much that the user doesn't learn anything, but isn't so stupid that the human has to provide unnecessary detail. Well, that's what I want, and I've been quite satisfied with miz3's "by" performance. What's bothered me is not knowing how to define things, but that's more HOL Light, and you and John helped me a lot. 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 -- 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
