The Boyer-Moore theorem prover and its interactive enhancement

The so-called Boyer-Moore Theorem Prover (otherwise known as Nqthm) has been used to perform a variety of verification tasks for two decades. We give an overview of both this system and an interactive enhancement of it, Pc-Nqthm, from a number of perspectives. First, we introduce the logic in which theorems are proved. Then, we briefly describe the two mechanized theorem proving systems. Next, we present a simple but illustrative example in some detail in order to give an impression of how these systems may be used successfully. Finally, we give extremely short descriptions of a large number of applications of these systems, in order to give an idea of the breadth of their uses. This paper is intended as an informal introduction to systems that have been described in detail and similarly summarized in many other books and papers; no new results are reported here. Our intention here is to present Nqthm to a new audience.