Thursday 25 July 2019, 14:00, LSV library: Ekstrakto, a tool to reconstruct Dedukti proofs from TSTP files, Yacine El Haddad (Deducteam PhD student) .

Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus, and the proof traces that are produced often lack many details to build a complete proof. We implemented a tool that extracts TPTP subproblems from TSTP file and reconstructs complete proofs in Dedukti using automated provers able to generate Dedukti proofs like ZenonModulo or ArchSAT.