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://anonsvn@gforge.inria.fr/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
- Sigmaid: a ς-calculus to Dedukti program 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
- ZenonArith: an extension of Zenon for arithmetic using the simplex algorithm
- ZenonModulo: an extension of Zenon using deduction modulo able to produce proofs in Dedukti format
- Zipperposition: a superposition prover featuring arithmetic and induction