I think you've got my position quite reasonably. On the other hand, I'm not sure I see why you think that it conflicts with your “new position”. Like you, I wouldn't mind if the automatic tactic behind "by" was arbitrarily powerful. Nonetheless, the current implementation of miz3's "by" does seem to emulate the deliberate weaknesses of Mizar's reasoner.
Thanks, Michael, that's great. I know I changed my position, and largely because of your criticism, for which I'm grateful. Since you say we're not in conflict, let me go back and re-interpret your post on Wed, 18 The illusion hangs together because the engineering heuristics that Freek and John have put together mean that the steps that a human thinks should be obvious are ones that the system often accepts too. [...] If you hit the sweet spot, then the system lurking behind "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. I think now that you were criticizing the way I used to think of miz3. But I think we now agree that the reason why miz3 is useful is that it's powerful enough that we don't have to provide unnecessary detail, but we produce human readable proofs by not asking miz3 to prove too much. Maybe you can study the issue of miz3 deliberate weakness with me. Freek pointed out that miz3 calls HOL_BY which calls MESON. Let's go to the hol_light directory. I think that miz3/miz3.ml just says HOL_BY is the prover, and refers us to Examples/holby.ml, which begins with the comment (* A HOL "by" tactic, doing Mizar-like things, trying something that is *) (* sufficient for HOL's basic rules, trying a few other things like *) (* arithmetic, and finally if all else fails using MESON_TAC[]. *) That doesn't look like any deliberate weaknesses to me. There are 3 occurrences of MESON_TAC in holby.ml, and I can't understand any of them. I certainly don't see any shackles being put on MESON there. However, as Freek explained to me, MESON has itself a limit, as explained in the reference manual def of GEN_MESON_TAC: Normally MESON, MESON_TAC and ASM_MESON_TAC explore the search space by successively increasing a size limit from 0, increasing it by 1 per step and giving up when a depth of 50 is reached. The more general tactic GEN_MESON_TAC allows the user to specify the starting, finishing and stepping value, but is otherwise identical to ASM_MESON_TAC. In fact, that is defined as: # let ASM_MESON_TAC = GEN_MESON_TAC 0 50 1;; I get the impression that MESON, MESON_TAC and ASM_MESON_TAC are much the same thing. BTW I'm now close to 3000 lines in my miz3 Hilbert axiomatic geometry code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz and I just coded up a reasonable proof of the SSS triangle congruence result. -- 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
