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.

Read more about this topic:  Automated Theorem Proving

Famous quotes containing the words notable and/or people:

    “Every notable advance in technique or organization has to be paid for, and in most cases the debit is more or less equivalent to the credit. Except of course when it’s more than equivalent, as it has been with universal education, for example, or wireless, or these damned aeroplanes. In which case, of course, your progress is a step backwards and downwards.”
    —Aldous Huxley (1894–1963)

    “The appeal of the New Right is simply that it seems to promise that nothing will change in the domestic realm. People are terrified of change there, because it’s the last humanizing force left in society, and they think, correctly, that it must be retained.”
    —Gerda Lerner (b. 1920)