All Deducteam tools are available on Github.

## Type-checking tools

- Dedukti: a type-checker for the λΠ-calculus modulo rewriting

## Proof development tools

- Lambdapi: a proof assistant for the λΠ-calculus modulo rewriting, compatible with Dedukti

## Proof translation tools

- CoqInE: a Coq to Dedukti translator
- Holide: an OpenTheory to Dedukti translator
- Agda2Dedukti: an Agda to Dedukti translator
- Isabelle_Dedukti: an Isabelle to Dedukti translator
- Krajono: a Matita to Dedukti translator
- Logipedia: a tool for translating Dedukti proofs in the theory STTfa to Coq, Lean, PVS and OpenTheory
- Ekstrakto: a TSTP to Dedukti translator
- SKonverto: generates a proof of a first-order formula from a proof of its skolemized version
- lrat2dk: a LRAT to Dedukti translator

## Automated theorem proving tools

- ArchSAT: an SMT/McSat solver producing Dedukti proofs
- iProverModulo: an extension of iProver with polarized resolution modulo
- ZenonModulo: an extension of Zenon with rewriting generating Dedukti and Lambdapi proofs

## Termination tools

- SizeChangeTool: a termination checker for Dedukti

## Libraries

- Logipedia.science: a website providing a library of arithmetic proofs in Dedukti, Coq, Lean, PVS and OpenTheory
- Nubo: a repository of Dedukti proofs
- CoLoR: a Coq library on rewriting theory and termination

## Code generation tools

- Moca: a generator of construction functions for data types with algebraic relations on constructors