From: Ben Goertzel (email@example.com)
Date: Mon Apr 05 2004 - 06:38:02 MDT
> I must say, I like the way you've been 'playing it'
> for your own projects. Far smarter than 'Sing Inst'
> in my opinion. I think the business-oriented model is
> the way to go. For any AGI Project to get on-going
> funding, I think what is needed is an emphasis on a
> series of more modest, shorter-term applications -
> which have clearly defined results and some potential
> monetary value. That's why I'm looking the 'theorem
> prover' angle.
I think that theorem-proving, as an application, excels in terms of
"clearly-defined results" but not so much in terms of "potential
However, I do know of one commercial application of theorem-proving. My
former colleague Deepak Kapur used his (fairly simplistic) automated
theorem proving software to formally prove the correctness of some of
His website it
An example paper title from his site is:
--- Theorem Proving Support for Hardware Verification Deepak Kapur Invited Talk, Third Intl. Workshop on First-Order Theorem Proving, FTP 2000 St. Andrews, Scotland, July 2000. --- Needless to say, that sorta thing is a lot easier than proving the Riemann hypothesis! In general, "proving program correctness" is of interest to a lot of people in the software industry, especially in the military where reliability is considered critical. For instance, some people use the Z specification language to formalize software designs: one then has a problem of efficiently proving a complex software design, formalized in Z, is correct. There are also variants like Object-Z (or something like that .. I haven't studied this stuff for a while). Among well-known theorem provers, I like Otter http://www-unix.mcs.anl.gov/AR/otter/ because it uses combinatory logic, which is related to the knowledge representation inside Novamente. However, the results obtained with Otter or any other theorem-provers to date are far, far short of prove-the-Riemann-hypothesis level! A review of Otter and some other contemporary systems is here: http://www-users.cs.umn.edu/~dliang/CSci8980/Projects/TheoremProvers.htm The TPTP problem set http://www.cs.jcu.edu.au/~tptp/ is a standard collection of theorem-proving problems for automated theorem-provers.... Before you think about the Riemann hypothesis you should definitely be able to handle this stuff with ease... > I'll see what I can do before the end of the year to > raise some interst in N.Z and Australia. At the very > least there will be a new Institute with a team of one > working away part-time ;) Sounds like fun ;-) -- Ben G
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:46 MDT