**From:** Ben Goertzel (*ben@goertzel.org*)

**Date:** Mon Apr 05 2004 - 06:38:02 MDT

**Next message:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Previous message:**Ben Goertzel: "Friendliness, Vagueness, self-modifying AGI, etc."**In reply to:**Marc Geddes: "RE: I'm making my move! A new AGI Project is born"**Next in thread:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

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

**Next message:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Previous message:**Ben Goertzel: "Friendliness, Vagueness, self-modifying AGI, etc."**In reply to:**Marc Geddes: "RE: I'm making my move! A new AGI Project is born"**Next in thread:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

*
This archive was generated by hypermail 2.1.5
: Wed Jul 17 2013 - 04:00:46 MDT
*