To contribute to the web site, please open an issue, create a pull request or send a mail to the science communication coordinators.

Type-checkers for the λΠ-calculus modulo theory

  • Dkcheck: type-checker
  • Kontroli: parallel version of dkcheck
  • Lambdapi: interactive extension of dkcheck with metavariables and tactics

Proof data bases

Proof translation tools

  • Agda2Dedukti: Agda to Dedukti/Agda or Lambdapi/Agda
  • Vodk: Coq to Dedukti/Coq
  • Dk2agda: Dedukti to Agda
  • Ekstrakto: TSTP to Dedukti/FOL or Lambdapi/FOL
  • Holide: OpenTheory to Dedukti/STTfa
  • HOLLightToDk: HOL-Light to Dedukti/STTfa
  • Krajono: Matita to Dedukti/Matita
  • Isabelle_dedukti: Isabelle to Dedukti or Lambdapi
  • Logipedia: Dedukti/STTfa to Coq, Lean, Matita, OpenTheory, HOL-Light, PVS
  • Personoj: PVS to Lambdapi
  • Skonverto: construct a proof of a formula from a proof of its skolemized version
  • Universo: type universes rewriting tool
  • SMTCoq: reconstruct proofs from SMT solvers in Coq
  • CoqHammer: reconstruct proofs from ATPs in Coq

Interactive theorem provers

Automated theorem provers

  • ArchSAT: SMT solver generating Dedukti/FOL.
  • cvc5: efficient versatile SMT solver generating proof traces.
  • E: High-performance equational theorem prover for first-order logic (and increasingly higher-order logic), creating proof objects in TPTP format.
  • Vampire: ATP handing first-order and higher-order logic with equality and theories producing fine-grained TPTP compliant proofs.
  • veriT: SMT solver generating detailed proof traces in the Alethe format.
  • ZenonModulo: ATP generating Dedukti/FOL or Lambdapi/FOL.
  • Zipperposition: Superposition prover initially designed for prototyping ideas but increasingly powerful especially on higher-order benchmarks.
  • z3: efficient SMT solver that generates proofs (for a subset of checks, at least).