First draft of a press release on the Solution of the Robbins problem.

The Robbins problem, which has puzzled mathematicians and
logicians for more than 60 years, has been solved by automated
reasoning software developed in the Mathematics and Computer
Science Division of Argonne National Laboratory.  The problem
was posed by Herbert Robbins at Harvard University in the
1930s, and some of the great mathematicians of the century
have worked on it.

The problem is in an area called Boolean algebra, which is a
mathematical model of some of the basic rules of logic and
thought.  Boolean algebra obeys laws such as "for any
proposition P, the negation of the negation of P means the
same thing as P", and "for any two propositions P, Q, the
conjunction of P and Q is false if and only if one or both of
them is false".

The Robbins problem was to determine whether one particular
set of rules is powerful enough to capture all of the laws of
Boolean algebra.  One way to state the Robbins problem in
mathematical terms is: Can the equation not(not(P))=P be
derived from the following three equations?

    [1] P or Q = Q or P,
    [2] (P or Q) or R = P or (Q or R),
    [3] not(not(P or Q) or not(P or not(Q))) = P.

Progress on the problem was made at Argonne in the early
1980s, when Larry Wos suggested to his student Steve
Winker that he attack the problem by going backwards; that is,
by finding conditions that, if true, would solve the problem.
One such condition, the existence of terms C and D such that
not(C or D) = not(C), was found by Winker to be sufficient by
a combination of automated reasoning methods and
pencil-and-paper reasoning [S. Winker, "Absorption and
idempotency criteria for a problem in near-Boolean algebras",
Journal of Algebra 153(2), 414--423 (1992)].

Interest in the problem was renewed recently with Argonne's
development of new automated reasoning techniques.  The
automated theorem-proving program EQP, designed by William
McCune, was given the basic problem and asked to prove,
several times, with different search strategies, that Winker's
condition holds.  One of the attempts, after 8 days of
searching on a UNIX workstation, succeeded with a 15-step
proof of the theorem.

On the nature of the solution, McCune said, "The proof of the
Robbins theorem is quite different from the proof of the
four-color theorem, which is probably the most famous computer
proof.  To prove the four-color theorem, mathematicians
devised an outline of a proof, wrote special-purpose software,
and gave the computer a large number of cases to verify; an
explicit proof was not constructed, so correctness of the proof
depends on correctness of the software.  For the Robbins
problem, a general-purpose automated reasoning system was given
a statement of the conjecture along with a few a search
parameters, and the program produced a relatively short proof
which can be verified by hand or by independent proof-checking
programs."

For more information on the Robbins problem, its solution
(including the computer proof), and automated reasoning at
Argonne, see http://www.mcs.anl.gov/home/mccune/ar/robbins/.