William McCune
Encyclopedia
William McCune was an American
computer scientist
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.
United States
The United States of America is a federal constitutional republic comprising fifty states and a federal district...
computer scientist
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
working in the fields of Automated reasoning
Automated reasoning
Automated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...
, Algebra
Algebra
Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...
, Logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, and Formal Methods
Formal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
. He was best known for the development of the Otter, Prover9
Prover9
Prover9 is an automated theorem prover for First-order and equational logic developed by William McCune. Prover9 is the successor of the Otter theorem prover.Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples...
, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP
EQP
EQP, an abbreviation for equational prover, is an automated theorem proving program for equational logic, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory. It was one of the provers used for solving a longstanding problem posed by Herbert Robbins,...
theorem prover.