Automated theorem proving started at Argonne in the early nineteen-sixties and remains a very active area of research there today. The theorem-proving systems developed during that last nearly thirty years have, in each generation, been among the most capable systems in the world, as new ideas have been incorporated into whatever the current program has been. Periodically programs have been replaced with entirely new ones, as the weight of accumulated additions and changes in computer science and computing as a whole have made completely new systems desirable.
Throughout all this change, however, certain ideas have remained constant. Some of them have been philosophical, such as the use of specific problems to motivate progress and the maintenance of a single, powerful current system, incorporating all of the features developed up to that point. In this paper we would like to focus on one central technical aspect that has remained exactly the same through multiple generations of systems and has perhaps been overlooked as a source of the success of the Argonne systems. We will call this feature the closure approach for reasons that will become apparent below. It is at the heart of all of the Argonne programs.
In this paper we will first explain in detail exactly what the closure approach is, and then illustrate how it has been able to continue to serve as a framework for a very wide variety of new ideas in automated reasoning. We will do the illustrating with a historical review of the major families of system that have been built and used at Argonne over the years. We will conclude by describing some current work that continues to be based on the same theorem-proving paradigm.