The research group primarily represents the subject area of Mathematical Logic viewed as an applied foundational discipline between mathematics and computer science. Research activities focus on the application of proof theoretic, recursion theoretic, category theoretic, algebraic and model theoretic methods from mathematical logic to mathematics and computer science.

Beside classical mathematical logic (with proof theory, recursion theory and model theory) this involves constructive type theory, categorical logic, universal algebra, domain theory, lattice theory, finite model theory, and algorithmic issues.

Within mathematics, a primary field of applications in the proof- and recursion-theoretic setting (Kohlenbach) is the extraction of new information from proofs in algebra, analysis, functional analysis, hyperbolic geometry and numerical mathematics (proof mining). This involves qualitative aspects (e.g., independence of existence assertions from certain parameters) as well as quantitative aspects of computability and complexity of solutions (extraction of algorithms and bounds from proofs, exact real arithmetic, “computational mathematics”: Kohlenbach, Streicher). Model theoretic investigations (Herrmann, Otto) make intra-mathematical links with algebra and discrete mathematics.

Concerning Logic in Computer Science and the mathematical foundations of computer science, major activities revolve around issues of semantics. On the one hand this involves the mathematical foundation of the semantics and the logic of programming languages (Streicher); on the other hand, logics and formal systems are investigated in the sense of model theoretic semantics, w.r.t. expressiveness and definability, with an emphasis on computational aspects (algorithmic model theory, finite model theory: Otto). We investigate complexity issues from the point of view of functional programs (implicit computational complexity: Kohlenbach), in the descriptive and the resource-oriented and structural sense (Otto). Besides specific application domains in computer science, as, e.g., verification, data bases and knowledge representation, there is work on foundational issues in the areas of computability and complexity, as well as type theory and category theory.

Overall, the unit forms an internationally well connected cluster of expertise, with a characteristic emphasis on the connections that mathematical logic has to offer, both w.r.t. other areas within mathematics and w.r.t. the Logic in Computer Science spectrum.

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

Based on lattice and order theoretic foundations, this group in the former AG1 (General Algebra and Discrete Mathematics) focuses on graphical logic systems for concept analysis in knowledge acquisition and processing applications. This research continues to be pursued in close co-operation with the Ernst-Schröder-Zentrum für Begriffliche Wissensverarbeitung.

In this Project we aim at using proof-theoretic methods from logic for the extraction of new data (such as effective bounds, “proof mining”) from prima facie noneffective proofs in convex optimization and related areas. We need to tailor the proof-theoretic methods to the specific domain of applications and will then apply them for the extraction of rates of asymptotic regularity, metastability (in the sense of T. Tao) and convergence of central iterative procedures used in convex optimization. In particular, we will study convergence proofs which make use of facts from the abstract theory of set-valued operators (e.g. maximally monotone operators).
(DFG 04/2018, Kohlenbach)

  • ERC Consolidator Grant (Schweitzer)
  • Proof Mining in der konvexen Optimierung und verwandten Gebieten (DFG, 04/2018, Kohlenbach)
  • Participation in the research area ,,Cognitive Science" at TU Darmstadt (Kohlenbach)
  • Emmy-Noether-Nachwuchsgruppe (DFG, 10/2021, 04/2023 continued at JMU Würzburg, Freund)
  • Konstruktionen und Modelltheorie für Hypergraphen kontrollierter Azyklizität (DFG,04/2013-03/2018, Otto)
  • Extraction of effective bounds from proofs based on sequential compactness vial logical analysis (DFG, 02/2009-02/2013 and 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)