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

The logic of Nqthm is a quantifier-free first order logic with equality. The basic theory includes axioms defining the following:
  1. the Boolean constants t and f, corresponding to the true and false truth values.
  2. Equality. x = y is t or f according to whether x is equal to y.
  3. An if-then-else function. if x then y else z endif is z if x is f and y otherwise.
  4. The Boolean arithmetic operations x and y, x or y, not x, x implies y, and x iff y.
The logic of Nqthm contains two `extension' principles under which the user can introduce new concepts into the logic with the guarantee of consistency.
  1. 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:
    1. 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).
    2. 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.
    3. 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 pairs.
  2. 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 rules of inference of the logic are those of propositional logic and equality with the addition of mathematical induction.

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 proof attempts.

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.

  1. To admit a new function under the definitional principle we invoke:
    Definition: FN-NAME(x, y) = body
  2. 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.

Obtaining Nqthm

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.

Home

http://dirleton.csres.utexas.edu/software/nqthm/index.html

This page is URL http://www.computationallogic.com/software/nqthm/index.html