William McCune

William McCune

name = William McCune

image_width= 200px
caption = William McCune
residence = USA
nationality = American
field = Computer Technology
work_institution = University of New Mexico
known_for = Otter, Mace, Prover9, Robbins conjecture

William McCune is an American computer scientist working in the fields of
Automated reasoning, Algebra, Logic, and Formal Methods.He is best known for the development of the Otter (theorem prover), Prover9, and Maceautomated reasoning systems, and the automated proof of the Robbins conjecture.

Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Alfred McCune Home — Coordinates: 40°46′26″N 111°53′26″W / 40.77389°N 111.89056°W / 40.77389; 111.89056 …   Wikipedia

  • Lisa McCune — [[Archivo:[1]|200px]] Nacimiento 19 de febrero de 1971 (40 años) Perth, Western Australia, Australia Pareja Tim Disney (2000 presente) Hijo/s …   Wikipedia Español

  • Lisa McCune — Infobox actor name = Lisa McCune imagesize = caption = birthdate = birth date and age|1971|2|19|df=yes location = Sydney, New South Wales, Australia occupation = Actress height = deathdate = birthname = othername = homepage = spouse = Tim Disney… …   Wikipedia

  • Richard William Enraght — Infobox clergy name = Richard William Enraght image size = 200px caption = Fr. Richard Enraght SSC.reproduced by kind permission of the Principal Chapter of Pusey House, Oxford.(Hall Collection 3/13, Pusey House Oxford) birth date = February 23… …   Wikipedia

  • Boolean algebra (structure) — For an introduction to the subject, see Boolean algebra#Boolean algebras. For the elementary syntax and axiomatics of the subject, see Boolean algebra (logic). For an alternative presentation, see Boolean algebras canonically defined. In abstract …   Wikipedia

  • Robbins algebra — A Robbins algebra is an algebra consisting of the set {0,1} and the logical operations lor (disjunction, or ) and eg (negation, not ), with the following axioms:* Associativity: a lor (b lor c) = (a lor b) lor c * Commutativity: a lor b = b lor a …   Wikipedia

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • Otter (theorem prover) — Otter is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois. Otter was the first widely distributed, high performance theorem prover for first order logic, and it pioneered a number of important… …   Wikipedia

  • Аксиома Вольфрама — является результатом исследований, осуществленных Стивеном Вольфрамом[1] в поиске кратчайшей аксиомы из одного уравнения, эквивалентной аксиомам булевой алгебры (или логике высказываний). Результатом[2] его поиска стала аксиома с шестью… …   Википедия

  • 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 …   Wikipedia