RE: I'm making my move! A new AGI Project is born

From: Ben Goertzel (
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
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
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:
The TPTP problem set
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