About TPS and ETPS
TPS and ETPS are automated theorem proving systems. The first automated theorem prover for first-order logic and type theory. The latest version of TPS, called ETPS, is intended for use by students and contains only commands related to theorem proving in an interactive mode. TPS and ETPS run on Common Lisp and can be used in any system where Common Lisp is available. TPS and ETPS are widely used on Unix and Linux systems, and to some extent on Windows.
Potential uses of automated theorem proving include hardware and software verification, partial automation of various mathematical activities, contributing to the development of formal theories in a wide range of disciplines, deductive information systems in these disciplines, expert systems capable of reasoning, and some aspects of artificial intelligence.
TPS can be used to prove first-order logic and higher-order logic theorems in an interactive mode, automatically, or in a combination of these modes. However, it is relatively primitive in some respects when used in automatic mode, for example, in dealing with equality. It has facilities for searching for proof extensions, translating them into natural deduction proofs, translating natural deduction proofs that do not contain expansions into proof extensions, and solving the problem of combining higher-order logic. It is a formula editor that facilitates the construction of new formulas from other known TPS formulas and an object library for storing formulas, definitions, and modes (sets of tactics).
Interactive versions of the TPS objects for constructing natural deduction proofs have been used under the name ETPS in logic classes at Carnegie Mellon for several years. Students usually learn to use ETPS quickly, simply by reading the manual (which includes some complete examples) and playing with the system. The student issues commands to apply inference rules in the indicated ways, and the computer handles the details of writing the corresponding proof lines and checking that the rules are being used correctly. Thus, the program allows students to focus on the main logical tasks underlying the proofs, and it provides them with immediate feedback for correct and incorrect actions. ETPS allows students to work forward, backward, or in combinations of these modes, and provides facilities for reconstruction of proofs, deletion of part of a proof, displaying only those parts of a proof actively being considered, and printing on paper. A convenient formula editor allows a student to retrieve necessary formulas occurring somewhere in a proof and build new formulas from them. Guidance for inference and directed questions in ETPS are mostly taken from the textbook: B. Andrew Seth, Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers 2002, description of inference rules available on the Internet. If allowed by the instructor, the student can receive hints from ETPS regarding what to try in different situations. Students can submit comments or questions to the instructor without leaving the program. A completed practice session is supported by ETPS, and can be processed by the GRADER program, which is also part of TPS, and can be used for grading and processing numerical or letter grades for any course. Additional information about ETPS can be found in the ETPS Report: A System to Help Students Create Formal Proofs (PostScript) (PDF).
TPS won the first competition among higher-order theorem proving systems, which had never been held before. The competition, part of the recently created Demonstrations Division of TGF, was a part of the CASC-22 system competition (CASC-22) at the 22nd International Conference on Automated Deduction (CADE-22) in Montreal, Canada, in September 2009.