Automated theorem proving
Encyclopedia
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
.
, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus
, with no ("proper") axioms, Gödel's completeness theorem
states that the theorems (provable statements) are exactly the logically valid well-formed formula
s, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.
However, invalid formulas (those that are not entailed by a given theory), cannot always be recognized. In addition, a consistent formal theory that contains the first-order theory of the natural numbers (thus having certain "proper axioms"), by Gödel's incompleteness theorem, contains true statements which cannot be proven. In these cases, an automated theorem prover may fail to terminate while searching for a proof. Despite these theoretical limits, in practice, theorem provers can solve many hard problems, even in these undecidable logics.
or program, and hence the problem is always decidable.
Interactive theorem provers
require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety of tasks, but even fully automatic systems have proven a number of interesting and hard theorems, including some that have eluded human mathematicians for a long time. However, these successes are sporadic, and work on hard problems usually requires a proficient user.
Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking
, which is equivalent to brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).
There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machine-aided proof of the four color theorem
, which was very controversial as the first claimed mathematical proof which was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called non-surveyable proofs). Another example would be the proof that the game Connect Four
is a win for the first player.
, the complicated floating point unit
s of modern microprocessors have been designed with extra scrutiny. Nowadays, AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.
theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semi-decidable, and a number of sound and complete calculi have been developed, enabling fully automated systems. More expressive logics, such as higher order logics, allow the convenient expression of a wider range of problems than first order logic, but theorem proving for these logics is less well developed.
(CASC), a yearly competition of first-order systems for many important classes of first-order problems.
Some important systems (all have won at least one CASC competition division) are listed below.
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...
(AR), is the proving
Mathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
of mathematical theorems by a computer program
Computer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
.
Decidability of the problem
Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but Co-NP-completeCo-NP-complete
In complexity theory, computational problems that are co-NP-complete are those that are the hardest problems in co-NP, in the sense that they are the ones most likely not to be in P...
, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
, with no ("proper") axioms, Gödel's completeness theorem
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
states that the theorems (provable statements) are exactly the logically valid well-formed formula
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
s, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.
However, invalid formulas (those that are not entailed by a given theory), cannot always be recognized. In addition, a consistent formal theory that contains the first-order theory of the natural numbers (thus having certain "proper axioms"), by Gödel's incompleteness theorem, contains true statements which cannot be proven. In these cases, an automated theorem prover may fail to terminate while searching for a proof. Despite these theoretical limits, in practice, theorem provers can solve many hard problems, even in these undecidable logics.
Related problems
A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive functionPrimitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
or program, and hence the problem is always decidable.
Interactive theorem provers
Interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety of tasks, but even fully automatic systems have proven a number of interesting and hard theorems, including some that have eluded human mathematicians for a long time. However, these successes are sporadic, and work on hard problems usually requires a proficient user.
Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, which is equivalent to brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).
There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machine-aided proof of the four color theorem
Four color theorem
In mathematics, the four color theorem, or the four color map theorem states that, given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color...
, which was very controversial as the first claimed mathematical proof which was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called non-surveyable proofs). Another example would be the proof that the game Connect Four
Connect Four
Connect Four is a two-player game in which the players first choose a color and then take turns dropping their colored discs from the top into a seven-column, six-row vertically-suspended grid...
is a win for the first player.
Industrial uses
Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bugPentium FDIV bug
The Pentium FDIV bug was a bug in the Intel P5 Pentium floating point unit . Certain floating point division operations performed with these processors would produce incorrect results...
, the complicated floating point unit
Floating point unit
A floating-point unit is a part of a computer system specially designed to carry out operations on floating point numbers. Typical operations are addition, subtraction, multiplication, division, and square root...
s of modern microprocessors have been designed with extra scrutiny. Nowadays, AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.
First-order theorem proving
First-orderFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semi-decidable, and a number of sound and complete calculi have been developed, enabling fully automated systems. More expressive logics, such as higher order logics, allow the convenient expression of a wider range of problems than first order logic, but theorem proving for these logics is less well developed.
Benchmarks and competitions
The quality of implemented system has benefited from the existence of a large library of standard benchmark examples — the Thousands of Problems for Theorem Provers (TPTP) Problem Library — as well as from the CADE ATP System CompetitionCADE ATP System Competition
The CADE ATP System Competition is a yearly competition of fully automated theorem provers for classical first order logic. CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated...
(CASC), a yearly competition of first-order systems for many important classes of first-order problems.
Some important systems (all have won at least one CASC competition division) are listed below.
- EE theorem proverE is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem...
is a high-performance prover for full first-order logic, but built on a purely equational calculusSuperposition calculusThe superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
, developed primarily in the automated reasoning group of Technical University of MunichTechnical University of MunichThe Technische Universität München is a research university with campuses in Munich, Garching, and Weihenstephan...
. - Otter, developed at the Argonne National LaboratoryArgonne National LaboratoryArgonne National Laboratory is the first science and engineering research national laboratory in the United States, receiving this designation on July 1, 1946. It is the largest national laboratory by size and scope in the Midwest...
, is the first widely used high-performance theorem prover. It is based on first-order resolution and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4. - SETHEO is a high-performance system based on the goal-directed model eliminationModel eliminationModel Elimination is the name attached to a pair of proof procedures invented by Donald W. Loveland, the first of which was published in 1968 in the Journal of the ACM...
calculus. It is developed in the automated reasoning group of Technical University of Munich. E and SETHEO have been combined (with other systems) in the composite theorem prover E-SETHEO. - VampireVampire theorem proverVampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester byProf. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov...
is developed and implemented at Manchester University by Andrei Voronkov, formerly together with Alexandre Riazanov. It has won the "world cup for theorem provers" (the CADE ATP System Competition) in the most prestigious CNF (MIX) division for eleven years (1999, 2001–2010). - Waldmeister is a specialized system for unit-equational first-order logic. It has won the CASC UEQ division for the last fourteen years (1997–2010).
- SPASS is a first order logic theorem prover with equality. This is developed by the research group Automation of Logic, Max Planck Institute for Computer ScienceMax Planck Institute for Computer ScienceThe Max Planck Institute for Computer Science is devoted to cutting-edge research in computer science with a focus on algorithms and their applications in a broad sense...
.
Popular techniques
- First-order resolution with unification
- Lean theorem provingLean theorem proverA lean theorem prover is an automated theorem prover implemented in a minimum amount of code. Lean provers are generally implemented in Prolog, and make proficient use of the backtracking engine and logic variables of that language. Lean provers can be as small as a few hundred bytes of source...
- Model eliminationModel eliminationModel Elimination is the name attached to a pair of proof procedures invented by Donald W. Loveland, the first of which was published in 1968 in the Journal of the ACM...
- Method of analytic tableauxMethod of analytic tableauxIn proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure...
- SuperpositionSuperposition calculusThe superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
and term rewritingRewritingIn mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems... - Model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
- Mathematical inductionMathematical inductionMathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
- Binary decision diagramBinary decision diagramIn the field of computer science, a binary decision diagram or branching program, like a negation normal form or a propositional directed acyclic graph , is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed...
s - DPLLDPLL algorithmThe Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem....
- Higher-order unification
Comparison
See also: Proof assistant#Comparison and :Category:Theorem proving software systems| Name | License type | Web service | Library | Standalone | Version | Last update | Author |
|---|---|---|---|---|---|---|---|
| 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... / Mace4 |
GPLv2 | v05 | 11/2009 | William McCune / Argonne National Laboratory | |||
| Otter | Public Domain | - | 09/2004 | William McCune / Argonne National Laboratory | |||
| j'Imp | ? | - | 05/28/2010 | André Platzer | |||
| Metis | ? | 2.2 | 05/24/2010 | Joe Hurd | |||
| Jape | ? | 1.0 | 03/22/2010 | Adolfo Gustavo Neto, USP | |||
| PVS Prototype Verification System The Prototype Verification System is a specification language integrated with support tools and a theorem prover.It was developed at the Computer Science Laboratory of SRI International in California. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent... |
? | 4.2 | 07/2008 | Computer Science Laboratory of SRI International SRI International SRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later... , California, USA |
|||
| Leo II | ? | 1.2.8 | 2011 | Christoph Benzmüller, Frank Theiss, Larry Paulson. FU Berlin and University of Cambridge | |||
| 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,... |
? | 0.9e | May/2009 | William McCune / Argonne National Laboratory | |||
| SAD | ? | 2.3-2.5 | 08/27/2008 | Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich | |||
| PhoX PhoX In automated theorem proving, PhoX is a proof assistant based on higher-order logic which is eXtensible. The user gives PhoX an initial goal and guides it through subgoals and evidence to prove that goal; internally, it constructs natural deduction trees... |
? | 0.88.100524 | - | Christophe Raffalli, Philippe Curmin, Pascal Manoury, Paul Roziere | |||
| KeYmaera | ? | 1.8 | 06/04/2010 | André Platzer, Jan-David Quesel; Philipp Rümmer; David Renshaw | |||
| Gandalf | ? | 3.6 | 2009 | Matt Kaufmann e J. Strother Moore, Universidade de Texas em Austin | |||
| Tau | ? | - | 2005 | Jay R. Halcomb e Randall R. Schulz da H&S Information Systems | |||
| E E equational theorem prover E is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem... |
GPL | E 1.2 | 10/24/2010 | Stephan Schulz, Automated Reasoning Group, Technical University of Munich | |||
| SNARK SNARK theorem prover SNARK, , is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering.... |
Mozilla Public License | snark-20080805r018b | 2008 | Mark E. Stickel | |||
| Vampire/Vampyre Vampire theorem prover Vampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester byProf. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov... |
? | Third re-incarnation Vampire | 2008 | Andrei Voronkov, Alexandre Riazanov, Krystof Hoder | |||
| Waldmeister | ? | - | - | Thomas Hillenbrand, Bernd Löchner, Arnim Buch, Roland Vogt, Doris Diedrich | |||
| Saturate | ? | 2.5 | 10/1996 | Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Pilar Nivela | |||
| Theorem Proving System (TPS) | ? | - | 06/24/2004 | Carnegie Mellon University | |||
| SPASS | ? | 3.7 | 11/2005 | Max Planck Institut Informatik | |||
| IsaPlanner IsaPlanner IsaPlanner is a proof planner for the interactive proof assistant, Isabelle. Originally developed by Lucas Dixon as part of his PhD thesis at the University of Edinburgh, it is now maintained by members of the Mathematical Reasoning Group, in the School of Informatics at Edinburgh.IsaPlanner is... |
GPL | IsaPlanner 2 | 2007 | Lucas Dixon, Johansson Moa | |||
| KeY KeY The KeY tool is used in formal verification of Java programs.It accepts both specifications written in JML or OCL to Java source files. These are transformed into theorems of dynamic logic and then compared against program semantics which are likewise defined in terms of dynamic logic. KeY is... |
GPL | 1.6 | 10/2010 | Karlsruhe Institute of Technology Karlsruhe Institute of Technology The Karlsruhe Institute of Technology is a German academic research and education institution with university status resulting from a merger of the university and the research center of the city of Karlsruhe. The university, also known as Fridericiana, was founded in 1825... , Chalmers University of Technology Chalmers University of Technology Chalmers University of Technology , is a Swedish university located in Gothenburg that focuses on research and education in technology, natural science and architecture.-History:... , University of Koblenz |
|||
| ACL2 | ? | 4.1 | 09/2010 | Matt Kaufmann, J. Strother Moore | |||
| Theorem Checker | ? | 0 | 2010 | Robert J. Swartz, Northeastern Illinois University | |||
Free software
- Alt-Ergo
- Automath
- CVC
- Gödel-machines
- iProver
- IsaPlannerIsaPlannerIsaPlanner is a proof planner for the interactive proof assistant, Isabelle. Originally developed by Lucas Dixon as part of his PhD thesis at the University of Edinburgh, it is now maintained by members of the Mathematical Reasoning Group, in the School of Informatics at Edinburgh.IsaPlanner is...
- KED theorem prover
- LCF
- LoTREC
- MetaPRL
- NuPRLNuPRLNuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL....
- Paradox
Proprietary Software
- Acumen RuleManager (commercial product)
- ALLIGATOR
- CARINECarineCarine may refer to* Carine, Western Australia, a suburb of Perth* some species of owls, including** Little Owl ** Rodrigues Owl * Guzmania 'Carine', a Bromeliad hybrid cultivar...
- KIV
- Prover Plug-In (commercial proof engine product)
- ProverBox
- ResearchCyc
- Simplify
- SPARK (programming language)
- Spear modular arithmetic theorem prover
- TwelfTwelfTwelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.-Introduction:...
Notable people
- Leo Bachmair, co-developer of the superposition calculusSuperposition calculusThe superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
. - Woody BledsoeWoody BledsoeWoodrow Wilson "Woody" Bledsoe was a mathematician, computer scientist, and prominent educator. He is one of the pioneers of artificial intelligence, pattern recognition, and automated theorem proving...
, artificial intelligenceArtificial intelligenceArtificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
pioneer. - Robert S. BoyerRobert S. BoyerRobert Stephen Boyer, aka Bob Boyer, is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore...
, co-author of the Boyer-Moore theorem proverNqthmNqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.- History :The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas, Austin. They began work on the system in 1971 in...
, co-recipient of the Herbrand AwardHerbrand AwardThe Herbrand Award for Distinguished Contributions to Automated Deduction is an award given by CADE Inc. to honour persons or groups for important contributions to the field of automated deduction. The award is named after the French scientist Jacques Herbrand and given at most once per CADE or...
1999. - Alan BundyAlan BundyAlan Bundy, FRSE, FBCS, FAAAI, FECCAI, FAISB, is a professor at the School of Informatics at the University of Edinburgh, known for his contributions to automated reasoning, especially to proof-planning, the use of meta-level reasoning to guide proof search....
, University of EdinburghUniversity of EdinburghThe University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
, meta-level reasoning for guiding inductive proof, proof planning and recipient of 2007 IJCAI Award for Research ExcellenceIJCAI Award for Research ExcellenceThe IJCAI Award for Research Excellence is a biannual award given at the IJCAI conference to researcher in artificial intelligence as a recognition of excellence of their career...
, Herbrand Award, and 2003 Donald E. Walker Distinguished Service Award. - William McCune Argonne National Laboratory, author of Otter, the first high-performance theorem prover. Many important papers, recipient of the Herbrand Award 2000.
- Hubert Comon, CNRS and now ENS Cachan. Many important papers.
- Robert Lee ConstableRobert Lee ConstableRobert "Bob" Lee Constable is a professor of computer science and first and former dean of the department at Cornell University. He is known for his work on connecting computer programs and mathematical proofs, especially the NuPRL system. Constable received his PhD in 1968 under Stephen Kleene and...
, Cornell University. Important contributions to type theory, NuPRL. - Martin DavisMartin DavisMartin David Davis, is an American mathematician, known for his work on Hilbert's tenth problem . He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church . He is Professor Emeritus at New York University. He is the co-inventor of the Davis-Putnam and the DPLL...
, author of the "Handbook of Artificial Reasoning", co-inventor of the DPLL algorithmDPLL algorithmThe Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem....
, recipient of the Herbrand Award 2005. - Branden Fitelson University of California at Berkeley. Work in automated discovery of shortest axiomatic bases for logic systems.
- Harald GanzingerHarald GanzingerHarald Ganzinger was a German computer scientist that together with Leo Bachmair developed the superposition calculus, which is used in most of the state-of-the-art automated theorem provers for first-order logic.He received his Ph.D. from the Technical University of Munich in 1978...
, co-developer of the superposition calculus, head of the MPI Saarbrücken, recipient of the Herbrand Award 2004 (posthumous). - Michael Genesereth, Stanford UniversityStanford UniversityThe Leland Stanford Junior University, commonly referred to as Stanford University or Stanford, is a private research university on an campus located near Palo Alto, California. It is situated in the northwestern Santa Clara Valley on the San Francisco Peninsula, approximately northwest of San...
professor of Computer Science. - Keith Goolsbey chief developer of the CycCycCyc is an artificial intelligence project that attempts to assemble a comprehensive ontology and knowledge base of everyday common sense knowledge, with the goal of enabling AI applications to perform human-like reasoning....
inference engine. - Michael J. C. GordonMichael J. C. GordonMichael John Caldwell Gordon, British computer scientist .Mike Gordon led the development of the HOL theorem prover. The HOL system is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language...
led the development of the HOL theorem prover. - Gérard HuetGérard HuetGérard Pierre Huet is a French computer scientist.- Biography :Gérard Huet graduated from the Université Denis Diderot , Case Western Reserve University, and the Université de Paris....
Term rewriting, HOL logics, Herbrand Award 1998. - Robert KowalskiRobert KowalskiRobert "Bob" Anthony Kowalski is a British logician and computer scientist, who has spent most of his career in the United Kingdom....
developed the connection graph theorem-prover and SLD resolutionSLD resolutionSLD resolution is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.-The SLD inference rule:...
, the inference engine that executes logic programsLogic programmingLogic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
. - Donald W. Loveland Duke University. Author, co-developer of the DPLL-procedure, developer of model eliminationModel eliminationModel Elimination is the name attached to a pair of proof procedures invented by Donald W. Loveland, the first of which was published in 1968 in the Journal of the ACM...
, recipient of the Herbrand Award 2001. - Norman Megill, developer of MetamathMetamathMetamath is a computer-assisted proof checker. It has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas...
, and maintainer of its site at metamath.org, an online database of automatically verified proofs. - J Strother MooreJ Strother MooreJ Strother Moore is a computer scientist, and he is a co-developer of the Boyer–Moore string search algorithm and the Boyer–Moore automated theorem prover, Nqthm. An example of the workings of the Boyer–Moore string search algorithm is given...
, co-author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999. - Robert Nieuwenhuis University of Barcelona. Co-developer of the superposition calculus.
- Tobias Nipkow of the Technical University of MunichTechnical University of MunichThe Technische Universität München is a research university with campuses in Munich, Garching, and Weihenstephan...
, contributions to (higher-order) rewriting, co-developer of the Isabelle proof assistant - Ross OverbeekRoss OverbeekRoss A. Overbeek is an American computer scientist with a long tenure at the Argonne National Laboratory. He has made important contributions to mathematical logic and genomics, as well as programming, particularly in database theory and the programming language Prolog.- Early life :He grew up in...
Argonne National Laboratory. Founder of The Fellowship for Interpretation of Genomes - Lawrence C. Paulson of the University of CambridgeUniversity of CambridgeThe University of Cambridge is a public research university located in Cambridge, United Kingdom. It is the second-oldest university in both the United Kingdom and the English-speaking world , and the seventh-oldest globally...
, work on higher-order logic system, co-developer of the IsabelleIsabelle theorem proverThe Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...
Theorem Prover - David A. Plaisted University of North Carolina at Chapel HillUniversity of North Carolina at Chapel HillThe University of North Carolina at Chapel Hill is a public research university located in Chapel Hill, North Carolina, United States...
. Complexity results, contributions to rewritingRewritingIn mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
and completionKnuth-Bendix completion algorithmThe Knuth–Bendix completion algorithm is an algorithm for transforming a set of equations into a confluent term rewriting system...
, instance-based theorem proving. - John RushbyJohn RushbyJohn Rushby is a British computer scientist now based in the United States.John Rushby was born and brought up in London, where he attended Dartford Grammar School. He studied at the University of Newcastle in the UK, gaining his computer science BSc there in 1971 and his PhD in 1977.From 1974 to...
Program Director - SRI InternationalSRI InternationalSRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later... - J. Alan Robinson Syracuse University. Developed original resolution and unification based first order theorem proving, co-editor of the "Handbook of Automated Reasoning", recipient of the Herbrand Award 1996
- Jürgen SchmidhuberJürgen SchmidhuberJürgen Schmidhuber is a computer scientist and artist known for his work on machine learning, universal Artificial Intelligence , artificial neural networks, digital physics, and low-complexity art. His contributions also include generalizations of Kolmogorov complexity and the Speed Prior...
Work on Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements - Stephan Schulz, E theorem Prover.
- Natarajan ShankarNatarajan ShankarNatarajan Shankar is a computer scientist working at SRI International, California.His PhD thesis was published as the book " Metamathematics, Machines, and Goedel's Proof" by Cambridge University Press in 1994. He has used the Boyer–Moore theorem prover to prove metatheorems such as the tautology...
SRI International, work on decision procedures, little engines of proof, co-developer of PVSPrototype Verification SystemThe Prototype Verification System is a specification language integrated with support tools and a theorem prover.It was developed at the Computer Science Laboratory of SRI International in California. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent...
. - Mark Stickel SRI International. Recipient of the Herbrand Award 2002.
- Geoff SutcliffeGeoff SutcliffeGeoff Sutcliffe is a US-based computer scientist working in the field of automated reasoning.He is of both British and Australian nationality.He was born in the former British colony of Northern Rhodesia ,...
University of Miami. Maintainer of the TPTP collection, an organizer of the CADE annual contest. - Dolph Ulrich Purdue, Work on automated discovery of shortest axiomatic bases for systems.
- Robert Veroff University of New Mexico. Many important papers.
- Andrei Voronkov Developer of Vampire and Co-Editor of the "Handbook of Automated Reasoning"
- Larry Wos Argonne National Laboratory. (Otter) Many important papers. Very first Herbrand Award winner (1992)
- Wen-Tsun Wu Work in geometric theorem proving: Wu's method, Herbrand Award 1997
- Christoph Weidenbach, author of SPASS, automated theorem prover.