 |
| Dr.
William McCune at Argonne Labs,
Illinois in his office with computer.
The "Proof of Robbins Conjecture"
problem is on the screen. Photo
credit: Lloyd DeGrane/The
New York Times |
In the early 1930s, Herbert Robbins
of Harvard University posed a question
that intrigued mathematicians: Is
a particular set of three equations
powerful enough to capture all the
laws of Boolean algebra? (Boolean
algebra is a mathematical model of
basic rules of logic and thought;
it obeys laws such as: "For any proposition
P, the negation of the negation of
P means the same thing as P"). Some
of the great mathematicians of the
century worked on the problem, but
the solution was not forthcoming until
1996, when Argonne National Laboratory
used powerful automated reasoning
software to conclude that yes, one
set of rules can capture all the laws
of Boolean algebra. Key to the 15-step
proof was a system called EQP (equational
prover) and a new strategy, both written
by William McCune. The problem was
so difficult that solving it required
more that eight days of computer time
on a number of Unix workstations.
Scientific Impact:
This work, cited as a major accomplishment
in artificial intelligence, demonstrated
that automated reasoning programs
can be used as powerful reasoning
assistants. Unlike previous attempts
to prove famous theorems using special-purpose
software, this work relied on a general-purpose
program, which produced a relatively
short proof that can be verified by
hand or by independent proof-checking
programs.
Social Impact: This
problem was solved using spare computer
time at smaller computers around the
world, suggesting that many other
complex problems can be addressed
without expensive supercomputers.
Furthermore, the mathematicians collaborated
without regard to institutional or
even international borders, and without
a research grant.
Reference: "Solution
of the Robbins Problem," W. McCune,
Journal
of Automated Reasoning (JAR)
19(3), 263-276 (1997)].
URL:
http://www-unix.mcs.anl.gov/~mccune/papers/robbins/
Technical Contact:
Daniel A Hitchcock, Mathematical,
Information, & Computational Sciences
Division, 301-903-6767
Press Contact: Jeff
Sherwood, DOE Office of Public Affairs,
202-586-5806
SC-Funding Office:
Office of Advanced Scientific Computing
Research |
