Skip to main content
SpringerLink
Log in

On sets, types, fixed points, and checkerboards

  • Invited Lectures
  • Conference paper
  • First Online:
Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1071))

Abstract

Most current research on automated theorem proving is concerned with proving theorems of first-order logic. We discuss two examples which illustrate the advantages of using higher-order logic in certain contexts. For some purposes type theory is a much more convenient vehicle for formalizing mathematics than axiomatic set theory. Even theorems of first-order logic can sometimes be proven more expeditiously in higher-order logic than in first-order logic. We also note the need to develop automatic theorem-proving methods which may produce proofs which do not have the subformula property.

This material is based upon work supported by the National Science Foundation under grant CCR-9201893.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, 1986.

    Google Scholar 

  2. 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 (to appear).

    Google Scholar 

  3. Grzegorz Bancerek, “The Mutilated Chessboard Problem — checked by Mizar,” in The QED Workshop II, edited by Roman Matuszewski, 1995, 43–45. Available from http://www.mcs.anl.gov/qed/index.html

    Google Scholar 

  4. Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and Lawrence Wos, Set Theory in First-Order Logic: Clauses for Gödel's Axioms, Journal of Automated Reasoning 2 (1986), 287–327.

    Google Scholar 

  5. Samuel R. Buss, On Gödel's Theorem on Lengths of Proofs I: Number of Lines and Speedup for Arithmetic, Journal of Symbolic Logic 59 (1994), 737–756.

    Google Scholar 

  6. Alonzo Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5 (1940), 56–68.

    Google Scholar 

  7. James Glanz, Computer Scientists Rethink Their Discipline's Foundations, Science 269 (September 1995), 1363–1364.

    Google Scholar 

  8. Kurt Gödel, Über die Länge von Beweisen, Ergebnisse eines Mathematischen Kolloquiums (1936), 23–24. Translated in [10], pp. 396–399.

    Google Scholar 

  9. Kurt Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory, Princeton University Press, Princeton, 1940.

    Google Scholar 

  10. Kurt Gödel, Collected Works, Volume I, Oxford University Press, 1986.

    Google Scholar 

  11. Seth Lloyd, Quantum-Mechanical Computers, Scientific American 273 (October 1995), 140–145.

    Google Scholar 

  12. John McCarthy. A Tough Nut for Proof Procedures, Stanford Artificial Intelligence Project Memo No. 16, 1964. Available from http://www-formal.stanford.edu/jmc/.

    Google Scholar 

  13. John McCarthy. http://www-formal.stanford.edu/jmc/nut.html.

    Google Scholar 

  14. John McCarthy, “The Mutilated Checkerboard in Set Theory,” in The QED Workshop II, edited by Roman Matuszewski, 1995, 25–26. Available from http://www.mcs.anl.gov/qed/index.html.

    Google Scholar 

  15. William McCune, Another Crack in a Tough Nut, Association for Automated Reasoning Newsletter 31 (1995), 1–3.

    Google Scholar 

  16. Richard Statman, Bounds for Proof Search and Speed-up in the Predicate Calculus, Annals of Mathematical Logic 15 (1978), 225–287.

    Google Scholar 

  17. Sakthi Subramanian, An Interactive Solution to the n x n Mutilated Checkerboard Problem, Journal of Logic and Computation (to appear).

    Google Scholar 

  18. Thomas E. Uribe and Mark E. Stickel, “Ordered Binary Decision Diagrams and the Davis-Putnam Procedure,” in Proceedings of the First International Conference on Constraints in Computational Logics, edited by J. P. Jouannaud, Lecture Notes in Computer Science 845, Springer-Verlag, 1994, 34–49.

    Google Scholar 

  19. Larry Wos, Ross Overbeek, Ewing Lusk, Jim Boyle, Automated Reasoning. Introduction and Applications, Prentice Hall, 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematics Department, Carnegie Mellon University, 15213, Pittsburgh, PA, USA

    Peter B. Andrews & Matthew Bishop

Authors
  1. Peter B. Andrews
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew Bishop
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

P. Miglioli U. Moscato D. Mundici M. Ornaghi

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Andrews, P.B., Bishop, M. (1996). On sets, types, fixed points, and checkerboards. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1996. Lecture Notes in Computer Science, vol 1071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61208-4_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-61208-4_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61208-7

  • Online ISBN: 978-3-540-68368-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation