Abstract
This is a brief update on the Tps automated theorem proving system for classical type theory, which was described in [3]. Manuals and information about obtaining Tps can be found at http://gtps.math.cmu.edu/tps.html.
In Section 2 we discuss some examples of theorems which Tps can now prove automatically, and in Section 3 we discuss an example which illustrates one of the many challenges of theorem proving in higher-order logic. We first provide a brief summary of the key features of Tps.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andrews, P.B.: Theorem Proving via General Matings. Journal of the ACM 28, 193–214 (1981)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, London (1986)
Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning 16, 321–353 (1996)
Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg, Braunschweig (1987)
Bishop, M.: A Breadth-First Strategy for Mating Search. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 359–373. Springer, Heidelberg (1999)
Bishop, M.: Mating Search Without Path Enumeration. PhD thesis, Department of Mathematical Sciences. Carnegie Mellon University (April 1999), Department of Mathematical Sciences Research Report No. 99-223, Available at http://gtps.math.cmu.edu/tps.html
Bishop, M., Andrews, P.B.: Selectively Instantiating Definitions. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 365–380. Springer, Heidelberg (1998)
Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940)
Issar, S.: Path-Focused Duplication: A Search Procedure for General Matings. In: AAAI-90, vol. 1, pp. 221–226. AAAI Press, Menlo Park (1990)
Issar, S.: Operational Issues in Automated Theorem Proving Using Matings. PhD thesis. Carnegie Mellon University, 147 pff (1991)
Miller, D.A.: A Compact Representation of Proofs. Studia Logica 46(4), 347–370 (1987)
Paulson, L., Grabczewski, K.: Mechanising Set Theory: Cardinal Arithmetic and the Axiom of Choice. Journal of Automated Reasoning 17, 291–323 (1996)
Pfenning, F.: Proof Transformations in Higher-Order Logic. PhD thesis. Carnegie Mellon University, 156 pff (1987)
Pfenning, F., Nesmith, D.: Presenting Intuitive Deductions via Symmetric Simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 336–350. Springer, Heidelberg (1990)
Rubin, H., Rubin, J.E.: Equivalents of the Axiom of Choice, II. North- Holland, Amsterdam (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andrews, P.B., Bishop, M., Brown, C.E. (2000). System Description: TPS: A Theorem Proving System for Type Theory. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_11
Download citation
DOI: https://doi.org/10.1007/10721959_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive