Institute of Computer Science



Truthmaker semantics for modal and justification logic


Truthmaker semantics is a novel framework that focuses on exact verification and falsification rather than on truth conditions. It has been recently and successfully applied to metaphysics and linguistic topics. Designing a truthmaker semantics for modal and justification logic is an open problem.



Higher-order approaches to metaphysic and deontic modality


Metaphysical modality (It is necessary/possible that) and deontic modality (it is obligatory/permitted that) are usually dealt with propositionally or at the first-order (with quantification over individuals), rather than higher-order (quantification over properties and propositions). This thesis explores higher-order metaphysics and deontic modality.



Predicate approaches to deontic modality


Deontic modality (it is obligatory/permitted that) is usually dealt with propositionally. This thesis explores a predicate approach to deontic modality, which is expressed through predicates, rather than propositional operators.



Topics in philosophy of language: scalarity, degrees, evaluatives


Evaluative adjectives (good, vile, etc.) seem to be scalar (e.g. they admit of degrees and comparisons: A is taller than B) and multidimensional, if non-additive. This thesis explores their formal semantics.



Formal Ethics


Formal ethics deal with topics from moral theory in a formal way. Some examples are practical reasons, value uncertainty, etc.



Conflict-driven clause learning


Conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). The CDCL approach has made SAT solvers so powerful that they are being used effectively in many real world application areas like AI planning, bioinformatics, and hardware and software verification.
The aim of the thesis is to understand the inner workings of CDCL and to write a tutorial about it that can be used in lectures.


Sequent calculus for macaroons


Macaroons provide a flexible authorization mechanism for distributed systems. There exists an extended authorization logic to formally describe properties of Macaroons. However, this logic is unsuitable for automated proof search and implementations.
The goal of this thesis is to develop a sequent calculus for this authorization logic that supports automatic proof search.

Information is physical


Landauer's principle pertains to the lower limit of energy consumption of a computation. It holds that "any logically irreversible manipulation of information, such as the erasure of a bit, must be accompanied by a corresponding entropy increase". Typically this increase takes the form of energy imported into the computer, converted to heat, and dissipated into the environment.
The aim of this thesis is to write an introduction to Landauer's principle for computer scientists. It may also cover related topics such as Maxwell's daemon or reversible computation.



The model checking algorithm for CTL


The labeling algorithm checks if a property is true in a model for the computation tree logic (CTL). This can be used for example to check if an algorithm guarantees mutual exclusion.

The aim of the thesis is to give an introduction to CTL and the labeling algorithm. It may also cover the question of complexity.



General algebraic structures for justification logic

In traditional justification logic, evidence terms have the syntactic form of polynomials, but they are not equipped with the corresponding algebraic structure.

The aim of the thesis is to present a semantic approach to justification logic that models evidence by general algebraic structures.



Diagonalization and the P vs. NP - Problem (Bachelor)

The P vs. NP -problem is a major open problem in theoretical computer science. It asks whether every problem whose solutions can be efficiently verified can also be solved efficiently. The special charm of this problem lies in the fact that it seems surprisingly simple and easy to understand, yet no one has been able to solve it in more than 50 years.

In this project we are going to take a first step at investigating why P vs. NP is so difficult to solve. To that end we will study the proof method of diagonalization including its applications in complexity theory and we will show why this method is not strong enough to resolve the P vs. NP -problem. If time permits, further topics in complexity theory can be explored. The aim of the thesis is to understand the method of diagonalization and its impact on complexity theory in general and on the P vs. NP -problem in particular and to summarize these results in a written paper.



Proof Theory for PDL (Bachelor)

Propositional Dynamic Logic (PDL) is an extension of modal logic with so-called fixed point operators, resulting in a logical language suitable to express properties of programs. Proof Theory is a branch of mathematical logic that studies proofs as mathematical objects. In standard proof theory, proofs are finite objects. However, for fixed point logics such as PDL, proofs are in general infinite. This step from finite to infinitary proofs is caused by the fixed point operators of the logic.

In this project we are going to study a specific infinitary proof system for PDL and explore its properties. If time permits, the student might prove some new properties of the system on her own. The goal of the thesis is to obtain a good understanding of PDL and gain some insight into its proof theory and to summarize the results of the investigation in a written paper.

Other topics in the area of logic and theoretical computer science are also possible. If you would like to propose a topic for a thesis, please contact us.