William McCune

You can help expand this article with text translated from the corresponding article in German. (March 2024) Click [show] for important translation instructions. Machine translation, like DeepL or Google Translate, is a useful starting point for translations, but translators must revise errors as necessary and confirm that the translation is accurate, rather than simply copy-pasting machine-translated text into the English Wikipedia. Do not translate text that appears unreliable or low-quality. If possible, verify the text with references provided in the foreign-language article. You must provide copyright attribution in the edit summary accompanying your translation by providing an interlanguage link to the source of your translation. A model attribution edit summary is Content in this edit is translated from the existing German Wikipedia article at [[:de:William McCune]]; see its history for attribution. You may also add the template {{Translated|de|William McCune}} to the talk page. For more guidance, see Wikipedia:Translation.

William Walker McCune (December 17, 1953 – May 2, 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.

In 2000, McCune received the Herbrand Award for Distinguished Contributions to Automated Reasoning.^[1] In 2013, Automated Reasoning and Mathematics - Essays in Memory of William W. McCune was published in his honour.^[2]

• Prover9 software
• William McCune home page
• Updated version of Prover9 software