On 21/07/2012, at 13:31, Bill Richter <[email protected]> wrote:
> Michael, this is scary: > > If you don't impose any limits to stop its search "prematurely" > then the first order prover is capable of proving any theorem that > has a proof. Of course, you do also have to prime said prover with > the relevant axioms. > > You seem to be saying that if we remove all the artificially imposed limits > from miz3 then we could prove any one of my 103 theorem with a 1-line proof > like this: > > let AnyOneOfThem_THM = thm `; > assertion > proof > qed by all the axioms and definitions is a list with commas`;; > Is that what you're saying? I would be very surprised if this was true. > This 1-line proof would be an example of what I meant by "little work." > Perhaps the way no-tactics miz3 would become so powerful was that we had "no > limit on [Cris's] depth of chaining". This is absolutely true. As Ramana said, model elimination is "complete", as are the methods used by the other first order provers, like Vampire. We know first order logic to be semi-decidable, so that we know that we can recursively enumerate all of the system's theorems. MESON implements an r.e. method for doing just that. And "by" uses MESON. I'm not suggesting that this is pragmatically reasonable. In particular, your computer may well run out of memory before it gets to the proof of your theorem. > Michael, I think miz3's "by" only uses MESON for simple purposes, so it > wouldn't matter that much if we were using MESON at full strength. Chris's > MESON example about MESON's astounding power doesn't refute my rather vague > claim, because Los's example isn't about a miz3 "by" justification involving > Hilbert's geometry axioms. Cris may be on to something, though... "by" invokes MESON in just the same way that you'd invoke it for using its "full power". There's no such thing as "simple purposes". When you say x by th1, th2, ... You set MESON up to prove the goal th1 /\ th2 /\ th3 ... ==> x, which it attempts using "full" MESON (i.e, full first order search). [Claim modulo time-outs and depth-limits etc.] > There's no way I'll believe that Mizar would prove the Robbins conjecture > without the user writing a very long proof. I'm skeptical that no-tactics > miz3 could do replicate the Waldmeister/Prover9 feat if we stopped imposing > limits to stop miz3's search "prematurely," to paraphrase Michael. Maybe not, but then MESON is not a state of the art first order prover with all of those other systems' smart heuristics. We also don't know how long the users had to wait to have the system actually prove the conjecture. 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
