# A Logical Framework

## What is Dedukti?

Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed.

## Where does the name "Dedukti" comes from?

"Dedukti" means "to deduce" in Esperanto.

## How to get/install/use Dedukti?

See the GitHub repository.

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

There is also a tutorial.

## Dedukti libraries

#### Manual developments

- Dklib is a library defining basic data structures.
- Sigmaid (SIGMA-calculus In Dedukti) is an encoding of the simply-typed ς-calculus in Dedukti.
- Libraries A github repository that aims to contain every hand-written Dedukti files. In the short run, the two links above should be outdated.

#### 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.

- The Holide library is the library produced by Holide on the standard library of the common format for HOL proof assistant: OpenTheory
- The Matita arithmetic library is a library of Dedukti files generated by Krajono.
- The Focalide library is a library of Dedukti files generated by Focalide.
- The Zenon Modulo Set Theory library is a library of Dedukti files generated by Zenon Modulo and dealing with the B Method set theory.
- The iProverModulo TPTP library is a library of Dedukti files generated by iProverModulo from TPTP problems.
- Verine is a library of Dedukti proofs translated from the SMT solver veriT (work in progress).
- STTforall is a library of Dedukti proofs encoded in an extension of Simple Type Theory with prenex polymorphism. These files have been generated from the Matita library encoded in Dedukti.

## Translators to Dedukti

- Holide (HOL In DEdukti) produces Dedukti proofs from HOL proofs, using the Open Theory standard.
- Krajono ("Pencil" in Esperanto) produces Dedukti files from Matita proofs.
- Focalide (FoCaLize In DEdukti) produces Dedukti files from FoCaLize developments.
- Zenon Modulo an extension of the tableaux automated theorem prover Zenon with typing and deduction modulo producing Dedukti files.
- iProver Modulo an extension of the resolution automated theorem prover iProver with deduction modulo produciing Dedukti files.
- CoqInE (Coq In dEdukti) produces Dedukti proofs from Coq proofs (work in progress).

## Publications

Publications related to Dedukti

For an introduction to Dedukti, see this paper (examples used in the paper).