Nqthm

Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.[1]

  1. ^ "Nqthm, the Boyer-Moore prover".