European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

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

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.
  • Eldarica: SMT solver for problems in the constrained Horn fragment. Can output models of Horn clauses in SMT-LIB, and proofs of unsatisfiability in several formats.
  • Goéland: A first-order concurrent tableau-based automated theorem prover with equality and management of theories with DMT that produce proofs in Rocq, LambdaPi, TPTP and Lisa.
  • Larus: Larus is a theorem prover for coherent logic that uses SAT/SMT provers to construct proofs. Larus can generate natural language proofs (in LaTeX) and machine checkable proofs (Coq/Isabelle/Mizar).
  • Leo-III: ATP for (polymorphic) higher-order logic, providing proofs in TPTP format.
  • Princess: ATP and SMT solver for first-order logic modulo various theories, with support for outputting proofs in different formats.
  • 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).

Type-checkers for the λΠ-calculus modulo theory

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

Problem data bases

  • TPTP: Thousands of Problems for Theorem Provers
  • TGTP: Thousand of Geometric Problems for Geometric Theorem Provers
  • ADGLib: Axiom systems, standard signature and library of problems for Geometric Theorem Provers

Proof data bases

Proof data bases tools

  • agda2train: extracts JSON proof objects from Agda programs, to be used for machine learning purposes (as in Quill)
  • DAMF: Distributed Assertion Management Framework
  • Lambdapi >= 2.4.0 includes commands for indexing Dedukti and Lambdapi files, making complex search queries and running a web server for making queries on the web

Search engines

Proof translation tools

  • Agda2Dedukti: Agda to Dedukti/Agda or Lambdapi/Agda
  • CoqInE: Coq to Dedukti/Coq
  • Dk2agda: Dedukti to Agda
  • Ekstrakto: TSTP to TPTP and Lambdapi/FOL (subsumed by GDV-LP)
  • GDV-LP: TPTP to Lambdapi/FOL (doc)
  • Hol2dk: HOL-Light to Dedukti and Lambdapi
  • 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
  • Logic embedding tool: Translates non-classical proof obligations into higher-order logic
  • Personoj: PVS to Lambdapi
  • Skonverto: construct a proof of a formula from a proof of its skolemized version
  • tptp-utils: Translates various TPTP/TSTP formats into each other
  • Universo: type universes rewriting tool
  • SMTCoq: reconstruct proofs from SMT solvers in Coq
  • CoqHammer: reconstruct proofs from ATPs in Coq
  • Maude2Lean
  • Lean2Coq: Lean to Coq
  • B-pog-translator: translator from Atelier B proof obligation files to Lambdapi
  • Predicativize: translate Dedukti proofs to Dedukti proofs with universe polymorphism, and translate them to Agda
  • Lean2dk: Lean4 to Dedukti
  • Carcara: translator from Alethe to Lambdapi
  • mml2lambdapi: translator from Mizar to Lambdapi

AI models for theorem proving

  • Quill: neural representation of dependently-typed Agda terms, with an application in premise selection (uses the JSON dataset generated from agda2train)