- 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 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 pairs.

*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 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.

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

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