The Flowering of Automated Reasoning

TitleThe Flowering of Automated Reasoning
Publication TypeBook Chapter
Year of Publication2005
AuthorsWos, L
Book TitleA Portrait to a Scientist: Logic, AI and Politics, A Festschrift in Honor of J. H. Siekmann
Other NumbersANL/MCS-P924-0102

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.