Bill McCune
1953 - 2011

Bill's untimely passing has shocked and saddened his many friends and
colleagues in the automated deduction community.

Bill grew up in the northeastern part of the U.S. and attended the
University of Vermont. He subsequently moved to the Chicago area and
got his Ph.D. in Computer Science from Northwestern University in 1984.
He worked at Argonne National Laboratory from 1984 until 2006, where
he had the title of Senior Computational Logician. Bill left Argonne
in 2006 to become a research faculty member at the University of New
Mexico in Albuquerque. He would have turned 58 this December.

Bill is perhaps best known for his expertise in the design and
implementation of automated reasoning programs, including Otter,
Prover9 and Mace4.  With their wide selection of advanced features,
sophisticated strategies and state-of-the-science algorithms and
data structures, these programs are recognized both for their power
and their performance.  Otter, in particular, continues to be used as a
benchmark to evaluate other programs. Most importantly, Bill's programs
have been used to solve numerous open questions in mathematics and logic
and continue to be used by researchers from various disciplines.

Bill also was an expert in the application of automated reasoning methods,
and he used his programs to solve several open questions; results have
appeared in journal publications, conference proceedings and a research
monograph. Bill received special recognition for his solution in 1996 to
the "Robbins Problem", a challenge problem proposed by the logician Alfred
Tarski and worked on (unsuccessfully) by several of Tarski's students.

Bill was honored with the Herbrand award in 2000 for distinguished
contributions to automated deduction.  In addition to his own research,
he served on the editorial board of the Journal of Automated Reasoning and
on the program committees of several conferences and workshops.  He was
the program chair for CADE-14 in 1997.  While at Argonne, Bill hosted and
mentored young researchers who have matured into leading researchers in
our field.

Bill will be sorely missed but will continue to be remembered for his
many contributions.