Be sure to read the license agreement in basis-pc.lisp.

This file contains notes on updates to `pc-nqthm' (proof-checker
nqthm), an interactive enhancement to the Boyer-Moore theorem prover
`nqthm' that supports full first-order quantification.  The system may
be obtained by ftp on the host cli.com in the directory
~ftp/pub/proof-checker/.  You can see which release you have by
evaluating the variable *pc-nqthm-version-number* in Lisp, e.g.

>*pc-nqthm-version-number*
"1.2"
>

If you have any questions or comments, please send them to Matt
Kaufmann, email address kaufmann@cli.com, postal address below:

Matt Kaufmann
Computational Logic Inc.
1717 W. Sixth St., Suite 290
Austin, TX  78703
phone:  (512) 322-9951

If there are any patches, they can be found in a file "patch.lisp",
with instructions on how to load them.  (There currently are none, and
I hope there won't need to be any!)

Everything before Release 1.2 is documented either in CLI Technical
Report 19 (the original user's manual for the system available from
cli.com), CLI Technical Report 42 (describing the addition of free
variables and a number of quite minor changes to the version described
in Technical Report 19), or CLI Technical Report 43 (describing the
addition of first-order quantification).  The Boyer-Moore theorem
prover itself is described (from a user's point of view) in the book
``A Computational Logic Handbook'' by Boyer and Moore (Academic Press,
1988).  The functional variables extension to that system is described
as follows in the file fs.lisp in directory ~ftp/pub/nqthm/ on
cli.com:

;  The code in this file, fs.lisp, implements two new NQTHM events:
;  CONSTRAIN and FUNCTIONALLY-INSTANTIATE.  These events are
;  documented in the paper "Functional Instantiation in First Order
;  Logic" by Robert S.  Boyer, David M. Goldschlag, Matt Kaufmann, and
;  J Strother Moore, Report 44, Computational Logic, Inc., 1717 W. 6th
;  Street, Suite 290, Austin, TX 78703.  A copy of this report may be
;  found on the NQTHM directory under the file names fs.mss and fs.ps.

Note:  This note is now rather obsolete, since this work has been
incorporated into Nqthm-1992.  Also, the reference here to "fs.ps"
should be replaced by a reference to:

``Functional Instantiation in First Order Logic,'' R.S. Boyer, D.
Goldschlag, M. Kaufmann, J S. Moore", in:  ``Artificial Intelligence
and Mathematical Theory of Computation: Papers in Honor of John
McCarthy,'' Academic Press, pp. 7-26, 1991.  (Versions also published
as CLI Technical Report 44 and in proceedings of the 1989 Workshop on
Programming Logic, Programming Methodology Group, University of
Goteborg, West Germany.

============================== Release 1.2 ==============================

1. Hash tables are now used to implement the DISABLEDP macro, which
can cause a significant improvement in performance when there are lots
of disabled functions and/or rewrite rules around.  This improvement
was written with Matt Wilding.

2. If the BASH command creates (new) subgoals that contain free
variables of the given proof state, then those variables are no longer
considered free in the new state.  This change was made out of a
concern for soundness that may or may not be warranted, and I'd be a
little surprised if it affects anyone.  Also, BASH reports more
vigorously when it proves a goal completely.

3. The ``fast rewriter'' (which is called by the S and X commands) has
been improved so that it is allowed to rewrite preserving only
propositional equivalence when it is rewriting the arguments of a call
of a basic boolean function (AND, OR, IMPLIES, NOT, or IFF).  (This
was already the case when rewriting the first argument of an IF term.)
Thanks go to David Goldschlag for pointing out the need for something
like this.  Here's an example he created that works in the new version
but not in the old.

(DEFN N (OLD NEW STATEMENT)
  (APPLY$ (CAR STATEMENT)
	  (APPEND (LIST OLD NEW)
		  (CDR STATEMENT))))

(DCL RING (INDEX N))

(PROVE-LEMMA TEST NIL
             (IMPLIES (AND (MEMBER STATEMENT
                                   (RING (SUB1 INDEX) N))
                           (N OLD NEW STATEMENT))
                      (AND (MEMBER STATEMENT
                                   (RING (SUB1 INDEX) N))
                           (N OLD NEW STATEMENT)
                           T))
             ((INSTRUCTIONS PROMOTE S)))

4. RETRIEVE and SAVE are implemented using an alist now.  They used to
be implemented using global variables, which was dangerous since one
could write to a system variable.

5. VERIFY and VERIFY-DEFN now take an additional optional argument:
an initial instructions list to run.  Note that all the instructions
will be run even if there is a failure, so if some kind of protection
is wanted, wrap them in a DO-STRICT form or some such thing.  All
instructions, even macro commands, are legal here.  Here is an
example, where the instructions set up the induction and prove the
base case.

(verify (equal (times x y) (times y x))
	((induct (times x y)) 
	 prove))

6. Based on a suggestion of David Goldschlag, the = command now allows
ID and IFF atoms as third arguments, saying to definitely
not-use/try-to-use IFF in place of EQUAL for the new subgoal.  For
details, see (HELP-LONG IFF).

7. Bill Bevier's LEMMA and AXIOM macros have been added, as has
Boyer's ADD-SHELL patch for shells whose constructor takes zero
arguments.

8. The DEFN-SK implementation of first-order quantification has been
added.  The handy macro DEFN-SK+ is included:  if you replace DEFN-SK
by DEFN-SK+ and you get each of the two new rewrite rules attached to
a single event name.

============================== Release 1.3 ==============================

1. New macro command REDUCE is like BASH except that it calls the
entire prover except induction, unlike BASH, which only calls the
simplifier.  For both commands, the result of the command is to create
new subgoals to replace the given goal in the case that the proof
isn't complete.  Also, with REDUCE you get the normal prover IO.

Actually, BASH has a new optional atomic argument that indicates
whether one wants to use the full prover.  So, (REDUCE ...) is the
same as (BASH T ...).  The help facility explains all this carefully.

2. The macro command FORWARD has received a very minor fix having
to do with (previously unanticipated) true goals.

3. A bug has been fixed in the processing of instructions in an
INSTRUCTIONS hint to PROVE-LEMMA.  It had been the case, for example,
that (CHANGE-GOAL) was parsed differently than CHANGE-GOAL so that it
was in fact treated about the same as (CHANGE-GOAL NIL).

4. The test suite examples.events now checks whether the functional
variables code is loaded in before trying to run the
Schroeder-Bernstein events.  Thus, it should work whether or not
fs.lisp has been loaded as part of nqthm.

============================== Release 1.4 ==============================

Was there a ``Release 1.4,'' really?

============================= Release "1992" ============================

*** THIS VERSION OF PC-NQTHM WORKS WITH NQTHM-1992 ONLY. ***  It is
NOT compatible with the previous release of Nqthm (from 1987).  The
primary changes in Pc-Nqthm have been made so that it is compatible
with Nqthm-1992.

NOTE:  This directory contains a potentially useful subdirectory
"misc/" that contains many enhancements compatible with Nqthm-1992
(not just Pc-Nqthm-1992).  THESE FILES ARE TO BE CONSIDERED AS COVERED
BY THE PC-NQTHM LICENSE -- IN PARTICULAR, THERE IS NO WARRANTY -- BUT
THEY ARE NOT PART OF THE PC-NQTHM SYSTEM PER SE.  See the README file
in the misc/ subdirectory for more information on what is available
there, including demos, emacs utilities, a trace package, .....

One user-visible change is an extension of the functionality of
DEFN-SK.  It is now the case that the user can specify the ordering of
formal parameters to skolem functions.  Also, COND and CASE may now be
used to build formulas.  See the file defn-sk.doc in the text
subdirectory for details.

Speaking of DEFN-SK:  the file defn-sk.lisp may now be loaded directly
on top of Nqthm-1992, even without loading Pc-Nqthm-1992 first.

Except for this enhancement to DEFN-SK, the changes are mainly
implementation-level changes that shouldn't affect the user's view of
the system.  There may be a few very minor user-level changes not
mentioned here, for example, the macro command SK* handles IFF a
little better than it did, and syntax errors involving quantifiers
produce slightly more informative error messages.

I hope (expect) that this is the last Pc-Nqthm release ever....
