What's New in TPS and ETPS

Release notes for distribution copy of June 24th 2004:

• Automatic Search
  • New search procedures MS03-7 and MS04-2 which search for proofs of theorems in extensional type theory using extensional expansion dags.
  • Added support for searching with set constraints to MS98-1, MS03-7 and MS04-2.
  • Setting PRIMSUB-METHOD to PR00 will cause TPS to use unification to determine a set substitution and make nonleaf connections (up to negation normal form).
• Extensional Proofs
  • New top level EXT-SEQ for manipulating extensional sequent calculus derivations.
  • New top level EXT-MATE for manipulating extensional expansion dags.
• Inference Rules for Natural Deduction
  • LIST-RULES*: Show important inference rules with intermediate rule definitions.
  • ADD-HYPS, DELETE-HYPS : Add/Delete hypotheses for a line.
  • TYPESUBST : Substitute for type variables in a line.
  • MAKE-ASSERT-A-HYP: Changes a line which is justified by 'Assert' to a hypothesis which can be discharged.
  • NNF, NNF-EXPAND: Converts a line to or from negation normal form.
  • ELIMINATE-CONJ*-RULEP-APPS, ELIMINATE-ALL-RULEP-APPS, ELIMINATE-RULEP-LINE: Replaces applications of RuleP (and certain other proposition rules) in favor of basic propositional rules.
  • ITRUTH: Rule to justify the formula TRUTH (without using RuleP).
• Libraries and Modes
  • Library directories can be modified by CREATE-LIB-DIR, CREATE-LIB-SUBDIR, DELETE-LIB-DIR, RENAME-LIBDIR, COPY-LIBDIR, UPDATE-LIB-DIR, IMPORT-NEEDED-OBJECTS and CHECK-NEEDED-OBJECTS
  • Users can create library classification schemes to organize the library and store these schemes in the library.
  • UNIXLIB : A new library top level with a unix-style interface using a library classification scheme.
  • GOODMODES : Support for saving a list of theorems with modes which prove them.
  • When the user sets a mode, all important flags are now set to their default values unless explicitly set by the mode.
• Proof Translations
  • There is a new version of NAT-ETREE for translating from a normal natural deduction proof to an expansion proof.
  • CUTFREE-TO-EDAG : EXT-SEQ command which translates from a cut-free extensional sequent derivation to a extensional expansion proof.
  • ETREE-NAT : EXT-MATE command which translates from an extensional expansion proof to a natural deduction proof.
• Misc.
  • There is a new Java interface for TPS and ETPS.
  • Support for using TPS under Microsoft Windows.
  • Support for using TPS as an external service (e.g., by Omega).
  • Support for using TPS as a web server to allow online use.
  • New top level MODELS for experimenting with standard models with finitely many individuals.
  • The flags ALLOW-NONLEAF-CONNS and DISSOLVE can be used to allow connections between nodes which are not atoms (e.g. connections between disjunctions).
  • Properties have been added to flags noting which flags are relevant or irrelevant given other flag settings. If the user sets a flag that is irrelevant, TPS issues a warning. The review command UPDATE-RELEVANT allows the user to set a flag and then all relevant flags.
  • SAVE-ETREE, RESTORE-ETREE: Saves and restores expansion trees.
  • Implemented dissolution which modifies a jform to remove connections listed in the value of DISSOLVE.
  • Support for including lemmas in expansion proofs (in particular, extensionality lemmas and set existence lemmas).
  • DEASSERT-LEMMAS, NORMALIZE-PROOF : Combine a proof with proofs of lemmas used and attempt to normalize the natural deduction proof.

Release notes for distribution copy of June 16th 1998:

• SKOLEM-DEFAULT NIL (meaning "use selection nodes instead of Skolemizing") now works.
• TPS-TEST can now modify the modes it uses in a uniform way, using the flag TEST-MODIFY.
• MS91-INTERLEAVE allows the search procedure to make primitive substitutions a few at a time, instead of doing them all at once.
• New flag PRINTTYPES-ALL implemented.
• PBRIEF summarises a natural deduction proof by omitting some of the unimportant details.
• REWRITE-EQUIVS changes the way in which equivalence is rewritten by the mating procedure.
• New search procedure MS98.
• Merging has been made faster by making the minimization of the mating an optional feature, rather than always attempting to do it.
• New commands PTREE, PTREE* and PTREE-FILE print the etree in a tree format.
• Library objects now contain keywords such as HIGHER-ORDER and WITH-EQUALITY, which allow for faster searching and categorization within the library.
• ADD-SUBDIRECTORIES has been completely rewritten, and now works with Lucid CL as well as Allegro CL and CMU CL.
• Added SUPPRESS-FLAGS, which allows the user to suppress all mention of a user-definable list of uninteresting flags.
• Various small improvements to manuals, help messages, etc.
• Various minor bug fixes.

