Freek, thanks for spotting my arithmetic error, and that was clever of you to figure out where the smaller MESON number for the miz3 proof came from. I'd like your opinion on some of the cool stuff I learned from Michael, Ramana, Cris and Rob:
1) Miz3 is definitely more powerful than Mizar, and miz3 can even be used as a 1-line proof theorem-prover, although it does not seem to be very efficient. 2) Given a statement x by th1, th2, ...; miz3 tries to construct (using MESON among other things) an FOL proof of the implication th1 /\ th2 /\ th3 ... ==> x Nothing limits the power of miz3 to prove such statements other than "heuristics", not only of MESON but because of timeouts and e.g. depth limitations imposed. 3) This to-me unexpected power of miz3 shouldn't affect any plans to use miz3 in education, e.g. my plans to use miz3 in high school Geometry courses. It's like converse of Jesus's slogan ``Ask and you shall receive.'' Miz3 won't do what you don't ask it to do! If the theorem is an implication, and you ask miz3 to prove the statement qed by antecedents`;; it may do so, and we've seen interesting example here recently. If the user only uses miz3, as I do, to justify statements that appear obvious to them, then I think miz3 is fine. The more-or-less unlimited MESON power should allow miz3 to, in a reasonable time, to prove what looks obvious to us. There's no precise mathematical meaning of obvious. If someone codes up a miz3 proof that works, and we don't understand their proof, we can ask them for more details, just like we'd ask a human for more details. The only difference is that now we can ask the human miz3-user to code up the extra details, and we can see that miz3 justified these as well. I found it very illuminating that when I coded up in miz3 Rob's proof of the logic puzzle, the MESON "solved at" number was far lower than 23088: 0..0..1..3..6..solved at 13 There's a question that nobody seemed to know the answer to, but I hope you do. Does miz3 do anything else to limit its power other than with the variable timeout, which you explained to me how to change long ago? Does miz3 impose any e.g. any depth limitations on MESON? -- Best, Bill ------------------------------------------------------------------------------ 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
