Automated reasoning about elementary point-set topology

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 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.