Herbrand Award
Encyclopedia
The Herbrand Award for Distinguished Contributions to Automated Deduction is an award given by CADE
Conference on Automated Deduction
The Conference on Automated Deduction is the premier academic conference on automated deduction and related fields. The first CADE was organized in 1974 at the Argonne National Laboratory near Chicago. Most CADE meetings have been held in Europe and the USA. However, conferences have been held all...

 Inc. (although it predates the formal incorporation of CADE) to honour persons or groups for important contributions to the field of automated deduction
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...

. The award is named after the French
France
The French Republic , The French Republic , The French Republic , (commonly known as France , is a unitary semi-presidential republic in Western Europe with several overseas territories and islands located on other continents and in the Indian, Pacific, and Atlantic oceans. Metropolitan France...

 scientist Jacques Herbrand
Jacques Herbrand
Jacques Herbrand was a French mathematician who was born in Paris, France and died in La Bérarde, Isère, France. Although he died at only 23 years of age, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse, and Richard Courant.He...

 and given at most once per CADE or IJCAR
International Joint Conference on Automated Reasoning
International Joint Conference on Automated Reasoning is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi-regularly as a merger of other meetings. IJCAR replaces those independent conferences in the years it takes place...

 conference. It comes with an endowment of US$ 1000. Anyone can be nominated, the award is awarded after a vote among CADE trustees and former recipients, usually with input from the CADE/IJCAR programme committee.

Past recipients of the award are:
  • Larry Wos
    Larry Wos
    Larry Wos is a mathematician, a researcher in the Mathematics and Computer Science Division of Argonne National Laboratories.Wos studied at the University of Chicago, receiving a bachelor's degree in 1950 and a master's in mathematics in 1954, and went on for doctoral studies at the University of...

     (1992)
  • Woody Bledsoe
    Woody Bledsoe
    Woodrow 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...

     (1994)
  • J. Alan Robinson
    J. Alan Robinson
    John Alan Robinson is a philosopher , mathematician and computer scientist. He is University Professor Emeritus at Syracuse University, United States....

     (1996)
  • Wu Wenjun
    Wu Wenjun
    Wu Wenjun is a Chinese mathematician and academician at the Chinese Academy of Sciences .-Biography:Wu's ancestral hometown is Jiashan, in Jiaxing of Zhejiang. Wu was born in Shanghai, China where he would later graduate from Chiao Tung University in 1940...

     (1997)
  • Gérard Huet
    Gérard Huet
    Gé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....

     (1998)
  • Robert S. Boyer
    Robert S. Boyer
    Robert 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...

     and J Strother Moore
    J Strother Moore
    J 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...

     (1999)
  • William W. McCune
    William McCune
    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...

     (2000)
  • Donald W. Loveland
    Donald W. Loveland
    Donald W. Loveland was a professor emeritus of computer science at Duke University who specialized in artificial intelligence....

     (2001)
  • Mark E. Stickel (2002).
  • Peter B. Andrews (2003)
  • Harald Ganzinger
    Harald Ganzinger
    Harald 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...

     (2004)
  • Martin Davis
    Martin Davis
    Martin 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...

     (2005)
  • Wolfgang Bibel
    Wolfgang Bibel
    Wolfgang Bibel is a German scientist and one of the founders of the research area of Artificial Intelligence in Germany. Until 2004 he was the head of the intellectics research group at the computer science department of the Darmstadt University of Technology.-Career:Wolfgang Bibel was born in...

     (2006)
  • Alan Bundy
    Alan Bundy
    Alan 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....

     (2007)
  • Edmund M. Clarke
    Edmund M. Clarke
    Edmund Melson Clarke, Jr. is a computer scientist and academic noted for developingmodel checking, a method for formally verifying hardware and software designs....

     (2008)
  • Deepak Kapur (2009)
  • David Plaisted
    David Plaisted
    David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.Plaisted's research interests include term rewriting systems, automated theorem proving, logic programming, and algorithms....

     (2010)
  • Nachum Dershowitz (2011)

External links

The source of this article is wikipedia, the free encyclopedia.  The text of this article is licensed under the GFDL.
 
x
OK