Die Fachvereinigung CADE Inc., Organisatorin der angesehenen „International Conference on Automated Deduction“, gab jetzt bekannt, dass Prof. Franz Baader, Inhaber der Professur Automatentheorie an der Fakultät Informatik der TU Dresden, der renommierten „Herbrand Award“ verliehen wird.

Dieser seit 1992 vergebene Preis ehrt Wissenschaftler, die herausragende Leistungen im Gebiet der automatisierten Deduktion erbracht haben, für ihr Lebenswerk. Prof. Baader reiht sich damit in die illustre Liste der bisherigen Preisträger ein, wie zum Beispiel J.A. Robinson (Erfinder des Resolutionsverfahrens), M. Davis (Erfinder des Davis-Putnam-Verfahrens, auf dem die äußerst erfolgreichen SAT-Solver beruhen), E. Clarke (Erfinder des Model Checking) und B. Buchberger (Erfinder der Gröbner-Basen). Er wird für seine Beiträge zur Unifikationstheorie, der Kombination logischer Theorien und der Beschreibungslogiken geehrt.

Der Preis ist nach Jaques Herbrand benannt, einem leider sehr jung verstorbenen französischen Mathematiker, der in den 20er Jahren des 20. Jahrhunderts in seiner Dissertationsschrift wesentliche Grundlagen für die automatisierte Deduktion gelegt hat. Das Gebiet der automatisierten Deduktion (auch automatisiertes Theorembeweisen genannt) ist ein Teilgebiet der Künstlichen Intelligenz, das die Automatisierung des logischen Schließens erforscht. Die ursprüngliche Intention war hier, mathematische Resultate (Theoreme) mit Hilfe von Computerprogrammen (sogenannten Theorembeweisern) zu beweisen. Obwohl das Gebiet auch in diesem Anwendungsbereich beachtliche Erfolge erzielt hat, liegen die Hauptanwendungen der automatisierten Deduktion aber derzeit in der Informatik, da sie die Verifikation von Hard- und Software unterstützt und damit wesentlich zur Sicherheit computerbasierter Systeme (wie z.B. Steuersoftware für Flug- und Kraftfahrzeugen) beiträgt.

Prof. Baaders Beiträge in der automatisierten Deduktion beschäftigen sich hauptsächlich damit, für eingeschränkte, aber anwendungsrelevante Klassen von Logiken spezialisierte Deduktionsverfahren zu entwickeln, welche effizienter sind als allgemeine Verfahren, wie z.B. Resolution. Nach seiner Promotion an der Friedrich-Alexander-Universität Erlangen-Nürnberg war er vier Jahre Senior Researcher am Deutschen Forschungszentrum für Künstliche Intelligenz (DFKI) und acht Jahre Professor für Theoretische Informatik an der RWTH Aachen, bevor er 2002 auf die Professur Automatentheorie an der TU Dresden berufen wurde. Seine Forschung wurde und wird durch die DFG im Rahmen von Sonderforschungsbereichen, Graduiertenkollegs und Normalverfahrensprojekten gefördert. Prof. Baader ist Fellow der European Association for Artificial Intelligence (EurAI) und Mitglied der Academia Europaea.

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

Informationen für Journalisten:
Prof. Franz Baader
Fakultät Informatik
Institut für Theoretische Informatik
Lehrstuhl für Automatentheorie
Tel.: +49 351 463-39160