The Flowering of Automated Reasoning
|Title||The Flowering of Automated Reasoning|
|Publication Type||Book Chapter|
|Year of Publication||2005|
|Book Title||A Portrait to a Scientist: Logic, AI and Politics, A Festschrift in Honor of J. H. Siekmann|
This article celebrates the obvious joy the role automated reasoning now plays for mathematics and logic. Simultaneously, this article evidences the realization of a dream thought impossible just four decades ago by almost all. But there were believers, including Joerg Siekmann to whom this article is dedicated in honor of his sixtieth birthday. Indeed, today (in the year 2001), a researcher can enlist the aid of an automated reasoning program often with the reward of a new proof or a better proof in some significant aspect. The contributions to mathematics and logic made with an automated reasoning assistant are many, diverse, often significant, and of the type Hilbert would indeed have found most pleasurable. The proofs discovered by W. McCune\'s OTTER (as well as other programs) are Hilbert-style axiom twenty-fourth problem (recently unearthed by Rudiger Thiele), which focuses on the completion of simpler proofs. In that regard, as well as others, I offer challenges and open questions, frequently providing appropriate clauses to provide a beginning.