Section: Overall Objectives

History

Deduction modulo theory is a formulation of predicate logic where deduction is performed modulo an equivalence relation defined on propositions. A typical example is the equivalence relation relating propositions differing only by a re-arrangement of brackets around additions, relating, for instance, the propositions $P\left(\right(x+y)+z)$ and $P(x+(y+z\left)\right)$. Reasoning modulo this equivalence relation permits to drop the associativity axiom. Thus, in Deduction modulo theory, a theory is formed with a set of axioms and an equivalence relation. When the set of axioms is empty the theory is called purely computational.

Deduction modulo theory was proposed at the end of the 20th century as a tool to simplify the completeness proof of equational resolution [6]. Soon, it was noticed that this idea was also present in other areas of logic, such as Martin-Löf’s type theory, where the equivalence relation is definitional equality, Prawitz’ extended natural deduction, etc. [2]. More generally, Deduction modulo theory gives an account on the way reasoning and computation are articulated in a formal proof, a topic slightly neglected by logic, but of prime importance when proofs are computerized.

The early research on Deduction modulo theory focused on the design of general proof search methods—Resolution modulo theory, tableaux modulo theory, etc.—that could be applied to any theory formulated in Deduction modulo theory, to general proof normalization and cut elimination results, to the definitions of models taking the difference between reasoning and computation into account, and to the definition of specific theories—simple type theory, arithmetic, some versions of set theory, etc.—as purely computational theories.

A new turn with Deduction modulo theory was taken when the idea of reasoning modulo an arbitrary equivalence relation was applied to typed λ-calculi with dependent types, that permits to express proofs as algorithms, using the Brouwer-Heyting-Kolmogorov interpretation and the Curry-de Bruijn-Howard correspondence [5]. It was shown in 2007, that extending the simplest λ-calculus with dependent types, the λΠ-calculus, with an equivalence relation (more precisely a congruence), led to a calculus, called the λΠ-calculus modulo theory, that permits to simulate many other λ-calculi, such as the Calculus of Constructions, designed to express proofs in specific theories.

This led to the development of a logical framework based on the λΠ-calculus modulo theory [29], that could be used to verify proofs coming from different proof systems, such as Coq [27], HOL [32], etc. To emphasize the versatility of this system, we called it Dedukti —“to deduce” in Esperanto. This system is currently developed together with companion systems, Coqine , Krajono , Holide , Focalide , and Zenonide , that permits to translate proofs from Coq , HOL , Focalize , and Zenon , to Dedukti . Other tools, such as Zenon Modulo , directly output proofs that can be checked by Dedukti . Dedukti proofs can also be exported to several other systems. All this is presented in [1].