Developed by Robert Boyer and Strother Moore, the Boyer-Moore theorem prover is an automatic and logic-based system. It is a heuristic theorem prover that is used to prove properties of pure Lisp programs in a logic that is quantifier-free. It also exploits the duality between proofs by induction and definitions by recursion. Boyer and Moore used a variant of LISP as their working logic. Therefore, it only deals with total functions and is based on the first-order logic with equality minus quantifiers.

The Boyer-Moore theorem prover is used as the last option as it is able to prove whether the other theorems applied earlier are correct or not. It also simplifies the problems of substitution and equivalence. The Boyer-Moore prover performs induction only when the other steps fail because it does not support quantifiers. Thus, the theorem’s statements and the proofs formulation would be unfamiliar. It does not generate large proofs but is led to them by the definitions and lemmas supplied by the user. Thus, it is more properly regarded as a proof checker.