Funded PhD studentship: Integrating Automated Provers in Proof Assistants

Do not wait for the deadline: applications will be treated on the fly.

Application deadline: 29 October 2017

PhD start deadline: 1st January 2018

Summary: To widen their use, proof assistants needs more
automation. This can be performed by calling external automated
theorem provers. Centered
around Dedukti, a proof
checker for the universal logical framework λΠ-calculus
modulo theory, the objective is to design a proof environment that is
able to call external provers to build part of the proof. The global
architecture must emphasize the need to have a correct and exhaustive
proof once the portions proved externally are glued together. From
Dedukti to external provers, proof obligations in the
λΠ-calculus modulo theory must be passed in an efficient
way, either by encoding them or by extending the external prover to
accept them. Reciprocally, proofs or proof traces produced by these
tools needs to be reconstructed back into Dedukti.