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. ============================== 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.