Theoretical Computer Science

Computer science is a theoretical science. It

But what can we construct? Does what we have constructed also behave as we expect? Computers change our lives.
Do they enrich it too? Do we know what man-made artifacts do, what they can do, and what their limits are?

These questions touch on the fundamentals of computer science. Answering them is difficult and requires the use of sophisticated tools from mathematics. Often the problems cannot be mastered with the available tools and new mathematics has to be developed and adapted for the treatment of computer science problems.

From this broad spectrum of problems, two groups of problems are primarily dealt with in the theoretical computer science department:

This problem area deals with the design of systematic methods for the synthesis, verification and optimization of algorithms and software systems. A special focus is on methods that can be described in logical calculi and thus implemented with the help of interactive and automatic proof systems, and on the application of such methods in the development of reliable and efficient software.

Proof calculi for expressive logics are in principle able to formalize and specify every proof problem. However, a practical problem in reasoning is the size of the resulting evidence. While interactive proof systems are a very good tool for constructing formal proofs without errors, the effort involved in finding such proofs makes interactive proof construction impractical for complex proof objectives. Fully automatic proof procedures, on the other hand, are currently only available for relatively weakly expressive logics. The aim of our work is therefore the development of automatic proof procedures for more expressive logics which are suitable for controlling the construction of proofs in interactive proof systems.