A Theorem Prover for a Computational Logic

We briefly review a mechanical theorem-prover for a logic of recursive functions over finitely generated objects including the integers, ordered pairs, and symbols. The prover, known both as NQTHM and as the Boyer-Moore prover, contains a mechanized principle of induction and implementations of linear resolution, rewriting, and arithmetic decision procedures. We describe some applications of the prover, including a proof of the correct implementation of a higher level language on a microprocessor defined at the gate level. We also describe the ongoing project of recoding the entire prover as an applicative function within its own logic.

• Type: Conference
• Year: 1990
• Where: CADE
• Authors: Robert S. Boyer, J. Strother Moore
• Keywords: Arithmetic Decision Procedures, Boyer-Moore Prover, CADE 1990, Entire Prover, Logical Reasoning