## 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:
- Larry Wos.
The Legacy of a Great Researcher.
- Leonardo de Moura and Grant Olney Passmore.
The Strategy Challenge in SMT Solving.
- Stephan Schulz.
Simple and Efficient Clause Subsumption with Feature Vector Indexing.
- Thomas Hillenbrand and Christoph Weidenbach.
Superposition for Bounded Domains.
- Hantao Zhang and Jian Zhang.
Mace4 and SEM: A Comparison of Finite Model Generators.
- Eric Ens and Ranganathan Padmanabhan.
Group Embedding of the Projective Plane PG(2,3).
- Ranganathan Padmanabhan and Robert Veroff.
A Geometric Procedure with Prover9.
- Michael Kinyon, Robert Veroff, and Petr Vojtechovský.
Loops with abelian inner mapping groups: an application of automated deduction.
- Rob Arthan and Paulo Oliva.
(Dual) Hoops Have Unique Halving.
- Branden Fitelson.
Gibbardâ€™s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach.
- Deepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi Lu, and ThanhVu Nguyen.
Geometric Quantifier Elimination Heuristics for Automatically Generating
Octagonal and Max-plus Invariants.
- Zachary Ernst and Seth Kurtenbach. Toward a Procedure for Data Mining Proofs.
- Josef Urban and Jirí Vyskocil.
Theorem Proving in Large Formal Mathematics as an Emerging AI Field.

Book cover picture:
Otter

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

*Maria Paola Bonacina*