In 1992 CADE Inc. established the Herbrand Award for Distinguished Contributions to Automated Reasoning, to honor an individual or (a group of) individuals for exceptional contributions to the field of Automated Deduction. Nominations for this award can be made at any time to the president of CADE Inc.

Winners


Procedure

The Herbrand award procedure (established 1992, amended 2001) has three stages: nomination; advisory voting by trustees, current PC and past winners; and final decision by the trustees. In this procedure, “worthiness” is separated from “ranking”. The CADE president is responsible for soliciting opinions and evaluations, and carrying out a vote. Nominations for this award can be made at any time to the president of CADE Inc. A nomination should include a letter (up to 2000 words) from a principal nominator describing the nominee’s contributions (including the relationship to CADE), along with two other letters (up to 2000 words) of endorsement. Current members of the board of trustees of CADE Inc. (including ex-officio members) are not eligible. The nomination of a group of individuals who are collaborators is considered to be a single nomination, but all members of the group must be eligible. Nominations will be kept confidential.

The current conference program committee, the award winners from the last 10 years, and the current board of trustees of CADE, Inc. will participate in the selection, with the final decision resting with the board of trustees. The award will be given at the CADE or IJCAR conference, whichever is scheduled for the year. The selection procedure will work as follows. The members of the current program program committee, winners from the past 10 years, and trustees are invited to express express their opinions on the nominees in two ways:

They indicate which candidates they believe are worthy of the award. They give a preferential ranking of all the candidates. It is expected that only those receiving an endorsement by a 2/3 majority under vote (1) will be considered by the trustees for the award. A preferred majority candidate will be selected by the single transferrable vote principle using the referential ranking (2). After possible further discussion among the trustees, the president of CADE proposes a candidate which should be endorsed in a final vote by 2/3 of the trustees. It is expected that in most cases this should be the majority candidate from the advisory vote.

Citations


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Bruno Buchberger

for the invention, implementation, and analysis of the Gröbner-basis method, resulting in the reshaping of symbolic computation towards comprehensive and widely applicable tools.

Presented at IJCAR 2018, the 9th International Joint Conference on Automated Reasoning July, 2018.

Christoph Weidenbach President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Lawrence C. Paulson

for his pioneering contributions to the automation in proof assistants and the foundations of formal security protocol verification as well as his impressive formalizations of deep mathematical theories.

Presented at CADE-26, the 26th International Conference on Automated Deduction.

Christoph Weidenbach President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Zohar Manna

for his pioneering research and pedagogical contributions (with Richard Waldinger) to automated reasoning, program synthesis, planning, and formal methods.

Presented at IJCAR 2016, the 8th International Joint Conference on Automated Reasoning June, 2016

Maria Paola Bonacina President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Richard Waldinger Acceptance Speech

for his pioneering research and pedagogical contributions (with Zohar Manna) to automated reasoning, program synthesis, planning, and formal methods.

Presented at IJCAR 2016, the 8th International Joint Conference on Automated Reasoning June, 2016.

Maria Paola Bonacina President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Andrei Voronkov

in recognition of his numerous theoretical and practical contributions to automated deduction, and the development of the award-winning Vampire theorem prover.

Presented at CADE-25 The 25th International Conference on Automated Deduction August, 2015

Maria Paola Bonacina President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Robert L. Constable Acceptance Speech

in recognition of his pioneering research in automated reasoning, including his seminal contributions to the foundations of computational type theory, the creation of Nuprl - the first constructive type theory based theorem prover - the development of the correct-by-construction programming paradigm, and their applications to verification and synthesis of computer systems, including distributed computing.

Presented at IJCAR 2014 The 7th International Joint Conference on Automated Reasoning July, 2014

Maria Paola Bonacina President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Greg Nelson

for his pioneering contributions to theorem proving and program verification, such as his seminal work with Derek Oppen on the combination of satisfiability procedures and fast congruence closure algorithms, the development of the highly influential theorem prover Simplify, and his role in the creation of the field of extended static checking.

Presented at CADE-24 The 24th International Conference on Automated Deduction June, 2013

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Melvin C. Fitting Acceptance Speech

in recognition of his outstanding contributions to tableau-based theorem proving in classical and non-classical logics, as well as to many other areas of Automated Reasoning, Logic Programming, and Philosophical Logic.

Presented at IJCAR 2012 The 6th International Joint Conference on Automated Reasoning June 26, 2012

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Nachum Dershowitz Acceptance Speech

in recognition of his ground-breaking research on the design and use of well-founded orderings in term rewriting and automated deduction.

Presented at CADE 2011 The 23rd International Conference on Automated Deduction August 2, 2011

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


David A. Plaisted Acceptance Speech

in recognition of his numerous seminal contributions to several areas of automated reasoning, including first-order theorem proving, term rewriting, completion, orderings, inductive reasoning, and pioneering research on abstraction, instance-based methods and search complexity in theorem proving.

Presented at IJCAR 2010 The 5th International Joint Conference on Automated Reasoning July 19, 2010

Maria Paola Bonacina President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Deepak Kapur

