On Fri, 21 Jul 2000, Max More wrote:
> Greg, if I understand your question, the answer is "yes". Computers have
> not only found valid mathematical proofs, they have found *new*
> proofs--one's never before thought up by humans. (I use this as a counter
> to the argument that machines cannot and never will do anything creative.)
> The one that I remember offhand was at the Argonne National Laboratory.
It is a very big field, coming under the heading of "Theorem proving"
or "Automated reasoning". Lenat gave a great example at the Contact
conference this year where Cyc had been ask to analyze some situations
that the DoD/CIA invented (something like -- if Iran sinks a bunch of
freighters in the straight of Hormouz (sp?), is there enough oil
produced in the world to satisfy demand for 3 months if all other
nations pumped at their maximum capacity?). Cyc couldn't answer
some the DoD/CIA analysts could, could answer some as well as they
could and even answered a couple that they couldn't!
Related to the mathematical proof situation, Max is correct.
A lot of work has been done over the last 30 years in these
areas at Argonne especially. A good place to start is:
http://www-unix.mcs.anl.gov/AR/new_results/
A major player in the past was Rusty Lusk, but the leaders now
appears to be William McCune and Larry Wos.
Interestingly enough, Lusk moved on to help develop MPI
(message passing interface) which was one of the areas I
had to brush up on when reviewing computational strategies
for MBrains...
Enjoy,
Robert
This archive was generated by hypermail 2b29 : Mon Oct 02 2000 - 17:35:04 MDT