Hi Bill, >Can you jump into the discussion Michael and I were having >about whether miz3 is intentionally weakened? Michael seems >to think yes, I think no, but I wonder what effect the MESON >depth limit of 50 has, or the fact that MESON is just FOL >and not HOL.
Ah no, there were no deep thoughts behind the choice of "by" in miz3. I just chose the most trivial option available (well, also I wanted it to be at least as strong as the real Mizar "by"... which it isn't, because you lack the properties and requirements.) As I wrote before, I think the thing actually is "bad", because often you can justify a proof step with a REWRITE_TAC that only does a very small number of rewrites, but not with the default "by". That feels very strange. Implementing a better "by" for miz3 is a nice project to think about, but it's not on the top of the stack of things I'm currently considering doing. Freek ------------------------------------------------------------------------------ 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
