A universal proof checker

What is Dedukti?

Dedukti is a universal proof checker, based on the λΠ-calculus modulo.

Where does the name "Dedukti" comes from?

"Dedukti" means "to deduce" in Esperanto.

How to get/install/use Dedukti?

See the manual for the current version (v2.5) of Dedukti.

There is also a tutorial.

Dedukti libraries

Manual developments

Generated libraries

Each tarball contains a Makefile in order to check the library. You may want to modify the variables DKDEP and DKCHECK that are the paths of the corresponding binaries.

Translators to Dedukti