The scientific organization CADE Inc., which runs the prestigious „International Conference on Automated Deduction“, has recently announced that Prof. Franz Baader, Professor of Automata Theory at the Faculty of Computer Science of TU Dresden, is this year’s winner of the renowned „Herbrand Award“.

This life-time achievement award is bestowed since 1992 on scientists that have made exceptional contributions to the field of Automated Deduction. Prof. Baader thus joins the illustrious list of former awardees, such as J.A. Robinson (inventor of the resolution principle), M. Davis (originator of the  Davis-Putnam method, on which the very successful SAT-Solvers are based), E. Clarke (co-inventor of model checking) and B. Buchberger (inventor of Gröbner-Bases). He is honored for his contributions to Unification Theory, the Combination of Logical Theories, and Description Logics.

The award is named after Jacques Herbrand, a French mathematician who unfortunately died very young. Herbrand’s doctoral thesis, which was written in the twenties of the 20^th Century, has laid the foundations for Automated Deduction. The field of Automated Deduction (also called “Automated Theorem Proving” or “Automated Reasoning”) is the subfield of Artificial Intelligence that investigates how to automate logical reasoning. Its original intention was to prove mathematical results (theorems) with the help of computer programs (so-called Theorem Provers). Although having made significant contributions to this application area, the main applications of Automated Deduction nowadays lie within Computer Science since it supports software and hardware verification, and thus contributes to the safety of computer-based systems (such as control software for airplanes and cars).

Prof. Baader´s contributions to Automated Deduction are mainly concerned with developing reasoning approaches for restricted classes of logics that are relevant for certain applications.  Such specialized deduction procedures are usually more efficient and easier to implement than general procedures, such as resolution. After obtaining his doctoral degree at the Friedrich-Alexander-Universität Erlangen-Nürnberg, he was a Senior Researcher at the German Research Center for Artificial Intelligence (DFKI) for four years, and Professor for Theoretical Computer Science at RWTH Aachen University for eight years. In 2002 he was appointed to lead the Chair of Automata Theory at TU Dresden. His research was and still is funded by the German Research Foundation (DFG) within Collaborative Research Centers (SFBs), Research Training Groups (GRKs) and stand-alone research projects. Prof. Baader is Fellow of the European Association for Artificial Intelligence (EurAI) and member of Academia Europaea.

Further information:
https://www.cadeinc.org/Herbrand-Award
https://tu-dresden.de/ing/informatik/thi/lat/die-professur/franz-baader .

Media inquiries:
Prof. Franz Baader
Faculty of Computer Science
Institute of Theoretical Computer Science
Chair of Automata Theory
Tel.: +49 351 463-39160