Tools
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
Problem data bases
- TPTP: Thousands of Problems for Theorem Provers
- TGTP: Thousand of Geometric Problems for Geometric Theorem Provers
Proof data bases
- Nubo: metadata on Dedukti libraries
- Logipedia: Matita arithmetic library translated to Dedukti/STTfa, Coq, Lean, OpenTheory, HOL-Light, PVS
- Coq Opam Packages
- Isabelle Archive of Formal Proofs
- Mizar Mathematical Library
Proof data bases tools
- FindFacts: search tool for Isabelle
- SErAPIS: search tool for Isabelle
- 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
Proof translation tools
- Agda2Dedukti: Agda to Dedukti/Agda or Lambdapi/Agda
- Vodk: Coq to Dedukti/Coq
- Dk2agda: Dedukti to Agda
- Ekstrakto: TSTP to TPTP and Lambdapi/FOL
- 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
Interactive theorem provers
- Agda
- Coq
- Isabelle (can reconstruct proofs generated by veriT and Z3)
- Lean
- Lambdapi
- LISA
- Matita
- Mizar
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.
- 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).