Mathesis Universalis - No.4, Autumn 1997 http://www.pip.com.pl/MathUniversalis/4/
When using any part of this text - by Witold Marciszewski - refer, please, to the above original URL.
Introductory Comment to Pages concerning
the Solution of Robbins Problem
Among the most important events in the area of automated reasoning there is the solving of the Robbins problem by automated reasoning software developed in the Mathematics and Computer Science Division of Argonne National Laboratory (US). 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 was solved in October 1996 by equational theorem prover EQP. The one who succeeded in that enterprise was Wiliam McCune (ANL). Here is his statement to account for the character of the project, made in the Introduction to his report.
"Although the solution was automatic in the sense that the user of the program did not know the solution, it was not a simple matter of giving the conjecture and pushing a button. The user made many computer runs, observed the output, adjusted the search parameters, and made more computer runs. The goal of this kind of iteration is to achieve a well-behaved search. Several of the searches were successful." -- W. McCune, "Well-Behaved Search and the Robbins Problem (extended abstract)" in: H.Comon (Ed.), Proceedings of RTA'97, Lecture Notes in Computer Science, Vol. 1232, Springer-Verlag, 1997, pp.1-7.There is quite a number of publications and WWW pages dealing with that solution and its history. A convenient introduction is found in the following texts:An extensive presentation of the solution is given in W.McCune's article "Solution of the Robbins Problem" forthcoming in Journal of Automated Reasoning, 1997.
- Robbins Algebras are Boolean (original site: http://www.mcs.anl.gov/home/mccune/ar/robbins). This page offers a historical background, a discussion of the solution, references, and related links.
- First draft of a press release on the solution of the Robbins problem This text includes McCunn's comment on a difference between the proof of the Robbins theorem and the famous earlier proof of the four-color theorem.
- ILF's Presentation of Otter's Proof of Winker's Condition Guided by a proof found by EQP, Otter produced a proof of Winker's second condition from the axioms of Robbins algebras. This completed the proof that all Robbins algebras are Boolean. The ILF system has tools to restructure and present proofs from several automated provers.
