Summary

In this history of Argonne-style theorem proving we have focused on the common theme that has run through all the systems in the extensive family: the use of the closure approach to theorem proving. It is this approach that provides the redundancy control necessary for successful navigation of the large search spaces that characterize significant problems.