Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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 details to build a complete proof. Hence these traces are hard to check and reuse in proof assistants. DEDUKTI is a proof checker whose proofs can be translated to various proof assistants: Coq, HOL, Lean, Matita, PVS. We implemented a tool that extracts TPTP subproblems from a TSTP file and reconstructs complete proofs in DEDUKTI using automated provers able to generate DEDUKTI proofs like ZenonModulo or ArchSAT. This tool is generic: it assumes nothing about the proof calculus of the prover producing the trace, and it can use different provers to produce the DEDUKTI proof. We applied our tool on traces produced by automated theorem provers on the CNF problems of the TPTP library and we were able to reconstruct a proof for a large proportion of them, significantly increasing the number of DEDUKTI proofs that could be obtained for those problems.
Document type :
Conference papers
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-02200548
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, July 31, 2019 - 11:25:56 AM
Last modification on : Wednesday, October 14, 2020 - 3:41:58 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

Citation

Mohamed El Haddad, Guillaume Burel, Frédéric Blanqui. Ekstrakto A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). PxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving, Aug 2019, Natal, Brazil. pp.27-35, ⟨10.4204/EPTCS.301.5⟩. ⟨hal-02200548⟩

Share

Metrics

Record views

197

Files downloads

1215