The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the

Conference on Automated Deduction The Conference on Automated Deduction (CADE) 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 Eur ...

(CADE), 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 (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

. The award is named after the French scientist

Jacques Herbrand Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Cour ...

and given at most once per CADE or

International Joint Conference on Automated Reasoning The International Joint Conference on Automated Reasoning (IJCAR) 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 replace ...

(IJCAR). It comes with a prize of US$1,000. 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.

Recipients

Past award recipients are:

1990s

Larry Wos Lawrence T. Wos (1930–2020) was an American mathematician, a researcher in the Mathematics and Computer Science Division of Argonne National Laboratory. Biography Wos studied at the University of Chicago, receiving a bachelor's degree in 1950 ...

(1992) *

Woody Bledsoe Woodrow Wilson "Woody" Bledsoe (November 12, 1921 – October 4, 1995) was an American mathematician, computer scientist, and prominent educator. He is one of the founders of artificial intelligence (AI), making early contributions in pattern r ...

(1994) *

John Alan Robinson John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University. Alan Robinson's major contribution is to the foundations of automated theorem pr ...

(1996) *

Wu Wenjun Wu Wenjun ( zh, s=吴文俊; 12 May 1919 – 7 May 2017), also commonly known as Wu Wen-tsün, was a Chinese mathematician, historian, and writer. He was an academician at the Chinese Academy of Sciences (CAS), best known for the Wu's method of ...

(1997) *

Gérard Huet Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and ...

(1998) *

Robert S. Boyer Robert Stephen Boyer is an American 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 efficie ...

and

J Strother Moore J Strother Moore (his first name is the alphabetic character "J" – not an abbreviated "J.") is a computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moo ...

(1999)

2000s

* William W. McCune (2000) * Donald W. Loveland (2001) * Mark E. Stickel (2002). *

Peter B. Andrews Peter Bruce Andrews (born 1937) is an American mathematician and Professor of Mathematics, Emeritus at Carnegie Mellon University in Pittsburgh, Pennsylvania, and the creator of the mathematical logic Q0. He received his Ph.D. from Princeton Uni ...

(2003) *

Harald Ganzinger Harald Ganzinger (31 October 1950, Werneck – 3 June 2004, Saarbrücken) was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is (as of 2007) used in most of the state-of-the-art automated ...

(2004) * Martin Davis (2005) *

Wolfgang Bibel Leonhard Wolfgang Bibel (born on 28 October 1938 in Nuremberg) is a German computer scientist, mathematician and Professor emeritus at the Department of Computer Science of the Technische Universität Darmstadt. He was one of the founders of the re ...

(2006) *

Alan Bundy Alan Richard Bundy is a professor at the School of Informatics at the University of Edinburgh,http://homepages.inf.ed.ac.uk/bundy/ Professor Alan Bundy's website known for his contributions to automated reasoning, especially to proof planning ...

(2007) *

Edmund M. Clarke Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor ...

(2008) * Deepak Kapur (2009)

2010s

* David Plaisted (2010) *

Nachum Dershowitz Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems. He obtained his B.Sc. summa cum laude in 1974 in Computer Scie ...

(2011) *

Melvin Fitting Melvin Fitting (born January 24, 1942) is a logician with special interests in philosophical logic and tableau proof systems. He was a professor at City University of New York, Lehman College and the Graduate Center. from 1968 to 2013. At the ...

(2012) * C. Greg Nelson (2013) * Robert L. Constable (2014) *

Andrei Voronkov Andrei Anatolievič Voronkov (born 1959) is a Professor of Formal methods in the Department of Computer Science at the University of Manchester. Education Voronkov was educated at Novosibirsk State University, graduating with a PhD in 1987. Res ...

(2015) *

Zohar Manna Zohar Manna (1939 – 30 August 2018) was an Israeli-American computer scientist who was a professor of computer science at Stanford University. Biography He was born in Haifa, Israel. He earned his Bachelor of Science (BS) and Master of Scienc ...

and

Richard Waldinger Richard Jay Waldinger is a computer science researcher at SRI International's Artificial Intelligence Center (where he has worked since 1969) whose interests focus on the application of automated deductive reasoning to problems in software enginee ...

(2016) * Lawrence C. Paulson (2017) *

Bruno Buchberger Bruno Buchberger (born 22 October 1942) is Professor of Computer Mathematics at Johannes Kepler University in Linz, Austria. In his 1965 Ph.D. thesis, he created the theory of Gröbner bases, and has developed this theory throughout his career. ...

(2018) * Nikolaj Bjørner and Leonardo de Moura (2019)

2020s

Franz Baader Franz Baader (15 June 1959, Spalt) is a German computer scientist at Dresden University of Technology. He received his PhD in Computer Science in 1989 from the University of Erlangen-Nuremberg, Germany, where he was a teaching and research assist ...

(2020) *

Tobias Nipkow Tobias Nipkow (born 1958) is a German computer scientist. Career Nipkow received his Diplom (MSc) in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of ...

(2021) *

Natarajan Shankar Natarajan Shankar is a computer scientist working at SRI International in Menlo Park, California, where he leads the Symbolic Analysis Laboratory. Education Shankar received his Ph.D. degree in computer science, under advisors Robert S. Boyer an ...

(2022)

External links