Nqthm
Encyclopedia
Nqthm is a theorem prover
sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.
and J Strother Moore
, professors of computer science at the University of Texas, Austin
. They began work on the system in 1971 in Edinburgh
, Scotland
. Their goal was to make a fully automatic, logic-based theorem prover. They used a variant of Pure
LISP as the working logic.
, the system makes extensive use of rewriting
and an induction
heuristic that is used when rewriting and something that they called symbolic evaluation fails.
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 TIMES is part of the BOOT-STRAP (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)))
Should the theorem prove to be true, it will be added to the knowledge basis of the system and can be used as a rewrite rule for future proofs.
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
. This gave the proof tools that the system uses automatically to the user, so that more guidance can be given to the proof. This is a great help, as the system has an annoying tendency to wander down infinite chains of inductive proofs.
, Matt Kaufmann
, and J Strother Moore
received the ACM
Software System Award for their work on the Nqthm theorem prover.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.
History
The system was developed by Robert S. BoyerRobert S. Boyer
Robert Stephen Boyer, aka Bob Boyer, is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore...
and J Strother Moore
J Strother Moore
J Strother Moore is a computer scientist, and he is a co-developer of the Boyer–Moore string search algorithm and the Boyer–Moore automated theorem prover, Nqthm. An example of the workings of the Boyer–Moore string search algorithm is given...
, professors of computer science at the University of Texas, Austin
University of Texas at Austin
The University of Texas at Austin is a state research university located in Austin, Texas, USA, and is the flagship institution of the The University of Texas System. Founded in 1883, its campus is located approximately from the Texas State Capitol in Austin...
. They began work on the system in 1971 in Edinburgh
Edinburgh
Edinburgh is the capital city of Scotland, the second largest city in Scotland, and the eighth most populous in the United Kingdom. The City of Edinburgh Council governs one of Scotland's 32 local government council areas. The council area includes urban Edinburgh and a rural area...
, Scotland
Scotland
Scotland is a country that is part of the United Kingdom. Occupying the northern third of the island of Great Britain, it shares a border with England to the south and is bounded by the North Sea to the east, the Atlantic Ocean to the north and west, and the North Channel and Irish Sea to the...
. Their goal was to make a fully automatic, logic-based theorem prover. They used a variant of Pure
Purely functional
Purely functional is a term in computing used to describe algorithms, data structures or programming languages that exclude destructive modifications...
LISP as the working logic.
Definitions
Definitions are formed as totally recursive functionsRecursion (computer science)
Recursion in computer science is a method where the solution to a problem depends on solutions to smaller instances of the same problem. The approach can be applied to many types of problems, and is one of the central ideas of computer science....
, the system makes extensive use of rewriting
Rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
and an induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
heuristic that is used when rewriting and something that they called symbolic evaluation fails.
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 TIMES is part of the BOOT-STRAP (called a "satellite") and is defined to be
(DEFN TIMES (X Y)
(IF (ZEROP X)
0
(PLUS Y (TIMES (SUB1 X) Y))))
Theorem formulation
The formulation of the theorem is also given in a Lisp-like syntax:(prove-lemma commutativity-of-times (rewrite)
(equal (times x z) (times z x)))
Should the theorem prove to be true, it will be added to the knowledge basis of the system and can be used as a rewrite rule for future proofs.
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
LaTeX
LaTeX is a document markup language and document preparation system for the TeX typesetting program. Within the typesetting system, its name is styled as . The term LaTeX refers only to the language in which documents are written, not to the editor used to write those documents. In order to...
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
Proofs
Many proofs have been done or confirmed with the system, particularly- (1971) list concatenation
- (1973) insertion sort
- (1974) a binary adder
- (1976) an expression compiler for a stack machine
- (1978) uniqueness of prime factorizations
- (1983) invertibility of the RSA encryption algorithm
- (1984) unsolvability of the halting problem for Pure Lisp
- (1985) FM8501 microprocessor (Warren Hunt)
- (1986) Godel's incompleteness theorem (Shankar)
- (1988) CLI Stack (Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
- (1990) Gauss' law of quadratic reciprocity (David Russinoff)
- (1992) Byzantine Generals and Clock Synchronization (Bevier and Young)
- (1993) bi-phase mark asynchronous communications protocol
- (1993) Motorola MC68020 and Berkeley C String Library (Yuan Yu)
- (1994) Paris-Harrington Ramsey Theorem (Kenneth KunenKenneth KunenHerbert Kenneth Kunen is an emeritus professor of mathematics at the University of Wisconsin–Madison who works in set theory and its applications to various areas of mathematics, such as set-theoretic topology and measure theory...
) - (1996) The equivalence of NFSA and DFSA (Debora Weber-Wulff)
PC-Nqthm
A more powerful version, called PC-Nqthm (Proof-checker Nqthm) was developed by Matt KaufmannMatt Kaufmann
Matt Kaufmann is a Senior Research Scientist in the Department of Computer Sciences at the University of Texas at Austin, USA. He was a recipient of the 2005 ACM Software System Award along with Robert S. Boyer and J Strother Moore, for his work on the The Boyer-Moore Theorem Prover.- External...
. This gave the proof tools that the system uses automatically to the user, so that more guidance can be given to the proof. This is a great help, as the system has an annoying tendency to wander down infinite chains of inductive proofs.
Literature
- A Computational Logic Handbook, R.S. Boyer and J S. Moore, Academic Press (2nd Edition), 1997.
- The Boyer-Moore Theorem Prover and Its Interactive Enhancement, with M. Kaufmann and R. S. Boyer, Computers and Mathematics with Applications, 29(2), 1995, pp. 27–62.
Awards
In 2005 Robert S. BoyerRobert S. Boyer
Robert Stephen Boyer, aka Bob Boyer, is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore...
, Matt Kaufmann
Matt Kaufmann
Matt Kaufmann is a Senior Research Scientist in the Department of Computer Sciences at the University of Texas at Austin, USA. He was a recipient of the 2005 ACM Software System Award along with Robert S. Boyer and J Strother Moore, for his work on the The Boyer-Moore Theorem Prover.- External...
, and J Strother Moore
J Strother Moore
J Strother Moore is a computer scientist, and he is a co-developer of the Boyer–Moore string search algorithm and the Boyer–Moore automated theorem prover, Nqthm. An example of the workings of the Boyer–Moore string search algorithm is given...
received the ACM
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
Software System Award for their work on the Nqthm theorem prover.
External links
- The Automated Reasoning System, Nqthm
- The Boyer-Moore Theorem Prover (NQTHM)
- Even though the system is no longer being supported, it is still available at [ftp://ftp.cs.utexas.edu/pub/boyer/nqthm]