Theorem provers based on connection calculi use a goal-oriented proof search, but in practice this simplicity is marred by a need for extensive backtracking.

This paper presents a strategy for restricting backtracking in such theorem provers. Furthermore, the paper shows how this strategy, along with some other basic techniques, can be implemented in Prolog. This program is the core of version 2 of the leanCoP theorem prover. For the purposes of restricting backtracking, the paper distinguishes between essential and nonessential backtracking. Essential backtracking for a particular literal occurs before the literal is solved; subsequent backtracking for the literal is then nonessential.

The resulting theorem prover is incomplete, but it seems to be quite effective in practice. The paper compares other lean theorem provers with the version of leanCoP that includes restricted backtracking, along with some other well-known techniques, such as the use of lemmata and of regularity. These comparisons provide evidence that restricted backtracking is a successful technique. Furthermore, the compactness of the core Prolog prover makes experimentation with other ideas straightforward--one such idea considered by the author is randomized search.

The presence of this explicit implementation, along with the actual code, makes the paper quite readable. The implementation, which runs under Eclipse, Sicstus, and SWI Prolog, serves to illuminate the early exposition of the system, making the paper significantly easier to understand.