Automated Reasoning and Mathematics: Essays in Memory of William McCune

Bill McCune had an enormous impact on automated reasoning, especially with the development of a series of systems of astounding power, robustness, and portability, including the theorem provers Otter, EQP, Prover9, the parallel prover ROO, the proof checker Ivy, and the model builder MACE, preceded by the prototype SAT-solver ANL-DP.

Bill McCune applied these systems to solve open problems in mathematics and logic, culminating with the fully automated solution in 1996 of the Robbins problem that had challenged mathematicians for over sixty years. This result brought unprecedented visibility to the field of automated deduction.

This book will collect articles presenting research in all aspects of automated reasoning and its applications to mathematics to honor his memory and contribute to preserving his legacy.

All interested authors are invited to consult the call for papers:

• Call for papers (plain text)
• Call for papers (pdf)

• Bill McCune's web page with his CV, and plenty of information, in his own words, on his systems, experiments and papers
• The Herbrand Award web page (under the CADE Inc web page)

It is planned that the book will be published as an LNAI Festschrift with Springer. Formatting instructions and the LNCS style files can be obtained at the Springer's website for Authors. For references, authors are kindly asked to list references in alphabetical order, and not in order of appearance, and to use numbers in brackets for citations, and not the (Name Year) style.

The editors of the book:
Maria Paola Bonacina and Mark E. Stickel