@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: Pc-Nqthm
Keywords: Nqthm, proof-checker, first-order quantification, interactive
Description:
Pc-Nqthm (Proof-Checker Nqthm) is a Common Lisp implementation of an
enhancement to the Boyer-Moore theorem-prover that provides
further interactive capabilities and first-order quantification.
Semantics: Boyer-Moore logic extended by first-order quantification
Deductive machinery: includes Nqthm mechanisms, but also allows
goal directed proof development with commands ranging from low-level
commands like applying a rewrite rule to full-blown calls to the
Nqthm prover. There is also a facility for ``macro commands,''
which are similar to the ``tactics'' and ``tacticals'' offered by
several other systems.
Dynamics: Essentially the same as Nqthm, except that an interactive
loop for goal-directed proof is provided as well.
Persistence: essentially the same as Nqthm.
Contact persons: kaufmann@aus.edsr.eds.com
User group support: nqthm-users@cli.com. Matt Kaufmann is happy to
answer questions: kaufmann@aus.edsr.eds.com.
Pragmatics: The system has all the power of Nqthm, but also allows finer-
grained user control of proofs. There is a potential for abuse: if
the user takes too much advantage of the lower-level capabilities, the
proofs are uglier than necessary. Put another way, if proofs are done
by proving appropriate lemmas first as rewrite rules, then often those
rewrite rules can be used automatically to assist with later proofs --
but this desirable state of affairs is lost if there is excessive
manual intervention in proofs. Instead, many users prefer to use the
interactive capability in order to better understand what lemmas or
modifications would be useful in completing a proof, and finally create
proofs that can be submitted in regular Nqthm.
Documentation:
In addition to on-line help, a carefully written user's manual is
available as Computational Logic Inc. Technical Report 19, with an
update as CLI Technical Report 42. These are available in
postscript form by anonymous ftp from
ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/.
Applications: This system has been used to check theorems stating the
correctness of a transitive closure program, a Towers of Hanoi
program, a ground resolution prover, a compiler, irrationality of the
square root of 2, an algorithm of Gries for finding the largest "true
square" submatrix of a boolean matrix [40], the exponent two version of
Ramsey's Theorem [41, 46], the Shroeder-Bernstein theorem [46],
Koenig's tree lemma, a finite version of the collapsing function of Cohen
forcing, and others. It has also been used to check the correctness of
several Unity programs and has been used for hardware verification.
40. Matt Kaufmann. A Mechanically-checked Semi-interactive
Proof of Correctness of Gries's Algorithm for Finding the
Largest Size of a Square True Submatrix. Internal Note 236,
Institute for Computing Science, University of Texas at Austin,
October, 1986.
41. Matt Kaufmann. An Example in NQTHM: Ramsey's Theorem.
Internal Note 100, Computational Logic, Inc., November, 1988.
46. Matt Kaufmann. DEFN-SK: An Extension of the Boyer-Moore
Theorem Prover to Handle First-Order Quantifiers. Tech. Rept.
43, Computational Logic, Inc., 1717 W. 6th St, Suite 290,
Austin, Texas, June, 1989.
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.
Extensions/enhancements: You might consider the ACL2 theorem prover, which
has many features not included in Nqthm and contains an interactive capability
similar to Pc-Nqthm. See
ACL2 home page
Resource requirements:
Nqthm installed and running; minimum of 8 megabytes of main memory
is recommended. It is important that your Common Lisp [in which the Nqthm
is running] supports redefinition of functions. For example, KCL
(as opposed to AKCL) is not acceptable for building pc-Nqthm.
Where-to-get-it
To get a copy follow these instructions:
1. get the
compressed tar file , uncompress, untar.
2. read the file README-pc and follow the directions it gives.
Copyright (C) 1994 by Matt Kaufmann and Computational Logic, Inc.
no fee, no support
Copying and use of Pc-Nqthm-1992 is authorized to those who have read and
agreed with the terms in the "Pc-Nqthm-1992 GENERAL PUBLIC SOFTWARE LICENSE,"
which may be found at the beginning of the Pc-Nqthm-1992 file "basis-pc.lisp"
and also in the files "pc-nqthm-public-software-license.doc" and
"pc-nqthm-public-software-license.ps".
[info source/date] email annoucement sep91,
additions by Matt Kaufmann 4/92, updated 7/95, 8/97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%