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 (Keimel, 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. to other areas within mathematics and w.r.t. to the Logic in Computer Science spectrum.

Research group on Formal Concept Analysis. 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 (Burmeister, Wille). This research continues to be pursued in close co-operation with the Ernst-Schröder-Zentrum für Begriffliche Wissensverarbeitung.



Current Projects/Cooperations

  • Logische Extraktion von effektiven uniformen Schranken aus Beweisen, die auf Folgenkompaktheit basieren (DFG)
  • Konstruktionen und Modelltheorie für Hypergraphen kontrollierter Azyklizität (DFG)
  • Mathematische Modelle für eine Semantik von nichtdeterministischen und probalistischen Phänomenen in der Programmierung (DFG)
  • Fragments of Dependence Logic with Applications to Real Multifunctions; cooperation with the University of Cambridge, Anuj Dawar (International Exchanges Scheme - 2011/R2 inc. RIA, The Royal Society)
  • Quantitative uniforme Komplexitätstheorie mehrwertiger reeller Funktionen und Operatoren in Analysis (DFG)
  • Ernst-Schröder-Zentrum für begriffliche Wissensverarbeitung

Former National and International Cooperations and Projects

  • Computable Analysis - COMPUTAL (EU IRSES)
  • Ausdrucksstärke monadischer Logik zweiter Stufe, ihrer Fragmente und Varianten (DFG)
  • Extraction of effective bounds from proofs based on sequential compactness vial logical analysis (DFG)
  • Strukturkonstruktionen und modelltheoretische Spiele in speziellen Strukturklassen (DFG), 2007-2011
  • 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)
  • Ernst-Schröder-Zentrum, NaviCon




Technische Universität Darmstadt
Department of Mathematics
Logic Group

Schloßgartenstraße 7
64289 Darmstadt

Phone: +49-(0)6151-1622863
Fax:     +49-(0)6151-1622840

Secretary's office
Betina Schubotz

Office hours:
Mo.-Fr.  10:00-15:00


« October 2017 »
Mo Tu We Th Fr Sa Su
39 1
40 2 3 4 5 6 7 8
41 9 10 11 12 13 14 15
42 16 17 18 19 20 21 22
43 23 24 25 26 27 28 29
44 30 31
A A A | Print Print | Impressum Legal note | Contact Contact
    zum Seitenanfangzum Seitenanfang