Most of the software written by members of Deducteam are using OCaml. We provide an Opam repository to make their installation easier. If you have opam installed, you only need to type:

`opam repository add deducteam https://scm.gforge.inria.fr/anonscm/git/opam-deducteam/opam-deducteam.git`

## Proof checking tools

- Dedukti: a universal proof checker
- Sukerujo: an extension of Dedukti with syntactic constructions for common data types
- Meta Dedukti: a Dedukti file normalizer
- Rainbow: a termination certificate verifier

## Proof translation tools

- Coqine: a Coq to Dedukti proof translator
- Focalide: a FoCaLiZe to Dedukti proof translator
- Holide: a HOL to Dedukti proof translator
- Krajono: a Matita to Dedukti proof translator

## Automated theorem proving tools

- HOT: an automated termination prover for higher-order rewrite systems
- iProver Modulo: a theorem prover based on polarized resolution modulo
- mSat: a modular SAT/SMT solver with proof output
- SuperZenon: an extension of the Zenon automated theorem prover using superdeduction
- ZenonModulo: an extension of Zenon using deduction modulo able to produce proofs in Dedukti format

## Libraries

- 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