**Next message:**Michael S. Lorrey: "Re: GAMES: Historical truths [was Re: The games are all crap...]"**Previous message:**hal@finney.org: "Re: GAMES: Historical truths [was Re: The games are all crap...]"**In reply to:**GBurch1@aol.com: "COMP: AI and mathematics: Proofs"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

GBurch1@aol.com says:

*> In a discussion in another forum, the question of whether computers have
*

*> "found" valid mathematical proofs has come up. Being mathematically stunted,
*

*> I thought I'd do a hand-off of the question to this forum, since someone able
*

*> to comment intelligently on the question probably inhabits this forum. Any
*

*> leads or help?
*

I read in the NY Times a few years ago about about a very interesting

line of research manifested in "EQP", a program whose moniker meant

"Equational theorem prover". I find that EQP is not the top of the

line of its family; that's a program called "Otter". You may read

about both here:

http://www-unix.mcs.anl.gov/AR/eqp/

Evidently, you can get EQP's source code and compile it yourself at:

ftp://info.mcs.anl.gov/pub/Otter/eqp-09d.tar.gz

This program used logical symbol manipulation rules, and was supposed

to try to get from an originating set of symbols and other similar

groups of symbols from its library of theorems to an unproven result.

It not only proved an unproven conjecture, but it had the ability to

analyze the intermediate lines in its proof for length and seek out

alternate proofs that might employ shorter intermediate lines of

symbols, more likely to appear to be obvious applications of rules to

human beings. Then, having proved a theorem, it could alter the depth

of its lookahead search for transition lines that it believed,

according to some scoring algorithm, could lead to a conclusive proof

or disproof of the desired end result, so it could find more elegant

proofs employing fewer steps.

Finally, I believe the research group working on EQP was supposed to

improve it by allowing it to analyze strategies from successfully

proven theorems so that it could continually upgrade its scoring

algorithm.

EQP and Otter evidently eminate form Argonne National Labs.

Regards,

James Wetterau

**Next message:**Michael S. Lorrey: "Re: GAMES: Historical truths [was Re: The games are all crap...]"**Previous message:**hal@finney.org: "Re: GAMES: Historical truths [was Re: The games are all crap...]"**In reply to:**GBurch1@aol.com: "COMP: AI and mathematics: Proofs"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b29
: Mon Oct 02 2000 - 17:35:07 MDT
*