PhD position on the verification of automated reasoning using Isabelle

The Automation of Logic group is looking for a PhD student to work on the formal verification of the metatheory of automated reasoning using the Isabelle proof assistant.

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

• Formalization can offer a convenient means to study extensions, generalizations, or variations of existing calculi.
• 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).
• 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 exact nature of the PhD project will be determined together with the candidate. Two potential projects are the following:

• Verify the correctness of theorem proving calculi and procedures developed in the Automation of Logic group as they are being developed, so that theorem proving research directly benefits its own researchers. One example is the algorithm that reduces (or “grounds”) the Bernays–Schönfinkel fragment of first-order logic over linear arithmetic to plain first-order logic.
• Verify a functional implementation of an automatic theorem prover based on the superposition calculus, corresponding to a minimalistic version of a leading prover such as E, SPASS, or Vampire. The formalized prover would introduce all the main features of such a prover, including a saturation loop, simplification, subsumption, and clause splitting, so that it could serve as a verified reference implementation of superposition.

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. The start date is negotiable.