Institute of Computer Science


Research Projects

Explicit reasons

This project is concerned with reasons why one believes something, reasons why one knows something, and reasons why one ought to do something. We develop formal languages in which reasons can be represented explicitly and investigate the logical properties of explicit reasons. To achieve this, we rely on the framework of justification logic.
In particular, we present non-normal deontic logics with justifications. Further, we develop a semiring framework for justifications, and we engineer a possible world semantics for justifications that supports additional structure like graded justifications or probability distributions on justifications.


Justifications and Non-Classical Reasoning

In most situations, the exact actual state of our environment is unknown and we only have incomplete information available when we have to make decisions. Therefore, we often use some form of reasoning under uncertainty in order to make inferences or to plan actions.

This project seeks to develop novel probabilistic justification logics and corresponding non-classical reasoning procedures to model epistemic situations with incomplete information.


Logic and Computation

This very general project deals with the close connections between mathematical logic and certain parts of computer science, and emphasis is put on a proof-theoretic approach to some of the central questions in this area of research. These include the development of perspicuous and feasible logical frameworks for studying typical questions in computer science like termination and correctness of functional programs, properties of distributed systems and the like.

We study applicative theories as well as strongly typed formalisms and are interested in the connections to constructive and explicit mathematics. Furthermore, we are interested in analyzing the close connections between the complexities of computations and proofs in suitable formalizations, ranging from propositional calculi up to abstract frameworks for computations (in higher types).