William Walker McCune (17 de diciembre de 1953 - 2 de mayo de 2011) fue un científico informático y lógico estadounidense que trabajó en los campos del razonamiento automatizado , el álgebra , la lógica y los métodos formales .
Fue más conocido por el desarrollo de los sistemas de razonamiento automatizado Otter , Prover9 y Mace4 , y por la prueba automatizada de la conjetura de Robbins utilizando el demostrador de teoremas EQP .
En 2000, McCune recibió el premio Herbrand por sus destacadas contribuciones al razonamiento automatizado . [1] En 2013, se publicó en su honor el libro Razonamiento automatizado y matemáticas: ensayos en memoria de William W. McCune . [2]