William McCune

William Walker „Bill“ McCune (* 1953; † 4. Mai 2011) war ein US-amerikanischer Mathematiker und Informatiker, der sich mit Automatischem Beweisen befasste.

Leben

McCune studierte Mathematik an der University of Vermont mit dem Bachelor-Abschluss 1976 und Informatik an der Northwestern University mit dem Master-Abschluss 1982 und der Promotion 1984. Danach war er am Argonne National Laboratory, einem Zentrum des Automated Theorem Proving (ATP) seit Larry Wos. Ab 1998 war er dort Senior Computer Scientist und 2005/06 Senior Computational Logician.

Daneben lehrte er an der University of New Mexico.

Er war am Argonne National Laboratory der Entwickler von Programmen zum ATP wie Otter, Mace4 (ein Model Builder), Prover9, EQP (Equational Prover), dem Parallelrechner-Programm ROO, dem Beweisprüfer Ivy. Viele davon (Prover9, Mace4, Ivy, Otter) sind dank McCune Open Source Software.

1996 löste er das lange offene Robbins-Problem mit Hilfe von ATP (genauer dem Programm EQP). Das Problem stammt von Herbert Robbins und besteht darin zu beweisen, dass die Robbins-Algebra eine Boolesche Algebra ist. An dem lange offenen Problem (einem der Hauptprobleme des ATP) versuchten sich schon der führende Logiker Alfred Tarski und seine Schule vergeblich. Die Lösung wurde von Seiten der auf dem Gebiet des ATP tätigen Informatiker als große Bestätigung ihres Arbeitsfeldes wahrgenommen.

Bei der Robbins Algebra handelt es sich um eine Algebra mit der kommutativen und assoziativen binären Operation $+$ und einer unären Operation $n(x)$ (die man als Negation auffassen kann). Edward Huntington hatte 1933 solche Algebren untersucht, die zusätzlich die Huntington-Gleichung (explizit $n(n(x)+y)+n(n(x)+n(y))=x$) erfüllen, und gezeigt, dass sie auf Boolesche Algebren führen. Herbert Robbins schlug wenig später vor, die Huntington-Gleichung durch die Robbins-Gleichung (explizit: $n(n(x+y)+n(x+n(y)))=x$) zu ersetzen und vermutete, dass die so entstehende Robbins-Algebra ebenfalls auf Boolesche Algebren führt. Eine Möglichkeit dazu ist die Ableitung der Huntington-Gleichung innerhalb der Robbins-Algebra.

2000 erhielt er den Herbrand Award.

Er sollte nicht mit dem Ingenieur William James McCune (1915–2017) verwechselt werden, der CEO von Polaroid war.

Schriften

• mit Robert Boyer, Ewing Lusk, Ross Overbeek, Mark Stickel, Lawrence Wos: Set theory in first-order logic: Clauses for Gödel’s axioms. In: Journal of Automated Reasoning. Band 2, Nr. 3, 1986, S. 287–327, doi:10.1007/BF02328452.
• mit Cynthia A. Wick: Automated reasoning about elementary point-set topology. In: Journal of Automated Reasoning. Band 5, Nr. 2, 1989, S. 239–255, doi:10.1007/BF00243005.
• mit Larry Wos: Automated theorem proving and logic programming: A natural symbiosis. In: The Journal of Logic Programming. Band 11, Nr. 1, 1991, S. 1–53, doi:10.1016/0743-1066(91)90008-D.
• mit Larry Wos: The application of automated reasoning to questions in mathematics and logic. In: Annals of Mathematics and Artificial Intelligence. Band 5, Nr. 2/4, 1992, S. 321–370, doi:10.1007/BF01543481.
• mit Ranganathan Padmanabhan: Automated Deduction in Equational Logic and Cubic Curves (= Lecture Notes in Computer Science. 1095). Springer, Berlin u. a. 1996, ISBN 3-540-61398-6.
• Solution of the Robbins Problem. In: Journal of Automated Reasoning. Band 19, Nr. 3, 1997, S. 263–276, doi:10.1023/A:1005843212881.

Literatur

• Maria Paola Bonacina, Mark E. Stickel (Hrsg.): Automated Reasoning and Mathematics. Essays in Memory of William W. McCune (= Lecture Notes in Computer Science. 7788). Springer, Berlin u. a. 2013, ISBN 978-3-642-36674-1.

Weblinks

• Homepage an der University of New Mexico
• William McCune: Robbins Algebras Are Boolean
• David Wheeler, Nachruf auf seinem Blog 2014