On Nov 2, 2007 8:52 PM, Matt Mahoney <[EMAIL PROTECTED]> wrote: > --- Benjamin Goertzel <[EMAIL PROTECTED]> wrote: > > Computer theorem-provers are way worse than any human mathematician, > > except at very special types of theorems. > > True, there has not been much progress since Gelernter used internal > graphical > models to heuristically trim the search space to prove theorems in plane > geometry in 1959 [1]. > > 1. Gelernter, H., Realization of a Geometry-Theorem Proving Machine, > Proceedings of an International Conference on Information Processing, > Paris: > UNESCO House, pp. 273-282, 1959.
There has been progress in "narrow-AI theorem proving", e.g. -- theorem-provers to prove correctness of circuits -- theorem-provers to prove existence/uniqueness theorems for various sorts of differential equations etc. etc. But not at general-purpose theorem-proving... -- Ben G ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=60658017-3ccb3d
