William McCune

William Walker "Bill" McCune (* 1953 ; † May 4, 2011 ) was an American mathematician and computer scientist who dealt with automatic proofs .

Life

McCune studied mathematics at the University of Vermont with a bachelor's degree in 1976 and computer science from Northwestern University with a master's degree in 1982 and a doctorate in 1984. He then went to the Argonne National Laboratory, a center of Automated Theorem Proving (ATP) since Larry What . From 1998 he was Senior Computer Scientist and Senior Computational Logician in 2005/06.

He also taught at the University of New Mexico .

At the Argonne National Laboratory he was the developer of programs for ATP such as Otter, Mace4 (a model builder), Prover9, EQP (Equational Prover), the parallel computer program ROO, and the evidence examiner Ivy. Many of them (Prover9, Mace4, Ivy, Otter) are open source software thanks to McCune .

In 1996 he solved the long-standing Robbins problem with the help of ATP (more precisely the EQP program). The problem comes from Herbert Robbins and is to prove that the Robbins algebra is a Boolean algebra . The leading logician Alfred Tarski and his school tried in vain to tackle the long-standing problem (one of the main problems of the ATP) . The solution was perceived by the computer scientists working in the field of ATP as a great confirmation of their field of work.

The Robbins algebra is an algebra with the commutative and associative binary operation and a unary operation (which can be understood as negation). Edward Huntington had investigated such algebras in 1933, which additionally satisfy the Huntington equation (explicitly ), and showed that they lead to Boolean algebras. Herbert Robbins suggested a little later to replace the Huntington's equation with the Robbins equation (explicitly:) and assumed that the resulting Robbins algebra also leads to Boolean algebras. One way to do this is to derive the Hungtington equation within Robbins' algebra. ${\ displaystyle +}$ ${\ displaystyle n (x)}$ ${\ displaystyle n (n (x) + y) + n (n (x) + n (y)) = x}$ ${\ displaystyle n (n (x + y) + n (x + n (y))) = x}$

In 2000 he received the Herbrand Award .

He should not be confused with the engineer William James McCune (* 1915), who was the CEO of Polaroid.

Fonts

with R. Padmanabhan: Automated Deduction in Equational Logic and Cubic Curves, Lecture Notes in Computer Science 1096, Springer-Verlag, Berlin, 1996.
Solution of the Robbins Problem, Journal of Automated Reasoning, Volume 19, 1997, pp. 263-276
with R. Boyer, E. Lusk, R. Overbeek, M. Stickel, L. Wos: Set theory in first-order logic: Clauses for Gödel's axioms. J. Automated Reasoning, Vol. 2, 1986, pp. 287-327
with C. Wick: Automated reasoning about elementary point-set topology. J. Automated Reasoning, Vol. 5, 1989, pp. 239-255
with L. Wos: Automated theorem proving and logic programming: A natural symbiosis, J. Logic Programming, Volume 11, 1991, pp. 1-53
with L. Wos: The application of automated reasoning to questions in mathematics and logic, Annals of Mathematics and Artificial Intelligence, Volume 5, 1992, pp. 321-370

literature

Maria Paola Bonacina, Mark E. Stickel (Eds.): Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, Lecture Notes in Artificial Intelligence 7788, Springer 2013

Web links

Individual evidence

↑ Website for the book

personal data
SURNAME	McCune, William
ALTERNATIVE NAMES	McCune, William Walker; McCune, Bill
BRIEF DESCRIPTION	American mathematician
DATE OF BIRTH	1953
DATE OF DEATH	May 4, 2011

[1] Website for the book