Boyer-Moore theorem prover

NQTHM

A theorem prover that has been under development since 1972. NQTHM is designed to be used mainly with the fixed set of axioms provided by its developers, R.S. Boyer and J.S. Moore, typically augmented by a number of definitions provided by the NQTHM user. The underlying logic (which is essentially PRA) and the conjectures entertained by NQTHM are quantifier free, or, more precisely, implicitly universally quantified. The NQTHM logic contains standard first-order principles and additional axioms that describe certain data structures, including the integers, ordered pairs, lists, and symbols. The logic also contains a principle of definition for recursive functions over these data structures. By using recursive functions, one can express many of the things that one usually expresses with quantifiers when dealing with finite objects (cf. also Recursive function). The Boyer–Moore prover, which implements this logic, also contains implementations of linear resolution, rewriting, and arithmetic decision procedures.

The main motivation for the development of the Boyer–Moore prover has been the wish for a system that can be used in a practical way to check the correctness of computer systems. By far the most significant application of NQTHM has been to a prove the correctness of a computing system known as the CLI Stack, which includes:

a) microprocessor-design based on gates and registers;

b) an assembler that targets the microprocessor; and

c) a higher-level language (micro Gypsy) that targets the assembler [a4]. Another major application of NQTHM is the work of N. Shankar in proof checking the Gödel incompleteness theorem [a6]. The text of this proof effort is included in the standard distribution of NQTHM, along with Shankar's checking of the Church–Rosser theorem.

In [a3], Chap. 1, many other applications of NQTHM are enumerated, including those in list processing, elementary number theory, meta-mathematics, set theory, and concurrent algorithms. Recently (1998), NQTHM has been used to develop a machine-checked proof of correctness of the Pease–Shostak–Lamport "oral messages" algorithm for solving the problem of achieving interactive consistency.

One of the main strengths of NQTHM is that it has been used to prove thousands of theorems, covering different parts of mathematics, and that it provides many heuristics, guessing strategies for searching through the space of possible proofs for conjectures; perhaps the most important of these is the induction heuristic. An important weakness of NQTHM is that it is built to work on conjectures about recursive functions over the integers and other finitely generated structures only; it does not support, especially well, attacks on theorems in set theory or about non-constructive entities such as the real numbers. Another weakness of NQTHM is that, like most other contemporary automated reasoning tools, successful checking of interesting theorems with NQTHM requires a considerable amount of mathematical talent, experience, and persistence. NQTHM should be regarded by the serious user as a proof checker rather than a proof discoverer. That is, the user should have in mind a proof of any theorem to be checked, and be prepared to guide NQTHM to checking that proof by giving hints, such as formulating lemmas.

The main sources of information on NQTHM are [a2], [a3], [a1]. The system runs well in at least these Common Lisps: Gnu Common Lisp (GCL), Allegro (Franz), Lucid, and Macintosh. There are no operating system or dialect conditionals, so the code may well run in other implementations of Common Lisp. A copy of NQTHM can be obtained via ftp, see [a7]. Recently, a successor of NQTHM, called ACL2, has been developed. ACL2 is an "industrial strength" version of the Boyer–Moore NQTHM, supporting as a logic (and programmed in) a large applicative subset of Common Lisp. Unlike NQTHM, ACL2 supports the rational numbers, complex rationals, character objects, character strings, and symbol packages. An overview of the ACL2 system is given in [a5].

References[edit]