It's amusing that they talk about Boyer-Moore. They mean, I think, the string search algorithm, not the theorem prover. Their string search algorithm was just intended as something Boyer and Moore could use as a hard case for code proofs. Their real work was the original Boyer-Moore theorem prover, their constructive theory of mathematics, their book "A Computational Logic", and their later ACL prover.
(I used to know Boyer and Moore, and used their theorem prover. Recently I took the original sources from the final 1992 version, put them on Github, and got it working with the current GNU Common LISP.[1] So you can now run their prover from the 1980s several thousand times faster than in the VAX days. It's neat to see it prove the basic theorems of number theory in about a second.)