The theory of parameterised complexity is primarily concerned with problems that cannot be solved in polynomial time. As the name suggests, the aim is to investigate parameterisations of the problem that are relevant in practice. The goal is to find a parameter such that the problem can be solved in a runtime that can be represented as a product of a polynomial of the input length and an arbitrary function in the parameter. In this case, the problem is said to be fixed parameter tractable.

Backdoors
A very interesting parameter is backdoors. These backdoors are supposed to provide a figurative shortcut to a sub-problem that can be solved efficiently. In the previous project, such backdoors were investigated in temporal logic, which is a fundamental tool in the field of program verification. In the follow-up project, further research will now be conducted on this concept. The aim is to find a suitable definition that is more practical and more closely interwoven with the temporal concepts. In the previous project, a coherent definition was also found in default logic, a non-monotonic logic used in the fields of artificial intelligence. Now, in addition to a precise classification of the problems parameterised in this way, the applicability of so-called QBF solvers is to be investigated. QBF solvers are programs that attempt to solve a more complex type of propositional logic formula. These types of formulas can (presumably, that is, under reasonable complexity-theoretic assumptions) formalise significantly stronger problems. Research on QBF solvers is still quite young compared to the highly optimised SAT solvers (which solve the prominent problem of the satisfiability of propositional formulas).

(Parametrised) Enumeration and Dependency Logic
Dependencies, whether on a functional level, play a role in the area of databases. However, other areas, such as game theory or physical properties, can also be modelled with this tool. So far, there have been no investigations into the parameterised complexity of problems in this logic. We would now like to analyse a propositional variant of this logic in more detail. In this section, we also want to address the algorithmic question of (parameterised) enumeration. Often it is interesting to know the most favourable solution or the k-th solution with respect to a certain order. Enumeration for non-classical logics, as we are investigating in this project, has so far been the subject of very little research. We want to close this gap and classify certain non-monotone formalisms in this regard. This analysis also serves to better understand enumeration as a task in itself.