An industrial strength theorem prover for a logic based on Common Lisp

Matt Kaufmann, J. Strother Moore
[doi] [Google Scholar] [DBLP] [Citeseer]

IEEE Transactions on Software Engineering 23(4)
Pages 203-213
April 1997
Note(s): ACL2 theorem prover