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'm afraid I don't really see what you mean by the combination of "little work" and "no limit on depth of chaining".)
Michael On 21/07/2012, at 5:00, Bill Richter <[email protected]> wrote: > Thanks, Cris, I did not know about John's paper > http://www.cl.cam.ac.uk/~jrh13/papers/me.html. It looks very interesting, > but his interesting details aren't what what I want to talk about. I want > to know if my education ideas fall apart if e.g. we put no `limit on depth of > chaining.' Otherwise we're talking about Michael's heuristics, where you > fiddle with various parameters trying to `hit the sweet spot' where tedious > things are proven easily and astounding results don't get proven > automatically. I'm satisfied that experts like John & Freek have done a > great job with the heuristics. I'm not going to try to explain that to my > audience of mathematicians, even if I understood it myself. I'm looking for > some kind of upper bound on how astounding a result you can prove with > little work if we have no heuristics, e.g. no `limit on depth of chaining.' > > -- > 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 ------------------------------------------------------------------------------ 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
