On Sat, Jul 21, 2012 at 4:31 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> 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.
>
[...]
> 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.
>
Isn't MESON (without limits) complete? I think the only question is how
long you would be willing to wait for each proof, and possibly how much
memory you have.
------------------------------------------------------------------------------
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
