Hi John, Bill, > | I really want to know how strong or weak you want miz3 to be. My > | belief (not based on a lot of info) is that Mizar is intentionally > | weak, partly to encourage very readable proofs and to make Mizar > | usable for student homework, but that you have no such interest in > | miz3 weakness. > > You are certainly right about Mizar's prover being intentionally weak. > I think efficiency of proof processing may have been a (or even the) > major factor behind this decision. With the batch processing model you > really want the individual steps to be quick.
The batch processing is not really a problem: there are easy directives/pragmas that switch off expensive repeated checking of previous proofs while you work on your next theorem. The major factor is the speed of re-factoring of a very large mathematical library. This is being done practically daily by people like Andrzej Trybulec, to make the library use concepts consistently, merge formalizations done by different authors into nicely re-usable pieces, throw out subsumed theorems when a stronger version is proved, etc. I believe Georges Gonthier also told me that he spends really a lot of time on refactoring his large Coq formalizations to make them re-usable for the next parts. If there are calls to many expensive search procedures left in the final proof code, extensive refactoring gets unpleasant. Refactoring MML (with over 1M calls to its own "MESON" - "by") would be a nightmare if each took 50s. I think the solution is not to avoid automation (as Gonthier seems to suggest), but to have good proof translation mechanism for the expensive proofs found in 50s by ATPs into bigger (but not too verbose) blocks of ITP code, e.g., multiple smaller MESON calls. And with the ATP power rising, and ATP/ITP bridges becoming common, this seems to be one of the more important work to be done. 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
