[TYPES/announce] PhD Position on the formalization of automated reasoning in Isabelle/HOL

[Jasmin Blanchette]

The Automation of Logic group, led by Dr. Christoph Weidenbach, is looking for a PhD student to work on the formalization, in the Isabelle proof assistant, of the metatheory of automated reasoning.

Researchers in automated reasoning spend a substantial portion of their work time developing logical calculi (e.g., DPLL, resolution, and superposition) and proving metatheorems about them. These proofs are typically carried out with pen and paper, which is error-prone and can be tedious. As part of the IsaFoL (Isabelle Formalization of Logic) project [1], we are interested in formalizing results concerning existing logical calculi. The motivation is manifold:

1. Formalization can offer a convenient means to study extensions, generalizations, or variations of existing calculi.

2. Once we have developed suitable libraries and a methodology, formalization becomes not only a way to gain more trustworthiness about the results, it also is more convenient than pen and paper (or LaTeX).

3. Isabelle includes automatic theorem provers as proving backends. There is an undeniable thrill in applying our own tools and find ways to improve them further, based on practical experience with them.

The PhD project is about verifying a functional implementation of a superposition prover: a minimalistic version of E, SPASS, or Vampire, based on the superposition calculus, a saturation loop, simplification, subsumption, and splitting. The project would be executed in close collaboration with Jasmin Blanchette at Vrije Universiteit Amsterdam and members of the Automation of Logic group [2] in Saarbrücken, including Mathias Fleury, Sophie Tourret, and Uwe Waldmann.

The candidate should ideally have some experience with automated or interactive theorem proving, or with some closely related area of theoretical computer science (e.g., term rewriting). To apply, please send your personal record (including CV, grade transcripts, and contact information for two references) by email to Jennifer Müller <jmueller at mpi-inf.mpg.de>.

[1] https://bitbucket.org/isafol/isafol/wiki/Home
[2] https://www.mpi-inf.mpg.de/departments/automation-of-logic/