Abstract
In this paper we present first-order formulas for basic point-set topology, in an attempt to extend the mathematical range available for exploration with automated theorem-proving programs. We present topology definitions and sample lemmas both in first-order logic and in clausal form. We then illustrate some of the difficulties of these sample lemmas through a proof of a basic lemma in five parts.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Bledsoe, W. W., ‘Non-resolution theorem proving’, Artificial Intelligence 9, 1–35 (1977).
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, 287–327 (1986).
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).
Kelley, J. L., General Topology, D. Van Nostrand, New York (1955).
Lusk, E. and Overbeek, R., ‘The automated reasoning system ITP’, ANL-84–27, Argonne National Laboratory, Argonne, Ill. (April 1984).
McCune, W., ‘Otter user's guide’, ANL-88–44, Argonne National Laboratory, Argonne, Ill. (1988).
Munkres, F. R., Topology: A First Course, Prentice-Hall, Englewood Cliffs, N.J. (1975).
Potter, R. C. and Plaisted, D. A., ‘Term rewriting: some experimental results’, Proceedings of the 9th International Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science 310, 435–454 (1988).
Smith, B. T., ‘Reference manual for the environmental theorem prover, an incarnation of aura’, ANL-88–2, Argonne National Laboratory, Argonne, IL (1988).
Stickel, M., ‘A non-clausal connection-graph resolution theorem-proving program’, Proceedings of the AIAA-82 National Conference on Artificial Intelligence, Pittsburgh, 229–233 (1982).
Stickel, M., ‘Schubert's steamroller problem: formulations and solutions’, J. Automated Reasoning 2, 89–101 (1986).
Wos, L., Veroff, R., Smith, B. T., and McCune, W., ‘The linked inference principle II: the user's view’, Proceedings of the Seventh International Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science 170, 316–332 (1984).
Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning: Introduction and Applications Prentice-Hall, Englewood Cliffs, N.J. (1984).
Author information
Authors and Affiliations
Additional information
This work was 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 by the Division of Educational Programs, Argonne National Laboratory.
Rights and permissions
About this article
Cite this article
Wick, C.A., McCune, W.W. Automated reasoning about elementary point-set topology. J Autom Reasoning 5, 239–255 (1989). https://doi.org/10.1007/BF00243005
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00243005