Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic

Melanie Taprogge, Frédéric Blanqui, Alexander Steen

We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving e…