Hi Bill, >Thus, I conclude that the purpose of the default timeout >isn't to weaken miz3, but to better instruct beginners
Ah no, the main point was that if an inference is _not_ correct, often MESON will run for the full timeout time. So checking proofs with errors (= all proofs when you're not finished yet) gets very slow, and without timeout close to infinite. The timeout thing is just to deal with that. I think the original Automath from the seventies had exactly the same feature. Typechecking in type theory _is_ decidable, but if things are type incorrect, in Automath it takes forever to establish this (because it will endlessly unfold all definitions: Automath didn't have opaqueness.) 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
