
Faculty:
Klaus Keimel;
Ulrich Kohlenbach;
Martin Otto;
Thomas Streicher;
Martin Ziegler;
Christian Herrmann;
Thomas Ihringer
Retired:
Peter Burmeister;
Rudolf Wille
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
recursiontheoretic 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,
sZiegler).
Model theoretic investigations
(Herrmann,
Otto) make intramathematical
links with algebra and discrete mathematics (Ihringer).
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 (Otto)
and the resourceoriented and structural sense
(running time, memory, information theory and topology:
Ziegler).
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 cooperation with the
ErnstSchröderZentrum für Begriffliche Wissensverarbeitung.
National and International Cooperations and Projects:
EUWorking 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
Martin Otto
Last modified: Fri May 21 09:40:48 CEST 2004
