A PhD position is open at the MPII in Saarbrücken, with Christoph Weidenbach, Sophie Tourret, and myself as supervisors. The project is about using Isabelle/HOL to formalize logical calculi. Today, much of the research done in automated reasoning is carried out with pen and paper, but we believe proof assistants can help researchers write better proofs and ultimately design better automatic theorem provers.
See the job ad for more information.
Last updated: Dec 05 2021 at 23:19 UTC