THE BOYER-MOORE THEOREM PROVER AND ITS INTERACTIVE ENHANCEMENT

The so-called Boyer-Moore Theorem Prover (otherwise known as Nqthm) ha s been used to perform a variety of verification tasks for two decades . We give an overview of both this system and an interactive enhanceme nt 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 extremel y short descriptions of a large number of applications of these system s, in order to give an idea of the breadth of their uses. This paper i s intended as an informal introduction to systems that have been descr ibed in detail and similarly summarized in many other books and papers ; no new results are reported here. Our intention here is to present N qthm to a new audience.