On 21/07/2012, at 14:49, Bill Richter <[email protected]> wrote:
> The miz3 proof is almost as quick, with a MESON `solved at' number of 23088. > The clear moral of your example is that if one uses no-tactics miz3 to solve > logic puzzle like this, then miz3 (using MESON) can astound us, proving > things we can't easily prove by ourselves. The reason those numbers are so similar is that the underlying technology is basically the same. > Now it's dimly possible that one would actually want to have a proof like > that in Hilbert axiomatic geometry code,So Michael's `sweet spot' seems to be > about what you want to use no-tactics miz3 for. Why am I hitting the sweet > spot with my geometry code? And Michael, do they play baseball in Australia? > Australia's favourite bat-and-ball game is cricket... > In fact, let's try the above one right now: > > let SupplementsCongAnglesCong_THM = thm `; > let alpha beta alpha' beta' be point_set; > assume alpha Suppl alpha' /\ beta Suppl beta' [H1]; > assume alpha === beta [H2]; > thus alpha' === beta' > > proof > > qed by -`;; > > miz3 instantly calculated my #1 inference error, with MESON getting only up > to 49. What if you quote H1, H2 and all of the theorems that you ultimately quoted in the final proof as arguments to "by"? Does miz3 "by" then get it in one step? That's the true test. Michael ------------------------------------------------------------------------------ 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
