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). Modelltheoretische Methoden (Herrmann, Otto) haben innermathematische Anknüpfungen in der Algebra und diskreten Mathematik.

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 (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 wie auch resourcen-orientiert und strukturell (Otto). 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.

Algorithmic model theory uses tools from mathematical logic to answer model-theoretic questions that arise from algorithmic issues in discrete mathematical structures and in the modelling of data, information and computation.

As a branch of mathematical logic, model theory is generally concerned with the study of

  • definability and the expressive power of logical formalisms for the specification of structural properties;
  • analysis and classification of the models of given logical specifications.

Immediate algorithmic themes in this context are, for instance,

  • decidability and complexity of the logical theories of given structures
    (a classical issue relevant for model checking and verification methodologies);
  • connections between the logical and algorithmic complexities of given structural properties.

Model-theoretic questions, which arise from the modelling of computations, specific models of computation or structural representations of data, include

  • definability issues over special classes of structures;
  • delineation of specialised formalisms designed to capture relevant properties at low levels of complexity;
  • delineation of classes of structures with good model-theoretic properties that are rich enough for the modelling of relevant phenomena.

All these issues typically display a sharp trade-off between tractability and richness/expressiveness (of structures/logics).

Methodological issues:

It is important to note that the basic logical notions of

  • logical equivalence (of two specifications),
  • satisfiability (of a specification),
  • validity (of a deduction)

crucially depend on the underlying class of admissible structures.

Finite model theory, for instance, differs from classical model theory in admitting just finite structures; this restriction is essential for many applications, where infinite instances do not correspond to intended models and hence need to be excluded from all considerations for which the distinction matters. If, for instance, all counter-examples to the equivalence between two specifications or database queries are infinite, then they need to be recognised as equivalent in a setting in which only finite models occur.

Apart from the class of all finite structures, there are many other specific classes of structures that similarly deserve attention – either because they form natural levels with respect to our methods and tools, or because they arise as classes of intended models in some specific context. Similarly, the class of relevant properties may have to be restricted to capture the essence of some modelling scenario: aspects of the structural models that do not correspond to intended aspects of the underlying phenomenon must not make a difference. This imposes specific constraints on the level of granularity at which structural properties are discerned, which in model-theoretic terms typically correspond to preservation properties.

In view of the trade-off mentioned above, the real challenge, besides the technical analysis of interesting scenarios, may often consist in striking a balance between

  • the richness of the class of admissible structures
  • the expressiveness of the logical formalism or the constraints on structural properties under consideration,

taking into account fundamental limitations (like undecidability or lower bounds on complexities) and primarily technical limitations in terms of the available methods.

Research questions and projects:

  • DFG-project: Model constructions and Model-Theoretic Games in Special Classes of Stuctures (2007-2011), involving these topics, among others: model theory of guarded logics and modal logics over special classes of frames, acyclicity in finite hypergraphs and relational structures.
  • DFG-project: Constructions and Analysis in Hypergraphs of Controlled Acyclicity (2013-2018), involving these topics, among others: finite Cayley groups and groupoids with strong acyclicity conditions, finite graph and hypergraph coverings, logical analysis of bisimulation invariance in graph- and hypergraph-like structures, local-to-global constructions for consistency and symmetries.
  • Boundedness Issues in Fixed-Point Recursion
  • Finitely Respresentable Structures
  • FO model checking on generalisations of pushdown graphs
  • Model Constructions and Decompositions
  • Expressive Power of Monadic Second-Order Logic
  • Automata Theory and Algebraic Language Theory

Contact: Prof. Martin Otto

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. Dieses Engagement wird in Kooperation mit dem Ernst-Schröder-Zentrum für Begriffliche Wissensverarbeitung weiterbetrieben.

In diesem Projekt geht es darum, beweistheoretische Verfahren aus der Logik zur Extraktion neuer Daten (wie z.B. effektiver Schranken, „proof mining“) aus prima facie inkonstruktiven Beweisen im Bereich der konvexen Optimierung (und angrenzender Gebiete) einzusetzen. Solche Verfahren, geeignete Formen sogenannter Beweisinterpretationen, wurden vom Antragsteller in den vergangenen Jahrzehnten entwickelt und erfolgreich in der Approximationstheorie, Ergodentheorie, Fixpunkttheorie und der Theorie abstrakter Cauchy-Probleme eingesetzt. In den letzten 2-3 Jahren haben wir zudem erstmals mit Anwendungen im Bereich der konvexen Optimierung begonnen. In dem vorliegenden Projekt soll diese logik-basierte Methodologie nun systematisch auf Probleme aus der konvexen Optimierung zugeschnitten und zur Analyse von Konvergenzbeweisen von in der konvexen Optimierung zentralen iterativen Verfahren eingesetzt werden. Ziel ist dabei insbesondere die Gewinnung expliziter und effektiver Raten asymptotischer Regularität, Metastabilität (im Sinne von T. Tao) und Konvergenz solcher Verfahren, aber auch die Verallgemeinerung auf andere Banachräume als Hilberträume und metrische Strukturen wie z.B. CAT(0)-Räume. Insbesondere analysieren wir Konvergenzbeweise, die Tatsachen aus der abstrakten Theorie mengenwertiger Operatoren (z.B. maximal-monotoner Operatoren) verwenden.
(DFG 04/2018, Kohlenbach)

  • ERC Consolidator Grant (Schweitzer)
  • Proof Mining in der konvexen Optimierung und verwandten Gebieten (DFG, 04/2018, Kohlenbach)
  • Beteiligung am Profilthema ,,Cognitive Science" der TU Darmstadt (Kohlenbach)
  • Emmy-Noether-Nachwuchsgruppe (DFG, 10/2021, ab 04/2023 an der JMU Würzburg, Freund)
  • Konstruktionen und Modelltheorie für Hypergraphen kontrollierter Azyklizität (DFG,04/2013-03/2018, Otto)
  • Logische Extraktion von effektiven uniformen Schranken aus Beweisen, die auf Folgenkompaktheit basieren (DFG, 02/2009-02/2013 und 09/2012-03/2018, Kohlenbach)
  • Mathematische Modelle für eine Semantik von nichtdeterministischen und probalistischen Phänomenen in der Programmierung (DFG, 07/2011-08/2016, Keimel†)
  • Quantitative uniforme Komplexitätstheorie mehrwertiger reeller Funktionen und Operatoren in Analysis (DFG, 04/2013-01/2016, Ziegler, Streicher)
  • Computable Analysis – COMPUTAL (EU IRSES, 12/2012-12/2015, Ziegler, Streicher)
  • Ausdrucksstärke monadischer Logik zweiter Stufe, ihrer Fragmente und Varianten (DFG, 04/2012-12/2014, Blumensath)
  • Strukturkonstruktionen und modelltheoretische Spiele in speziellen Strukturklassen (DFG, 06/2007-03/2011, Otto)
  • Fragments of Dependence Logic with Applications to Real Multifunctions; cooperation with the University of Cambridge (International Exchanges Scheme – 2011/R2 inc. RIA, The Royal Society, Dawar, Otto)
  • Algorithmic Model Theory for Specific Domains (EPSRC, Otto)