by H. Zhang
Two decades ago, Boyer and Moore built one of the first automated theorem provers that was capable of proofs by mathematical induction. Today, the Boyer-Moore theorem prover remains the most succes…