Breadth-first search: Some surprising results

Although breadth-first search procedures cannot explore truly large search spaces, actual implementations of such procedures can result in surprisingly powerful problem-solvers that outperform more sophisticated heuristic search procedures. We describe two breadth-first search procedures. The first one, S&R, proves theorems from Principia of Whitehead and Russell, and is compared to two versions of the Logic Theorist. Previous estimates of the size of the search space are significantly reduced. When theorems are proved in an optimal order, this order differs markedly from that found in Principia, while more general theorems than those of Principia are often found.The second system, S&M, adapts breadth-first search to locally infinite search spaces in systems of rewriting rules. S&M is compared extensively to the heuristic theorem-prover of Quinlan and Hunt, and to some other theorem provers.