The Automated Reasoning System, Nqthm
We briefly review the automated reasoning system Nqthm, also known as
`the Boyer-Moore Theorem Prover'. Nqthm is a Common Lisp program for
proving mathematical theorems. Since A Computational Logic
was published in 1979, Nqthm has been used by several dozen
users to check proofs of over 16,000 theorems from many areas of
number theory, proof theory, and computer science.
Nqthm-Users Mailing List
The logic of Nqthm is a quantifier-free first order logic with
equality. The basic theory includes axioms defining the following:
The logic of Nqthm contains two `extension' principles under which
the user can introduce new concepts into the logic with the guarantee
- the Boolean constants t and f, corresponding to the true
and false truth values.
- Equality. x = y is t or f
according to whether x is equal to y.
- An if-then-else function. if x then
y else z endif is z if
x is f and y otherwise.
- The Boolean arithmetic operations x and y, x
or y, not x, x implies
y, and x iff y.
The rules of inference of the logic are those of propositional logic
and equality with the addition of mathematical induction.
- The Shell Principle allows the user to add axioms
introducing `new' inductively defined `abstract data types.'
Natural numbers, ordered pairs, and symbols are axiomatized
in the logic by adding shells:
- Natural Numbers. The nonnegative integers are built from
the constant 0 by successive applications of the
constructor function ADD1. The function NUMBERP
recognizes natural numbers. The function SUB1 returns
the predecessor of a non-0 natural number.
x in N abbreviates numberp(x).
- Symbols. The data type of symbols, e.g., 'RUNNING, is
built using the primitive constructor PACK and 0-terminated
lists of ASCII codes. The symbol 'NIL, also abbreviated
NIL, is used to represent the empty list.
- Ordered Pairs. Given two arbitrary objects, the function
CONS builds an ordered pair of these two objects. The function
LISTP recognizes ordered pairs. The functions CAR and
CDR return the first and second component of such an ordered
pair. Lists of arbitrary length are constructed with nested
- The Definitional Principle allows the user to define new
functions in the logic. For recursive functions, there must be an
ordinal measure of the arguments that can be proved to decrease in
each recursion, which, intuitively, guarantees that one and only one
function satisfies the definition. Many functions are added as part
of the basic theory by this definitional principle. For example, we
define for the natural numbers these familiar expressions: i
+ j, i - j, i < j,
i * j, i / j, i
mod j, and i^j. ZEROP(i)
returns f if and only if i is a positive integer.
EVENP(x) returns f if and only if
x is an odd positive integer.
The Theorem Prover
Nqthm is a mechanization of the preceding logic. It takes as input a
term in the logic, and repeatedly transforms it in an effort to reduce
it to non-f. Many heuristics and decision procedures are
implemented as part of the transformation mechanism.
The theorem prover is fully automatic in the sense that once a proof
attempt has started, the system accepts no advice or directives from
the user. The only way the user can interfere with the system is to
abort the proof attempt. However, on the other hand, the theorem
prover is interactive: the system may gain more proving power through
its data base of lemmas, which have already been formulated by the user
and proved by the system. Each conjecture, once proved, is converted
into some `rules' which influence the prover's action in subsequent
The commands to the theorem prover include those for defining new
functions, proving lemmas, and adding shells, etc. The following
two commands are the most often used.
- To admit a new function under the definitional principle we invoke:
Definition: FN-NAME(x, y) = body
- To initiate a proof attempt for the conjecture statement,
naming it LEMMA-NAME, we invoke:
Theorem: LEMMA-NAME statement
Typically, the checking of difficult theorems by Nqthm requires
extensive user interaction. The behavior of the prover is influenced
profoundly by the user's actions. The user first formalizes the
problem to be solved in the logic. The formalization may involve many
concepts and so the specification may be very complicated. The user
then leads the theorem prover to a proof of the goal theorem by
proving lemmas that, once proved, control the search for additional
proofs. Typically, the user first discovers a hand proof, identifies
the key steps in the proof, formulates them as a sequence of lemmas,
and gets each checked by the prover.
Above text from:
R. S. Boyer and Yuan Yu,
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor,
in D. Kapur, editor, (Automated Deduction -- CADE-11), Lecture Notes in Computer
Science 607, Springer-Verlag, 1992, pp. 416-430.
This page is URL http://www.computationallogic.com/software/nqthm/index.html