From: James Wetterau (jwjr@ignition.name.net)
Date: Sat Jul 22 2000 - 20:00:17 MDT
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
This archive was generated by hypermail 2.1.5 : Fri Nov 01 2002 - 15:30:07 MST