EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)

Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui

Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many detai…