Thanks to everyone for responding, especially Michael, as this is a point that I need to straighten out for my paper which I'm pretty close to submitting. 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. I have 2841 lines of miz3 no-tactics Hilbert axiomatic geometry code. 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". miz3's "by" is just an invocation of MESON but with, as I understand, a time limit imposed. As computers get faster, your "by" steps will become ever more capable and ever "closer" to the full power of MESON. 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... Josef, can you confirm that what you ran Vampire on my Tarski miz3 (or Mizar) code, your program was quite small, much smaller than my 1000 lines? You basically just stated my Tarski theorems and then Vampire proved them (all but a few such as Gupta's theorem)? Since you're a Mizar expert, can you compare this to Mizar or miz3: In some parts of math, systems like Waldmeister and Prover9 already produce fairly astounding results, like the proof of the Robbins conjecture (http://en.wikipedia.org/wiki/Robbins_algebra). 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. -- 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
