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