Automated Theorem Proving - Notable People

Notable People

• Leo Bachmair, co-developer of the superposition calculus.
• Woody Bledsoe, artificial intelligence pioneer.
• Robert S. Boyer, co-author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999.
• Alan Bundy, University of Edinburgh, meta-level reasoning for guiding inductive proof, proof planning and recipient of 2007 IJCAI Award for Research Excellence, 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 Constable, Cornell University. Important contributions to type theory, NuPRL.
• Martin Davis, author of the "Handbook of Artificial Reasoning", co-inventor of the DPLL algorithm, 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 Ganzinger, co-developer of the superposition calculus, head of the MPI Saarbrücken, recipient of the Herbrand Award 2004 (posthumous).
• Michael Genesereth, Stanford University professor of Computer Science.
• Keith Goolsbey chief developer of the Cyc inference engine.
• Michael J. C. Gordon led the development of the HOL theorem prover.
• Gérard Huet Term rewriting, HOL logics, Herbrand Award 1998.
• Robert Kowalski developed the connection graph theorem-prover and SLD resolution, the inference engine that executes logic programs.
• Donald W. Loveland Duke University. Author, co-developer of the DPLL-procedure, developer of model elimination, recipient of the Herbrand Award 2001.
• Norman Megill, developer of Metamath, and maintainer of its site at metamath.org, an online database of automatically verified proofs.
• J Strother Moore, 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 Munich, contributions to (higher-order) rewriting, co-developer of the Isabelle proof assistant
• Ross Overbeek Argonne National Laboratory. Founder of The Fellowship for Interpretation of Genomes
• Lawrence C. Paulson of the University of Cambridge, work on higher-order logic system, co-developer of the Isabelle Theorem Prover
• David A. Plaisted University of North Carolina at Chapel Hill. Complexity results, contributions to rewriting and completion, instance-based theorem proving.
• John Rushby Program Director - SRI International
• 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 Schmidhuber Work on Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements
• Stephan Schulz, E theorem Prover.
• Natarajan Shankar SRI International, work on decision procedures, little engines of proof, co-developer of PVS.
• Mark Stickel SRI International. Recipient of the Herbrand Award 2002.
• Geoff Sutcliffe 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.