@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

Name: Nqthm

Keywords:  
  quantifier free, structured data, recursively defined functions, induction

Description: 
   Semantics:  quantifier free first-order theory of inductively defined
     data structures, intended model - a term model
   Deductive machinery: events -- shell definition, recursive function 
     definition, proving lemmas using heuristics for generating 
     induction schemata, rewriting, generalization, elimination of destructors,
     User can specify how proved lemmas are to be used by the heuristics.
     Hints can be given.  Proved meta-theorems can be installed as simplifiers.
   Dynamics:  theories are event histories
   Persistence: the current state can be saved in a library and restored.

Contact persons: 
boyer@cs.utexas.edu
moore@cs.utexas.edu

User group support: 
  mailing list: nqthm-users@cs.utexas.edu
  (send requests for addition or deletion to nqthm-users-request@cs.utexas.edu)

  mailing list maintainer:
    Robert S. Boyer
    Philosophy Department
    University of Texas
    Austin, TX 78712
    boyer@cs.utexas.edu

Pragmatics:
Strengths: 

That well over 16,000 theorems have been checked with Nqthm covering
different parts of mathematics, especially those related to computing,
demonstrates something about Nqthm.  Has any other theorem proving
system has been used to check a proof of quadratic reciprocity, which
Gauss called the crown jewel of number theory?  Has any other
automated reasoning system been used to prove not only the correctness
of a compiler that targets a typical von Neumann processor which has
been fabricated, but also to prove the correctness of the design of
that processor down to the level of gates and registers?  Many Nqthm
theorem proving efforts are very well-documented in papers, reports,
and theses.  The user's manual, A Computational Logic Handbook, gives
voluminous hints for successful use of the prover, and precisely
describes the logic and user commands.

Weaknesses:

1. Nqthm is built to work on conjectures about recursive functions
over the integers and other finitely generated structures, e.g.,
conses.  Nqthm does not support, especially well, attacks on theorems
in set theory or about such nonconstructive entities as the real
numbers.  (It is certainly possible to axiomatize set theory in Nqthm,
as one can in practically any first order prover.  However, the
theorem-proving strategies of Nqthm are not especially appropriate for
dealing with arbitrary user axioms.)

2. As with any contemporary automated reasoning tool, successful
checking of interesting theorems with Nqthm requires a considerable
amount of mathematical talent, experience, and persistence.  As with
most uses of most contemporary automated reasoning tools, Nqthm should
be regarded by the serious user as a proof checker rather than a proof
discoverer.  That is, the user had better have in mind a proof of any
theorem to be checked, and be prepared to guide Nqthm to checking that
proof by giving hints, such as formulating lemmas.  Otter is sometimes
used to find novel solutions to hard, open questions, but Nqthm has
not been used in this way, and one might doubt that it could ever be
used successfully in this way.

3.  Is it a strength or a weakness that Nqthm does not support typed
syntax?

Documentation: 

@book{boyer-moore-acl,
author = {Boyer, Robert S. and Moore, J. Strother},
title = {A Computational Logic},
year = 1979,
publisher = {Academic Press},
ISBN = {0-12-122952-1},
comment = {description of logic, heuristics, and many examples}
}

@book{boyer-moore-aclh,
author = {Boyer, Robert S. and Moore, J. Strother},
title = {A Computational Logic Handbook},
year = 1988,
publisher = {Academic Press},
ISBN = {0-12-122950-5},
order-info = {This book may be ordered by calling Academic Press at 
(800)321-5068 FAX 1-800-874-6418 or by writing to
to the Academic Press Books, Customer Service Department, Orlando, FL 32887}
comment = {comprehensive user's manual}
}

R. S. Boyer, M. Kaufmann, and J S. Moore, The Boyer-Moore Theorem Prover and
Its Interactive Enhancement, {\em Computers and Mathematics with Applications,}
Vol. 29, No. 2, pp. 27-62, 1995.

The ./doc/ directory in the Nqthm distribution, which includes several
revised chapters for "A Computational Logic Handbook", including the
two most essential chapters, which describe the logic and all the user
commands.  A second edition of this handbook is scheduled to appear in
late 1997 or early 1998.

Applications: 

By far, the most significant application of Nqthm has been to a prove
the correctness of a computing system known as the CLI Stack, which
includes (a) a microprocessor design (FM8502) based on gates and
registers, (b) an assembler (Piton) that targets FM8502, and (c) a
higher level language (micro Gypsy) that targets Piton.  We have also
seen a proof of correctness of a small operating system kernel (KIT).
FM8502, Piton, micro Gypsy, and Kit are documented in [62, 62a].

Another major application of Nqthm is the Ph.D.  work of N. Shankar in
proof checking Goedel's incompleteness theorem [69a].  The text of this
proof effort is included in the standard distribution of Nqthm, along
with Shankar's checking of the Church-Rosser theorem.

In the first chapter of "A Computational Logic Handbook", many other
applications of Nqthm are enumerated, including those in list processing,
elementary number theory, metamathematics, set theory, and concurrent
algorithms.

Recently Bill Young and Bill Bevier at Computational Logic, Inc., 
have used Nqthm to develop a machine checked proof of correctness of the 
``Oral Messages'' Algorithm of Pease, Shostak, and Lamport for solving the 
problem of achieving interactive consistency.  Such algorithms are important 
in ensuring fault tolerance by redundant processing.

J. S. Moore, et. al.  "Special Issue on System Verification".  Journal of
Automated Reasoning 5, 4 (1989), 409-530.

Books:

 W. Hunt.  FM8501: A Verified Microprocessor.  LNCS 795. Spring-Verlag.  1994.

 N. Shankar.  Metamathematics, Machines, and Goedel's Proof, Cambridge
 University Press, 1994.

 J S. Moore. A Mechanically Verified Assembly-Level Language. Kluwer, 1996.

Resource requirements:

The system runs well in at least these Common Lisps: Gnu Common Lisp (GCL),
Allegro (Franz), Lucid, and Macintosh.  There are no operating system or
dialect conditionals, so the code may well run in other implementations of
Common Lisp.  Executable images for some of this Lisps are available.

Bibliography:  (lists about 100 publications about Nqthm's design
                and about use of Nqthm)

  ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html

Where-to-get-it:

To get a copy of Nqthm, read

   ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html

Extensions/enhancements: Pc-Nqthm

[info date  July 97]  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%