From: Ben Goertzel (ben@goertzel.org)
Date: Mon Apr 05 2004 - 06:38:02 MDT
Marc wrote:
> 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
monetary value."
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
Intel's chips:
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