William McCune

From Wikipedia, the free encyclopedia
Jump to: navigation, search
William McCune
Born December 1953
Died May 2011 (2011-06) (aged 57)
Residence USA
Nationality American
Fields Computer Technology
Institutions University of New Mexico
Known for Otter, Mace4, Prover9, Robbins conjecture

William McCune (December 1953 – May 2011) was an American computer scientist and logician working in the fields of Automated reasoning, Algebra, Logic, and Formal Methods. He was best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP theorem prover.


External links[edit]