Automated assessment of programming exercises
Learning programming requires a lot of hands-on training. This can be supported by automated grading tools that evaluate students' solutions. This project will compile requirements for grading systems to be used in secondary schools and/or universities. Existing tools will then be evaluated and perhaps even a complete grading system will be developed and deployed.
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.
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.
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.
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.
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.
