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. (Remark: this is a tar archive containing gzipped Dedukti files.)
• The iProverModulo TPTP library is a library of Dedukti files generated by iProverModulo from TPTP problems. (Remark: this is a tar archive containing gzipped Dedukti files.)
• 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.
• GeoCoqInE is a library of Dedukti proofs encoded in an extension of the Calculus of Inductive Constructions. It has been generated from the GeoCoq library originally written in the Coq theorem prover.

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.
• iProverModulo an extension of the resolution automated theorem prover iProver with deduction modulo producing Dedukti files.
• CoqInE (Coq In dEdukti) produces Dedukti proofs from Coq proofs (work in progress).
• Ekstrakto ("To extract" in Esperanto) A tool to extract TPTP problems from a TSTP trace and reconstruct the proof in Dedukti.

Publications

Publications related to Dedukti

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

Most theories encoded in Dedukti are presented in A Modular Construction of Type Theories.