Automated Reasoning and Mathematics: Essays in Memory of William W. McCune

This web page is about the Festschrift dedicated to the memory of the 2000 Herbrand Award winner William W. (Bill) McCune (1953-2011). 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. The Festschrift collects articles presenting research in all aspects of automated reasoning and its applications to mathematics, to honor Bill's memory and contribute to preserving his legacy:

Book cover picture: Otter

The call for papers is now closed and is left here for reference:

Maria Paola Bonacina