Nqthm

Nqthm

Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.[1]

Contents

History

The system was developed by Robert S. Boyer 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.

Definitions

Definitions are formed as totally recursive functions, 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))))

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 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 Kunen)
  • (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 Kaufmann. 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. Boyer, Matt Kaufmann, and J Strother Moore received the ACM Software System Award for their work on the Nqthm theorem prover.[2]

External links

References

  1. ^ "Nqthm, the Boyer-Moore prover". http://www.cs.utexas.edu/users/boyer/ftp/nqthm/. 
  2. ^ Association for Computing Machinery, [http://campus.acm.org/public/pressroom/press_releases/3_2006/software.cfm "ACM: Press Release, March 15, 2006"], campus.acm.org, accessed December 27, 2007. (English version).

Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • Robert S. Boyer — Robert Stephen Boyer, aka Bob Boyer, is a 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… …   Wikipedia

  • ACL2 — es, a la vez, un lenguaje de programación, una lógica matemática para especificar y demostrar formalmente propiedades de los programas escritos en dicho lenguaje, y un demostrador automático de teoremas que asiste al usuario en dicha tarea. ACL2… …   Wikipedia Español

  • Automated reasoning — is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically. Although automated… …   Wikipedia

  • ACL2 — ACL2, (A Computational Logic for Applicative Common Lisp), is a software system consisting of a programming language, an extensible theory in a first order logic, and a mechanical theorem prover. ACL2 is designed to support automated reasoning in …   Wikipedia

  • J Strother Moore — (his first name is the alphabetic character J ndash; not an abbreviated J. ) 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. A good example of the… …   Wikipedia

  • ACL2 — es un demostrador automatizado de teoremas con una lógica basada en un subconjunto aplicativo del lenguaje Common Lisp. También está escrito es ese mismo sublenguaje y puede correr en diversas implementaciones de Common Lisp. Tiene un alto grado… …   Enciclopedia Universal

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”