Publications

L. Wos and B. Fitelson, "Automating the Search for Answers to Open Questions," Preprint ANL/MCS-P825-0500, May 2000. [pdf]

This article provides evidence for the arrival of automated reasoning. Indeed, one of its primary goals of the early 1960s has been reached: The use of an automated reasoning program frequently leads to significant contributions to mathematics and to logic. In addition, although not clearly an original objective, the use of such a program now plays an important role for chip design and for program verification. That importance can be sharply increased; indeed, in this article we discuss the possible value of automated reasoning to finding better designs of chips, circuits, and computer code. We also provide insight into the mechanisms—in particular, strategy—that have led to numerous successes. To complement the evidence we present and to encourage further research, we offer challenges and open questions for consideration. We include a glimpse of the future and some commentary on the possibly unexpected benefits of automating the search for answers to open questions.