Research

Papers

• Ekstrakto, a tool to reconstruct Dedukti proof from TSTP files, with Guillaume Burel and Frédéric Blanqui, 9 pages, PxTP'19, to appear in EPTCS 301 [PDF].

Software

• Ekstrakto: a TSTP to Dedukti translator (Author).
• SKonverto: a De-Skolemize tool for Dedukti proofs (Author).
• Dedukti: a universal proof checker (Contributor).
• Lambdapi: an extension of Dedukti with metavariables and tactics (Contributor).
• Zenon Modulo: a first-order automated theorem prover based on the tableau method (Contributor).

Talks

• Barbizon, June 2018, Integrating Automated Provers in Proof Assistants. [Slides]

• SAMOVAR, November 2018, Integrating Automated Provers in Proof Assistants. [Slides] & [Poster]

• Natal-Brazil, August 2019, ekstrakto, a tool to reconstruct Dedukti proof from TSTP files. [Slides]