Abstract
This is description of TPS, a theorem-proving system for classical type theory (Church's typed λ-calculus). TPS has been designed to be a general research tool for manipulating wffs of first- and higher-order logic, and searching for proofs of such wffs interactively or automatically, or in a combination of these modes. An important feature of TPS is the ability to translate between expansion proofs and natural deduction proofs. Examples of theorems that TPS can prove completely automatically are given to illustrate certain aspects of TPS's behavior and problems of theorem proving in higher-order logic.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Andrews, P. B.: Resolution in type theory, J. Symbolic Logic 36 (1971), 414–342.
Andrews, P. B.: Provability in elementary type theory, Z. Math. Logic und Grundlagen der Mathematik 20 (1974), 411–418.
Andrews, P. B.: Refutations by matings, IEEE Trans. Computers C-25 (1976), 801–807.
Andrews, P. B.: Transforming matings into natural deduction proofs, in W. Bibel and R. Kowalski (eds), 5th Conf. Automated Deduction, Les Arcs, France, Lecture Notes in Computer Sci. 87, Springer-Verlag, 1980, pp. 281–292.
Andrews, P. B.: Theorem proving via general matings. J. ACM 28 (1981), 193–214.
Andrews, P. B., Miller, D. A., Cohen, E. L., and Pfenning, F.: Automating higher-order logic, in W. W. Bledsoe and D. W. Loveland (eds), Automated Theorem Proving: After 25 Years, Contemporary Mathematics Series, Vol. 29, Amer. Math. Soc., 1984, pp. 169–192.
Andrews, P. B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Academic Press, New York, 1986.
Andrews, P. B.: On connections and higher-order logic. J. Automated Reasoning 5 (1989), 257–291.
Andrews, P. B., Issar, S., Nesmith, D., Pfenning, F., Xi, H., and Bishop, M.: TPS3 Facilities Guide for Programmers and Users, 1994.
Andrews, P. B., Issar, S., Nesmith, D., Pfenning, F., Xi, H., and Bishop, M.: TPS3 Facilities Guide for Users, 1994.
Bailin, S. C. and Barker-Plummer, D.: Z-match: An inference rule for incrementally elaborating set instantiations. J. Automated Reasoning 11 (1993), 391–428. Errata: JAR 12 (1994), 411–412.
Barker-Plummer, D.: Gazing: An approach to the problem of definition and lemma use, J. Automated, Reasoning 8 (1992), 311–344.
Bibel, W.: Automated Theorem Proving, Vieweg, Braunschweig, 1987.
Bishop, M., Nesmith, D., Pfenning, F., Issar, S., Andrews, P. B., and Xi, H.: TPS3 Programmer's Guide, 1994.
Bledsoe, W. W. and Bruell, P.: A man-machine theorem-proving system, Artificial Intelligence 5 (1974), 51–72.
Bledsoe, W. W.: A maximal method for set variables in automatic theorem proving, in J. E.Hayes, D.Michie, and L. I.Mikulich (eds), Machine Intelligence, Vol. 9, Ellis Harwood Ltd., Chichester, and Wiley, New York, 1979, pp. 53–100.
Bledsoe, W. W. and Feng, G.: Set-var, J. Automated Reasoning 11 (1993), 293–314.
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., and Wos, L.: Set theory in first-order logic: Clauses for Gödel's axioms, J. Automated Reasoning 2 (1986), 287–327.
Church, A.: Introduction to Mathematical Logic, Princeton University Press, Princeton, NJ, 1956.
Church, A.: A formulation of the simple theory of types, J. Symbolic Logic 5 (1940), 56–68.
Constable, R. L. et al.: Implementing Mathematics with the Nuprl Proof Development System, Prentice Hall, 1986.
Coquand, T. and Huet, G.: The calculus of constructions, Information and Computation 76 (1988), 95–120.
Farmer, W. M., Guttman, J. D., and Thayer, J.: IMPS: An interactive mathematical proof system, J. Automated Reasoning 11 (1993), 213–248.
Gallier, J. H., Narendran, P., Raatz, S., and Snyder, W.: Theorem proving using equational matings and rigid E-unification. J. ACM 39 (1992), 377–429.
Goldson, D. and Reeves, S.: Using programs to teach logic to computer scientists, Notices Amer. Math. Soc. 40 (1993), 143–148.
Goldson, D., Reeves, S., and Bornat, R.: A review of several programs for the teaching of logic, Computer J. 36 (1993), 373–386.
Gordon, M. J. C., Milner, A. J., and Wadsworth, C. P.: Edinburgh LCF, Lecture Notes Computer Sci. 78, Springer-Verlag, 1979.
Gordon, M. J. C.: HOL: A proof generating system for higher-order logic, in G.Birtwistle and P. A.Subrahmanyam (eds), VLSI Specification, Verification, and Synthesis, Kluwer, Dordrecht, 1988, pp. 73–128.
Gordon, M. J. C. and Melham, T. F.(eds): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge University Press, 1993.
Helmink, L. and Ahn, R.: Goal directed proof construction in type theory, in G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991, pp. 120–148.
Huet, G. P.: A mechanization of type theory, in Proc. 3rd Int. Joint Conf. Artificial Intelligence, IJCAI, 1973, pp. 139–146.
Huet, G. P.: A unification algorithm for typed λ-calculus, Theor. Comp. Sci. 1 (1975), 27–57.
Issar, S.: Path-focused duplication: A search procedure for general matings, in AAAI-90 Proc. 8th Nat. Conf. Artificial Intelligence, AAAI Press/The MIT Press, 1990, pp. 221–226.
Issar, S.: Operational issues in automated theorem proving using matings, PhD Thesis, Carnegie Mellon University, 1991.
Issar, S., Andrews, P. B., Pfenning, F., and Nesmith, D.: GRADER Manual, 1992.
Kolodner, I. I.: Fixed points, Amer. Math. Monthly 71, (1964), 906.
Miller, D. A., Cohen, E. L., and Andrews, P. B.: A look at TPS, in D. W. Loveland (ed.), 6th Conf. Automated Deduction, Lecture Notes in Computer Sci. 138, Springer-Verlag, 1982, pp. 50–69.
Miller, D. A.: Proofs in higher-order logic, PhD Thesis, Carnegie Mellon University, 1983.
Miller, D. A.: Expansion tree proofs and their conversion to natural deduction proofs, in R. E. Shostak (ed.), 7th Int. Conf. Automated Deduction, Lecture Notes in Computer Sci. 170, Springer-Verlag, 1984, pp. 375–393.
Miller, D. A.: A compact representation of proofs, Stud. Logica 46 (1987), 347–370.
Milner, R.: A theory of type polymorphism in programming, J. Computer System Sci. 17 (1978), 348–375.
Nesmith, D., Bishop, M., Andrews, P. B., Issar, S., Pfenning, F., and Xi, H.: TPS User's Manual, 1994.
Ohlbach, H. J.: A resolution calculus for modal logics, PhD Thesis, Department of Computer Science, University of Kaiserslautern, 1988.
Paulson, L. C.: The foundation of a generic theorem prover, J. Automated Reasoning 5, (1989), 363–397.
Pfenning, F.: Analytic and non-analytic proofs, in R. E. Shostak (ed.), 7th Int. Conf. Automated Deduction, Lecture Notes Computer Sci. 170, Springer-Verlag, 1984, pp. 394–413.
Pfenning, F.: Proof transformations in higher-order logic, PhD Thesis, Carnegie Mellon University, 1987.
Pfenning, F. and Nesmith, D.: Presenting intuitive deductions via symmetric simplification, in M. E. Stickel (ed.), 10th Int. Conf. Automated Deduction, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 336–350.
Pfenning, F., Issar, S., Nesmith, D., Andrews, P. B., Xi, H., and Bishop, M.: ETPS User's Manual, 1994.
Quaife, A.: Andrews' challenge problem revisited, AAR Newslet. 15 (1990), 3–7.
Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. ACM 12 (1965), 23–41.
Russell, B.: The Principles of Mathematics, Cambridge University Press, 1903.
Russell, B.: Mathematical logic as based on the theory of types, Amer. J. Math. 30 (1908), 222–262. Reprinted in [55], pp. 150–182.
Snyder, W.: Higher-order E-unification, in M. E. Stickel (ed.), 10th Int. Conf. Automated Deduction, Kaiserslautern, FRG, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 573–587.
Sutcliffe, G., Suttner, Ch., and Yemenis, T.: The TPTP problem library, in A. Bundy (ed.), Automated Deduction — CADE-12, 12th Int. Conf. Automated Deduction, Nancy, France, Lecture Notes in Artificial Intelligence 814, Springer-Verlag, 1994, pp. 252–266.
vanHeijenoort, J.: From Frege to Gödel, Harvard University Press, Cambridge, MA, 1967.
Wallen, L. A.: Automated Deduction in Nonclassical Logics, The MIT Press, 1990.
Whitehead, A. N. and Russell, B.: Principia Mathematica, 3 vols, Cambridge University Press, Cambridge, England, 1910–1913.
Wos, L.: The problem of definition expansion and contraction, J. Automated Reasoning 3 (1987), 433–435.
Author information
Authors and Affiliations
Additional information
This material is based upon work supported by the National Science Foundation under grant CCR-9201893 and previous grants.
Rights and permissions
About this article
Cite this article
Andrews, P.B., Bishop, M., Issar, S. et al. TPS: A theorem-proving system for classical type theory. Journal of Automated Reasoning 16, 321–353 (1996). https://doi.org/10.1007/BF00252180
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF00252180