Product Code Database
Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.
The system was built on top of Lisp and had some very basic knowledge in what was called "Ground-zero", the state of the machine after bootstrapping it onto a Common Lisp implementation.
This is an example of the proof of a simple arithmetic theorem. The function is part of the (called a "satellite") and is defined to be
(DEFN TIMES (X Y)
(IF (ZEROP X)
0
(PLUS Y (TIMES (SUB1 X) Y))))
(prove-lemma commutativity-of-times (rewrite)
(equal (times x z) (times z x)))
The proof itself is given in a quasi-natural language manner. The authors randomly choose typical mathematical phrases for embedding the steps in the mathematical proof, which does actually make the proofs quite readable. There are macros for LaTeX that can transform the Lisp structure into more or less readable mathematical language.
The proof of the commutativity of times continues:
Give the conjecture the name *1.
We will appeal to induction. Two inductions are suggested by terms in the conjecture,
both of which are flawed. We limit our consideration to the two suggested by the
largest number of nonprimitive recursive functions in the conjecture. Since both of
these are equally likely, we will choose arbitrarily. We will induct according to
the following scheme:
(AND (IMPLIES (ZEROP X) (p X Z))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))
(p X Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme
produces the following two new conjectures:
Case 2. (IMPLIES (ZEROP X)
(EQUAL (TIMES X Z) (TIMES Z X))).
and after winding itself through a number of induction proofs, finally concludes that
Case 1. (IMPLIES (AND (NOT (ZEROP Z))
(EQUAL 0 (TIMES (SUB1 Z) 0)))
(EQUAL 0 (TIMES Z 0))).
This simplifies, expanding the definitions of ZEROP, TIMES, PLUS, and EQUAL, to:
T.
That finishes the proof of *1.1, which also finishes the proof of *1.
Q.E.D.
[ 0.0 1.2 0.5 ]
COMMUTATIVITY-OF-TIMES
|
|
