Hi Bill, On Mon, Aug 27, 2012 at 7:19 AM, Bill Richter <[email protected]> wrote: > 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"),
I am not sure I can read that e-mail as suggesting that Mizar/miz3 is "bad design". But certainly, there are many opinions out there in the ITP world. > 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. Yes. But will they? I think that for example most of the SW/HW verification people don't care much about this, they often want to have the job done ASAP. So people like Andrzej and Georges (who have to maintain their large math libraries) choose to limit the power of their proof *checking* procedures. I believe both of them have been reasonably successful in large-scale math formalization. Also note that I disagree with both of them when it comes to the use of strong (often external) proof *finding* procedures. > I respectfully submit that John's code for "holby" is not a good description > of what Mizar does, It is not a full description, but the best which is publicly available. The code in it will give you an idea 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 Yes, John uses MESON as a fallback, but the MESON code has little to do with Mizar proof checking. > > 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? http://rd.springer.com/article/10.1007/BF00247436 http://www.springerlink.com/content/j42q143754533x73/ > > 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, No. They do different things. > but that Mizar, unlike MESON, is shackled with various limitations aimed at > hitting Michael's "sweet spot". Yes, Mizar is certainly shackled in the way Michael described. Josef ------------------------------------------------------------------------------ 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
