The Robbins problem was solved in October 1996 [7] by the equational theorem prover EQP [61. Although the solution was automatic in the .sense that the user of the program did not know a 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. The purpose of this presentation is to convey some of the methods that have led to well-behaved searches in our experiments and to speculate on automating the achievement of weII-behaved search. First, I give some background on the Robbins problem and its solution.
展开▼
