This tutorial will teach participants how to make effective use of TPS and ETPS, and provide hands-on experience with these programs.
TPS is an automated theorem proving system which can be used to prove theorems of first- or higher-order logic automatically, interactively, or in a combination of these modes of operation. Proofs in TPS are presented in natural deduction style. ETPS is a program which was obtained from TPS by deleting all the facilities for proving theorems automatically. ETPS can be used by students to learn how to prove theorems interactively.
Information about TPS, including manuals and information about obtaining the system, can be found at http://gtps.math.cmu.edu/tps.html.
There will be a discussion of how to use ETPS as a teaching tool in logic courses. ETPS can be used effectively in a course which is concerned purely with first-order logic as well as one which also deals with higher-order logic. Students using ETPS can construct rigorous proofs of harder theorems than they would find it practical to construct without ETPS. ETPS gives students immediate feedback for both correct and incorrect actions, checks proofs automatically, and creates records of the theorems proved by each student which can be automatically transferred to the teacher's grade file.
The logical language of TPS is Church's type theory, a formulation of higher-order logic in which theorems of mathematics can be expressed very naturally. The notation of this language is displayed on the screen and in printed proofs. Definitions are handled elegantly by lambda-notation.
Participants in the tutorial are expected to be familiar with first-order logic, but no familiarity with higher-order logic will be presupposed. There will be an introduction to the notation of type theory, examples showing how to express theorems of mathematics (including those involving inductive definitions) in this language, and lessons on how to write theorems and definitions in TPS and put them into a TPS library.
It will be shown how to use the rules of inference for constructing natural deduction proofs, which are common to TPS and ETPS. Additional facilities for using tactics to apply these rules semi-automatically, which are available in TPS but not in ETPS, will also be exhibited. It will be shown how the automatic procedures in TPS can be used to fill gaps in a partially completed natural deduction proof.
TPS searches for proofs in automatic mode by first searching for an expansion proof, and then translating this into a natural deduction proof. TPS has a number of search procedures, and there are many flags which control the behavior of TPS and set bounds for the many dimensions of proof search in higher-order logic. A discussion of these matters will prepare the potential user of TPS to learn how to set the flags in ways that will produce automatic proofs of chosen theorems.
The tutorial will include a general survey of the many features of TPS which make it a useful research tool. These include proof windows (where the proof, and the active lines of the proof, are displayed as the proof is constructed interactively), facilities for rearranging proofs and displaying selected parts of them, separate top-levels for unification problems and mating searches, vertical path diagrams, facilities for printing proofs in various styles including tex, the formula editor, the library, online help, and documentation (some of which is produced automatically).
Participants are encouraged to bring to the tutorial one or more simple theorems about sets, functions, and relations (which need not be theorems of first-order logic) which can be used as examples to demonstrate how various things are done in TPS.
Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, 1986.
Peter B. Andrews, "On Connections and Higher-Order Logic", Journal of Automated Reasoning 5 (1989), 257-291.
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi, "TPS: A Theorem Proving System for Classical Type Theory", Journal of Automated Reasoning 16 (1996), 321-353.
Matthew Bishop and Peter B. Andrews, "Selectively Instantiating Definitions", Automated Deduction - CADE-15; 15th International Conference on Automated Deduction, Springer, Lecture Notes in Artificial Intelligence 1421, edited by Claude Kirchner and Helene Kirchner, Lindau, Germany, 1998, 365-380.
Matthew Bishop, "A Breadth-First Strategy for Mating Search", 16th International Conference on Automated Deduction (CADE-16), edited by Harald Ganzinger, Trento, Italy, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag, 1999, 359-373.
Doug Goldson, Steve Reeves and Richard Bornet, "A Review of Several Programs for the Teaching of Logic", The Computer Journal 36 (1993), 373-386.
Sunil Issar, "Path-Focused Duplication: A Search Procedure for General Matings", AAAI-90. Proceedings of the Eighth National Conference on Artificial Intelligence, July 29, 1990 - August 3, 1990, AAAI Press/The MIT Press Volume 1, 221-226.
Dale A. Miller, "A Compact Representation of Proofs", Studia Logica XLVI, 1987, 347-370.
Frank Pfenning and Dan Nesmith, "Presenting Intuitive Deductions via Symmetric Simplification", 10th International Conference on Automated Deduction, edited by M. E. Stickel, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, 336-350.