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.
Michael On 26/07/2012, at 16:50, Bill Richter <rich...@math.northwestern.edu> wrote: > Freek, I realized that my new position is that think I I don't agree with > Michael, who I believe was saying that miz3 only behaves in a Mizar-like > fashion because limitations you & John imposed on miz3 and the weakness of > MESON. If I misquoted Michael, I apologize. My new position is that miz3 is > Mizar-like enough for me no matter how powerful miz3 and MESON are. Even if > miz3 could quickly prove all my theorems if I asked it too, I can still write > up what I call readable proofs, and miz3 will only try to justify my proofs. > Miz3 won't on its own steam go prove the theorem. ------------------------------------------------------------------------------ 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