Release notes for distribution copy of October 30th 1997:

• Dual instantiation of definitions and equalities has been implemented (see forthcoming paper).
• New methods for primitive substitution (discussed in the same paper) have also been implemented.
• New command TPS-TEST allows for a test run through a batch of proofs without requiring interaction from the user.
• Major changes to the library facilities: both the default and backup directories may now be lists of directories. Multiple definitions of the same object are allowed, and the user is asked which definition to use when such objects are loaded. SHOW-TIMING can now show the proof times for all instances of a given object.
• Library objects are now stored with a PROVABILITY property, allowing for fast searches to find provable (or unprovable) theorems.
• TPS now supports rewrite rules (for interactive proofs only). These may be bidirectional and/or polymorphic, and may invoke arbitrary functions to test for applicability of the rule and to clean up afterwards (e.g. applying lambda-normalization after each application).
• Rewrite rules can be bundled into THEORIES for ease of use. Many theories can be stored in memory, to be activated or deactivated as needed.
• Unification is now timed separately, so the user can see how much of the search time was spent on unification.
• The command UNIFORM-SEARCH has been improved.
• It is now possible to find out, during a proof search but without interrupting it, the time that TPS has spent searching for a proof.
• The new command FINDPROOF searches through saved proof files for a proof of a given theorem.
• The flags SHORT-HELP and ALPHA-LOWER-FLAG reformat the output from HELP, ? and ?? in a more readable manner.
• Command completion of an ambiguous command now offers a list of possible completions instead of just failing.
• The command OOPS allows the user to make minor changes in the previous command without retyping it.
• ND Proofs containing assertions of reflexivity or transitivity of equality can now be rewritten automatically into a form that can be translated by NAT-ETREE.
• The command AUTO-SUGGEST takes a ND proof and makes (not necessarily completely correct) suggestions about how to set the flags for an automatic proof.
• Help messages are now available for flag settings as well as for flags.
• The command PAUSE allows greater user control over execution of work files.
• TeX output can now be formatted for LaTeX.
• TPS can now be run on a problem from the command line in "batch mode", with the output being sent to a file.
• The VPT command can now produce TeX output with the literal names in boxes.
• SKOLEM-DEFAULT SK3 and SKOLEM-DEFAULT NIL (corresponding, respectively, to skolemizing over just the free variables and to using selection nodes instead of skolemization) now work properly.

Release notes for distribution copy of June 18th 1996:

• Interactive Proofs
  • Proofs, and lines within proofs, can now have comments attached to them.
  • Commands SAVE-SUBPROOF, CREATE-SUBPROOF, MERGE-PROOFS and TRANSFER-LINES allow easy manipulation of partial proofs (e.g. pasting the proof of a lemma into a larger proof).
  • Command FIND-LINE looks for lines of a given form within a proof.
  • New command DIY-L for automatic proof of lemmas within an interactive proof.
  • New interactive proof commands ECONJ*, ICONJ*, UGEN*, CASES3, CASES4, ASSOC-LEFT, RULEC1, SUBST-EQUIV, IDISJ-LEFT, IDISJ-RIGHT.
  • New implementation of NAT-ETREE, allowing easier conversion of natural deduction proofs to eproofs.
• Unification
  • Implementation of variable depth bounds in unification via MAX-SUBSTS-VAR and its associated flags, bringing the time for THM15B (in the JAR paper) down from 2.5 hours to 1 minute.
  • Improved unification output via flags UNIF-COUNTER and UNIF-TRIGGER.
  • UN90 now allows breadth-first unification as well as depth-first.
  • Improvements to the unification routines; new flag DNEG-IMITATION, plus implementation of a subsumption-checker, bringing the time for THM15B (in the JAR paper) down from 2.5 hours to 5 minutes.
  • New unification command UTREE* prints the unification tree in a tree format.
  • New unification command PP* prints detailed information about unification problems (are they linear, monadic, second order, etc...?).
