Thanks, Josef, that's very helpful, and you're saying I was wrong (but right originally)
I think the original intention behind the "weakness" was to capture the right level of reasoning that would be "obvious" to humans, i.e., not too strong to puzzle the readers and not too weak to drown them in detail. This motivation is probably still quite strong Michael taught me that aiming for obvious/not-tedious is bad design (see his post about "illusion" and "sweet spot"), and all the evidence is that John isn't trying to weaken miz3 in this way. Folks can still write readable proofs, making only "obvious" steps, even if the proof assistant is powerful enough to take much bigger inference leaps. I respectfully submit that John's code for "holby" is not a good description of what Mizar does, and my evidence is that my miz3 Tarski code http://www.math.northwestern.edu/~richter/TarskiAxiomGeometryCurry.ml makes heavy use of MESON, even using Freek's substitution of HOL Light currying for Mizar-friendly infixes. I think Mizar does a ton of things that John didn't code up, but that's OK because MESON does the job: "and finally if all else fails using MESON_TAC[]." You seem to understand this even, writing Both "MESON" and "by" are the respective workhorses in HOL Light and Mizar, but they do different things. Thanks for the links to Freek's article. Can you tell me again the links to the "obvious inference" papers by Davis and Rudnicki? There are really many proof search procedures (and ways how to limit them and combine them). I'd interpret this as saying that Mizar is doing much the same kind of FOL proving that MESON does, but that Mizar, unlike MESON, is shackled with various limitations aimed at hitting Michael's "sweet spot". -- 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
