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