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.
See the citations and photographs below.
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, along with two other letters (up to 2000 words) of endorsement. The nomination of a group of individuals who are collaborators is considered to be a single nomination. Current members of the board of trustees of CADE Inc. are not 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:
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.
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.
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.
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.
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.
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.
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.
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.
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.
in recognition of his role aspresented atand his numerous other contribution to the field.
- 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;
CADE-20
The Twentieth International Conference on Automated Deduction
July 26, 2005
Franz Baader
President of CADE Inc.
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.
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.
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 reasoningpresented at
CADE-18
The Eighteenth International Conference on Automated Deduction
July 29, 2002
Ulrich Furbach
President of CADE Inc.
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.
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.
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.
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.
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
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
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
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
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.
