Solving open questions with an automated theorem-proving program

Abstract

The primary objective of this paper is to demonstrate the feasibility of using an automated theorem-proving program as an automated reasoning assistant. Such usage is not merely a matter of conjecture. As evidence, we cite a number of open questions which were solved with the aid of a theorem-proving program. Although all of the examples are taken from studies employing the single program, AURA [19] (which was developed jointly at Argonne National Laboratory and Northern Illinois University), the nature of the various investigations shows that much of the success also could have been achieved with a number of theorem-proving programs. In view of this fact, one can now correctly state that the field of automated theorem proving has reached an important goal. A theorem-proving program can now be used as an aid to ongoing research in a number of unrelated fields. The open questions are taken from studies of ternary boolean algebra, finite semigroups, equivalential calculus, and the design of digital circuits. Despite the variety of successes, no doubt there still exist many who are very skeptical of the value of automating any form of deep reasoning. It is the nature of this skepticism which brings us to the second objective of the paper. The secondary objective is that of dispelling, at least in part, some of the resistance to such automation. To do this, we discuss two myths which form the basis for the inaccurate evaluation of both the usefulness and the potential of automated theorem proving. Rejection of the two myths removes an important obstacle to assigning to an automated theorem-proving program its proper role—the role of colleague and assistant.