• Automatic Proof Search
  • Implementation of variable time bounds for searches with primitive substitutions.
  • New (optional) method for generating primitive substitutions, by counting the number of literals as well as the number of quantifiers. Governed by the flag PRIMSUB-METHOD.
• Other Stuff
  • SCRIBEPROOF and TEXPROOF now allow more user control over the output format.
  • The SEARCH command now allows searches of all objects in the library.
  • SAVEPROOF now saves all related abbreviations as well.
  • New editor command PRIM-SUBST simulates the mate command PRIM-SINGLE in the editor.

Release notes for distribution copy of April 26th 1995:

• The new commands BUG-SAVE and BUG-RESTORE provide a uniform way to store information about bugs in TPS. New commands BUG-LIST, BUG-HELP show all the stored information about bugs.
• The new matingstree top level has been implemented.
• New editor commands to delete left or right scope of a binary connective.
• New editor commands to embed the current wff under a connective or binder.
• Pop-up windows can now use a different font from the main window.
• Literals which are copies of each other can now be labelled as such: e.g., copies of LEAF7 will be labelled LEAF7.1, LEAF7.2, etc.
• It is now possible to print the proof structure as a tree rather than a list.
• Mating searches can now be interrupted cleanly, and it is possible to continue searching after such an interrupt.
• Searches in the test top level now behave in a similar way to the mate top level; this makes test more intuitive to use.
• There is a new setting for ORDER-COMPONENTS which orders the conjunctions in a vpform from largest to smallest.
• It is now possible to save unification problems created during mating search in the library, and to restore them later.

Release notes for distribution copy of November 11th 1994:

• Natural deduction proofs now have the variables relabelled to make them more readable (in particular, the same variable will not be used twice with different types, and superscripts are eliminated where possible).
• All known bugs in proof search have been fixed.
• There is a new command ^PN, which prints active lines in full and abbreviates other lines to just the line number.
• There is a new flag ETREE-NAT-VERBOSE which controls the output of ETREE-NAT and can redirect it to the proofwindows.
• SCRIPT files can now be produced in Scribe or TeX format.
• Library files can now be sorted, with the SORT command.
• The KEY command can now be used on the library, to find all library objects containing a given string.
• Beta and eta conversion can now be done either separately or together or (in the case of eta conversion) not at all. This applies to both interactive and automatic proofs.
• MS90-3 now handles truth values properly.
• EQUIV-EQ now generates more useful default values.
• The hypotheses for a new lemma no longer have to be the same as those of the conclusion (they can now be a subset).
• The manuals have been heavily rewritten and updated.
• A new flag TURNSTILE-INDENT-AUTO allows the user to improve the formatting of printed proofs.
• There are new commands to reindex the library and purge it of backup files, and damaged library files can be salvaged automatically.
• If TPS is given a mode name or a gwff name which it does not recognise, it will now automatically ask whether to search the library for an object of that name.
• MOVE* now works properly.
• The backtracking strategy for MS90-* has been made more efficient.
• MS90-* now always prefers to duplicate the innermost quantifier of a jform.
• The new TPS-TEST command allows long runs, without user intervention, in which many proofs are completed and all the timing details are recorded in a file.
• Files in the patch file are now not loaded unless they have been changed since the last time TPS was built; this allows one patch file to work for many different versions of TPS all built at different times.
• The new command ETP prints the shallow formula at all nodes of an etree.
• The test top level has been considerably expanded, and it is now possible for TPS to automatically construct appropriate searchlists for either improving a correct mode, or finding a correct mode.
• The test top level will now fix the unification depths to the correct value as soon as it finds a proof, rather than continuing to vary them.
• The flag MIN-QUANT-ETREE was implemented.
• The flag LAST-MODE-NAME was implemented; TPS now records the name of the current mode when DATEREC is called.
• The library command SHOW-TIMING was implemented; this prints out all the timing records for a given theorem in the library.
• The command COMPARE-MODES was implemented.
• TPS can now measure garbage collecting time in Lucid CL.
• The proofwindows, editor windows, etc. are now available in Lucid CL.
• The problem in which an empty option set was generated many times in each MS91 search has been fixed.