in recognition of of his seminal contributions to several areas of automated deduction including inductive theorem proving, geometry theorem proving, term rewriting, unification theory, integration and combination of decision procedures, lemma and loop invariant generation, as well as his work in computer algebra, which helped to bridge the gap between the two areas.

Presented at CADE-22 The 22nd International Conference on Automated Deduction August 5, 2009

Reiner Hähnle Vice-president of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Edmund M. Clarke

in recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades.

Presented at IJCAR 2008 The 4th International Joint Conference on Automated Reasoning August 13, 2008

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Alan Bundy Acceptance Speech

in recognition of his outstanding contributions to proof planning and inductive theorem proving, as well as to many other areas of Automated Reasoning and Artificial Intelligence.

Presented at CADE-21 The 21st International Conference on Automated Deduction July 17, 2007

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Wolfgang Bibel Acceptance Speech

in recognition of his seminal work on first order theorem proving and its applications in Artificial Intelligence and Programming. His research on the connection method laid the foundations for many modern deduction systems, and it had signifcant influence on other research areas such as Logic Programming, Knowledge Representation, and Deductive Planning.

Presented at IJCAR 2006 The International Joint Conference on Automated Reasoning August 19, 2006

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Martin Davis

in recognition of his role as a founding father of the field of automated reasoning; coauthor of both papers that introduce what is now called the Davis-Putnam or Davis-Putnam-Logemann-Loveland procedure, variants of one of the most outstanding and useful proof procedures known today; historian regarding the early history of the field of automated deduction; and his numerous other contribution to the field.

Presented at CADE-20 The Twentieth International Conference on Automated Deduction July 26, 2005

Franz Baader President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Harald Ganzinger

in recognition of his seminal work on the theory underlying modern theorem proving systems; the breadth of his research covering nearly all major areas of deduction, and the depth of his results in each one of them; his effective contributions to the development of systems and implementation techniques; and his dedicated promotion of automated reasoning both inside and outside the community.

Presented at IJCAR-2004 The 2nd International Joint Conference on Automated Reasoning July 2004

Frank Pfenning President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Peter Andrews Acceptance Speech

for his seminal contributions and pioneering research in type theory, mating-based theorem proving, automated deduction in higher-order logic, proof presentation, logic education, and many other contributions to the field of automated reasoning. presented at CADE-19 The Nineteenth International Conference on Automated Deduction August 1, 2003

Ulrich Furbach President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Mark E. Stickel

for his ground-breaking discoveries in AC-unification, reasoning modulo a theory, term indexing, and thorough development of the SNARK and PTTP provers, as well as many other contributions to the field of automated reasoning presented at CADE-18 The Eighteenth International Conference on Automated Deduction July 29, 2002

Ulrich Furbach President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Donald Loveland

for his development of the model elimination procedure, for his contributions to propositional satisfiability testing realized in the Davis-Putman-Logemann-Loveland-Procedure, for his work on the nearHorn-Prolog family of calculi for disjunctive logic programming, and many other contributions to the field of automated reasoning.

Presented at IJCAR-2001 The First International Joint Conference on Automated Reasoning June 19, 2001

Ulrich Furbach President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


William W. McCune

for his development of powerful and portable automated deduction tools, including ITP, LMA, OTTER, ROO, MACE and EQP, and for creative new strategies and rules associated with them. His solution of the Robbins Algebra problem using EQP has brought visibility and distinction to the field.

Presented at CADE-17 The Seventeenth International Conference on Automated Deduction June 18, 2000

Ulrich Furbach President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Robert S. Boyer

for his work (with J Strother Moore) on the automation of inductive inference and its application to the verification of hardware and software.

Presented at CADE-16 The Sixteenth International Conference on Automated Deduction July 7, 1999

John Slaney President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


J Strother Moore

for his work (with Robert S. Boyer) on the automation of inductive inference and its application to the verification of hardware and software.

Presented at CADE-16 The Sixteenth International Conference on Automated Deduction July 7, 1999

John Slaney President of CADE Inc.


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Gérard Huet

for his contributions to term rewriting and to theorem proving in higher-order logic, and many other contributions to the field of automated reasoning.

Presented at CADE-15 The 15-th International Conference on Automated Deduction July, 1998

John Slaney President of CADE Inc


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Wen-Tsun Wu

for groundbreaking work in geometric theorem proving and many other contributions to the field of automated reasoning.

Presented at CADE-14 The 14-th International Conference on Automated Deduction July, 1997

John Slaney President of CADE Inc


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


John Alan Robinson

for the invention of the resolution inference rule and many other contributions to the field of automated reasoning. presented at CADE-13 The Thirteenth International Conference on Automated Deduction Tuesday, July 30, 1996

Alan Bundy President of CADE Inc


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Woody Bledsoe

for his numerous contributions to the field of Automated Deduction including natural proof systems, interactive systems, decision procedures, analogical reasoning and applications to set theory, analysis and program verification.

Presented at CADE-12 The Twelfth International Conference on Automated Deduction June/July, 1994

Larry Wos President of CADE Inc


The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning presented to


Larry Wos

Larry Wos received the first Herbrand award in automated deduction, presented at the 1992 Conference on Automated Deduction. He was recognized for his contributions to the field, as well as for his leadership in the area of automated reasoning.