Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element