Research

Papers


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]