Two PhD-student positions are open in the project
Non-wellfounded and cyclic proof theory
in the Logic and Theory Group of the Institute of Computer Science at the University of Bern (www. ltg.unibe.ch). The positions are available from September 2023 (negotiable) for a period of up to 4 years.
Tasks
This SNSF-funded project is concerned with fixed points, recursive definitions, and proofs by induction, which are essential concepts in mathematics and computer science. In recent years, a novel approach to formal proofs representing concepts of this kind has become popular, namely non-wellfounded and cyclic proofs. These proofs not only derive propositions from axioms, but they also provide a formal counterpart to proofs by infinite descent, i.e. proof branches that are not well-founded but satisfy some global soundness condition. In this project, we aim for a better understanding of the structural properties of non-wellfounded and cyclic proof systems. We plan to develop syntactic cut-elimination procedures for (fragments of) the modal mu- calculus. Further, we will devise novel modal logics featuring non-monotone inductive definitions. In the last part of the project, we will investigate closure ordinals of positive and non-monotone modal fixed point operators.
Requirements
Candidates should have a strong background in logic (mathematics, computer science). University regulations require doctoral students to hold a Master's or equivalent degree.
We offer
We offer a stimulating research environment in an international research group. The University of Bern conducts excellent research and lives up to its vision that Knowledge generates value. Bern is ideally located in the middle of Switzerland and Europe, providing rich cultural and outdoor activities. The gross salary is around 48k CHF for PhD students.
Applications should include: 1) a motivation letter (max. 1 page), 2) a complete CV, 3) academic transcripts and a copy of relevant diplomas, 4) contact information or reference letter of the MSc thesis supervisor.
The complete application should be sent as a single pdf file to Prof. Thomas Studer at [email protected]
www. unibe.ch