PhD thesis: Formal Verification of Higher-Order Superposition in Isabelle/HOL
Team: Mosel-VeriDis, team.inria.fr/veridis/
Automated reasoning is the field of research that investigates techniques for the mechanization of logical reasoning. Superposition is a state-of-the-art calculus to derive the satisfiability of equational formulas in first-order logic. It is implemented in well-known provers such as E and Vampire, that have demonstrated their use in various contexts, including the automation of interactive proofs in proof assistants such as Isabelle/HOL.
In the last few years, we have been involved in an effort to extend this technique to higher-order logic [1,2,3], to allow for reasoning in an even more expressive framework and for a tighter integration of the provers in the proof assistants.
The resulting higher-order superposition calculus, HOSup, was proven complete for Henkin semantics using pen and paper , relying on a framework for saturation theorem proving that we also developed recently . This framework has been formally verified using Isabelle/HOL .
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann: Superposition with Lambdas. CADE 2019.
- Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic: Superposition with First-Class Booleans and Inprocessing Clausification. CADE 2021.
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic: Superposition for Full Higher-Order Logic. CADE 2021.
- Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette: A Comprehensive Framework for Saturation Theorem Proving. IJCAR 2020.
- Sophie Tourret, Jasmin Blanchette: A modular Isabelle framework for verifying saturation provers. CPP 2021.
The doctoral researcher will extend this line of research by formalizing the HOSup calculus, including its proof of completeness, as well as the zipperposition prover architecture realizing HOSup, by instantiating the Isabelle saturation framework previously mentioned.
This formalization will not only strengthen the existing results, but also serve as a starting point for exploring variants of the calculus that preserve its completeness, aiming at containing the explosivity of the functional extensionality axiom and of the unification of flex-flex pairs of terms.
There are several elements that will need to be formalized, including a full higher-order unification algorithm, an ordering compatible with HOSup’s constraints and several variants of superposition that grow in complexity, from ground first-order superposition to full HOSup, including ground first-order superposition with Booleans and ground higher-order superposition. Depending on the interests of the PhD student, the work can be oriented towards the study of calculi for automated reasoning for higher-order logic or towards the application to actual theorem provers, but our overall aim is to go beyond paper-and-pencil proofs and formalize the theoretical development in Isabelle/HOL in order to strengthen confidence in the proofs, be able to explore variations, and eventually derive executable implementations.
- Master degree in computer science (or equivalent)
- Strong foundations in logic, ideally including automated reasoning
- Experience with using a proof assistant, ideally Isabelle/HOL
- Language: English or French
How to apply
- Your CV.
- A cover / motivation letter describing your interest in this topic.
- A short (max one page) description of your Master thesis (or equivalent) or of the work in progress if the thesis is not yet completed.
- Your degree certificates and transcripts for Bachelor and Master (or equivalent).
- Your Master thesis (or equivalent) if it is already completed and publications if any (it is not expected that you have any). If possible, provide Web links to these documents rather than the documents themselves.