The best way to get a sense of the state of the art in automated theorem proving would be to download and play with the systems
http://en.wikipedia.org/wiki/Isabelle_(theorem_prover) and http://en.wikipedia.org/wiki/Prover9 , which are state-of-the-art automated theorem provers. Isabelle is fairly close to how theorem-proving would be done in PLN, if one suppressed uncertainty and used only crisp truth values, and didn't try anything funky with experience-based inference control. Prover9 is different as it uses some special normal forms to represent theorems (Skolemizing out all existential quantifiers, for instance). I don't know these systems well, but I played with HOL and Otter, which were the predecessors to these two systems. Looking at the publications by the folks involved with these projects will give you a sense for the state of the art. -- Ben G On Thu, Oct 16, 2008 at 11:50 PM, Abram Demski <[EMAIL PROTECTED]>wrote: > "Your intuition is dead wrong based on the last decades of work in > automated theorem proving!!" > > Ben, > > Thanks... though I do find that rather strange... can you cite any > particular references? > > The reason I find it surprising, is that it suggests the existence of > actual shortcuts, rather than only heuristics that work in the domains > we're interested in but which become useless on random problems. If > these shortcuts exist, I wonder, could they be enumerated by some > brute-force method? > > --Abram > > On Thu, Oct 16, 2008 at 11:26 PM, Ben Goertzel <[EMAIL PROTECTED]> wrote: > > > > > > On Thu, Oct 16, 2008 at 11:21 PM, Abram Demski <[EMAIL PROTECTED]> > > wrote: > >> > >> On Thu, Oct 16, 2008 at 10:32 PM, Dr. Matthias Heger <[EMAIL PROTECTED]> > >> wrote: > >> > In theorem proving computers are weak too compared to performance of > >> > good > >> > mathematicians. > >> > >> I think Ben asserted this as well (maybe during an OpenCog tutorial?). > >> Is this proven? My intuition is that a computer could easily beat a > >> mathematician on randomly generated problems from theorem space, but > >> could not generate mathematically interesting theorems the way a > >> mathematician could. In other words, I would expect the hard AGI > >> problem to be "figure out what other mathematicians will be excited > >> about", not "prove theorems". > > > > Your intuition is dead wrong based on the last decades of work in > automated > > theorem proving!! > > > > Combinatorial explosion is the problem. The lack of effective inference > > control, as we discussed in last night's OpenCog chat/tutorial session. > > > > All the most interesting achievements of automated theorem proving have > been > > **semi-automated**, with humans helping the AI to prune the > > backward-chaining inference tree at the difficult places. > > > >> > >> So, I don't see how one would proceed in making math-based AGI... it > >> seems like an effective natural language interface would be needed > >> after all, to allow the AGI to read mathematical papers, and to write > >> its own. Otherwise, it would just be creating theorems of interest to > >> itself, and it would be impossible to judge these as "interesting" or > >> "uninteresting" in an objective way. > > > > The way to proceed would be to feed the AGI on proofs from Mizar.org ... > > > > But, this is certainly very hard if the AGI doesn't have any way to > accept > > tutoring > > > > Still, I imagine that via a combination of Lojban and Mizar, one could > teach > > an AGI theorem-proving, without needing to mess with the horrible syntax > or > > excessive semantic ambiguity of natural languages... > > > > -- Ben > > > > ________________________________ > > agi | Archives | Modify Your Subscription > > > ------------------------------------------- > agi > Archives: https://www.listbox.com/member/archive/303/=now > RSS Feed: https://www.listbox.com/member/archive/rss/303/ > Modify Your Subscription: > https://www.listbox.com/member/?&; > Powered by Listbox: http://www.listbox.com > -- Ben Goertzel, PhD CEO, Novamente LLC and Biomind LLC Director of Research, SIAI [EMAIL PROTECTED] "Nothing will ever be attempted if all possible objections must be first overcome " - Dr Samuel Johnson ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
