Professoren: Klaus Keimel; Ulrich Kohlenbach; Martin Otto; Thomas Streicher; Martin Ziegler;

Apl. Professoren: Christian Herrmann; Thomas Ihringer

Emeritierte und entpflichtete Professoren: Peter Burmeister; Rudolf Wille

Die Arbeitsgruppe repräsentiert die Mathematische Logik als angewandte Grundlagendisziplin zwischen Mathematik und Informatik. Die Forschungsaktivitäten konzentrieren sich auf die Anwendungen beweistheoretischer, rekursionstheoretischer, kategorieller, algebraischer und modelltheoretischer Methoden der Logik in Mathematik und Informatik.

Neben der klassischen Mathematischen Logik (Beweistheorie, Rekursionstheorie, Modelltheorie) spielen hier konstruktive und kategorielle Logik, Funktional- und Realisierbarkeitsinterpretationen, allgemeine Algebra, Domaintheorie, Verbandstheorie, endliche Modelltheorie und algorithmische Fragestellungen eine wesentliche Rolle.

Innermathematische Anwendungen der Beweis- und Rekursionstheorie (Kohlenbach) betreffen die Extraktion neuer Informationen aus Beweisen in Algebra, Funktionalanalysis, hyperbolischer Geometrie und numerischer Mathematik (Proof Mining). Dabei geht es sowohl um qualitative Aspekte (etwa die Unabhängigkeit von Existenzaussagen von gewissen Parametern) wie auch quantitative Aspekte der Berechenbarkeit und Komplexität von Lösungen (Extraktion von Algorithmen und Schranken aus Beweisen, exakte reelle Arithmetik, "computational mathematics": Kohlenbach, Streicher, Ziegler). Modelltheoretische Methoden (Herrmann, Otto) haben innermathematische Anknüpfungen in der Algebra und diskreten Mathematik (Ihringer).

Hinsichtlich der Logik in der Informatik und den mathematischen Grundlagen der Informatik stehen Aspekte der Semantik im Vordergrund. Darunter fällt einerseits die mathematische Grundlegung der Semantik und Logik von Programmiersprachen (Keimel, Streicher); andererseits die Analyse von Logiken von formalen Systemen im Sinne der modelltheoretischen Semantik, d.h. Untersuchungen zur Ausdruckstärke und Definierbarkeit, besonders auch unter algorithmischen Gesichtspunkten (algorithmische Modelltheorie, endliche Modelltheorie: Otto). Komplexität wird untersucht vom Blickwinkel funktionaler Programme aus (Implicit Computational Complexity: Kohlenbach), im deskriptiven Sinne (Otto) sowie ressourcen-orientiert und strukturell (Laufzeit, Speicherplatz, informationstheoretisch und topologisch: Ziegler). Neben speziellen Anwendungsfeldern in der Informatik, wie etwa Verifikation, Datenbanken und Wissensrepräsentation, werden Grundlagenfragen im Bereich der Berechenbarkeit und Komplexität, sowie der Typentheorie und Kategorientheorie bearbeitet.

Insgesamt bildet die Arbeitsgruppe einen international stark vernetzten Forschungsknoten, der sich durch die starke Betonung der vielfältigen Außenbeziehungen auszeichnet. Dies betrifft die Beziehungen sowohl zu anderen Bereichen der Mathematik als auch zur Informatik im internationalen Logic in Computer Science Spektrum.

Forschungsgruppe Begriffsanalyse: Auf der Grundlage der Ordnungs- und Verbandstheorie wird in der Forschungsgruppe der früheren AG1 (Allgemeine Algebra und diskrete Mathematik) vornehmlich die angewandte Seite der Formalen Begriffsanalyse mit einem Forschungsprogramm zu graphischen Logiksystemen in der Begrifflichen Wissensverarbeiteng verfolgt (Burmeister, Wille). Dieses Engagement wird in Kooperation mit dem ErnstSchröderZentrum für Begriffliche Wissensverarbeitung weiterbetrieben.

Kooperationen/Projekte
EU-Working Group APPSEM II (APPLIED SEMANTICS)
CCA (Computability and Complexity in Analysis)
MAP (Mathematics, Algorithms and Proofs)
Algorithmische Modelltheorie (Aachen/Berlin/Freiburg/Mainz/Marburg)
EPSRC project: Algorithmic Model Theory for Specific Domains (Otto)
ErnstSchröderZentrum, NaviCon