[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Set theory in first-order logic: Clauses for Gödel's axioms

  • Problem Corner
  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

In this paper we present a set of clauses for set theory, thus developing a foundation for the expression of most theorems of mathematics in a form acceptable to a resolution-based automated theoren prover. Because Gödel's formulation of set theory permits presentation in a finite number of first-orde formulas, we employ it rather than that of Zermelo-Fraenkel. We illustrate the expressive power of thi formulation by providing statements of some well-known open questions in number theory, and give some intuition about how the axioms are used by including some sample proofs. A small set of challeng problems is also given.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. BledsoeW. W., ‘Splitting and reduction heuristics in automatic theorem proving’,Artificial Intelligence 2 55–77 (1971).

    Article  MATH  Google Scholar 

  2. Bledsoe, W. W., ‘Some automatic proofs in analysis’, inAutomated Theorem Proving: After 25 Years, (eds. D. Loveland and W. W. Bledsoe), American Mathematical Society (1984).

  3. Gödel, K.,The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Princeton University Press (1940).

  4. KellyJ.,General Topology, D. van Nostrand, Princeton, New Jersey (1955).

    Google Scholar 

  5. McDonald, J. and Suppes, P., ‘Student use of an interactive theorem prover’, inAutomated Theorem Proving: After 25 Years, (eds. D. Loveland and W. W. Bledsoe), American Mathematical Society (1984).

  6. MorseA. P.,A Theory of Sets, Academic Press, New York (1965).

    Google Scholar 

  7. Pastre, D., ‘Demonstration automatique de theoremes en theorie des ensembles’, Paris 6 (1976). (Ph.D. thesis)

  8. Quine, W.,Set Theory and Its Logic, Harvard University Press (1969).

  9. ShoenfieldJ. R.,Mathematical Logic, Addison-Wesley, Reading, Ma. (1967).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microelectronics and Computer Technology Corporation, 9430 Research Boulevard, 78759, Austin, TX, USA

    Robert Boyer

  2. Mathematics and Computer Science Division, Argonne National Laboratory, 60439 4844, Argonne, IL, USA

    Ewing Lusk, William McCune, Ross Overbeek & Lawrence Wos

  3. Artificial Intelligence Center, SRI International, 94025, Menlo Park, CA, USA

    Mark Stickel

Authors
  1. Robert Boyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ewing Lusk
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. William McCune
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ross Overbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mark Stickel
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Lawrence Wos
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This work was partially supported by the Applied Mathematical Sciences subprogram of the office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38, and partially supported by the Defence Advanced Research Projects Agency under contract N00039-84-K-0078 with the Naval Electronic Systems Command.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Boyer, R., Lusk, E., McCune, W. et al. Set theory in first-order logic: Clauses for Gödel's axioms. J Autom Reasoning 2, 287–327 (1986). https://doi.org/10.1007/BF02328452

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02328452

Key words

Search

Navigation