Home

This work was founded by the INRIA collaboration program ( in french actions de recherches collaboratives de l'INRIA). The project finished end 2010.


Objectives

(Super)deduction modulo is a formalism [DHK01,DHK03] in which deduction steps are seperated from computational steps. Besides its philosophical interest, this distinction allows to reduce the size of proofs (as showed in  [Bur07]) by transfering the algorithmic part of a proof into a congruence defined by rewriting rules. This formalism allows to deduce the coherence and witness properties directly from the cut elimination property.


The project focusses on the development of an universal proof checker called Dedukti. It is based on the application of principles of (super)deduction modulo to type theory [CD07]. The development of this tool requires:

  • to obtain theoritical results for examples for the encoding of proofs from Coq (Calculus of Inductive Constructions formalism) in Dedukti (lambda Pi-calculus modulo formalism)
  • to develop implementation techniques for a successful scale-up.

The first release of Dedukti is now available.


In the current state, the computation of the rewriting systems to encode theories (or inference systems) is not automatic. In this project, we want to extend the work of [BK09] based on completion, to contribute to this automatisation. In this context, it could be useful to have powerful termination techniques (using for example the techniques presented in [BR09]).


We do not restrict ourselves to proof assistants based on type theory but we are also using the proof assistant Lemuridae [BHK07] making explicit a proof term language for superduction modulo and providing as interactive construction of proof terms like in Coq. The originality of Lemuridae is that it is based on the classical sequent calculus, allowing thus to expore non-deterministic calculus as well as proof search.


References

All07
L. ALLAli - «Algorithmic equality in heyting arithmetic modulo», TYPES (M. Miculan, I. Scagnetto et F. Honsell, éds.), Lecture Notes in Computer Science, vol. 4941, Springer-Verlag, 2007, p. 1-17.

BHK07
P. BRAUNER, C. HOUTMANN ET C. KIRCHNER - «Principles of superdeduction», liCS '07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (Washington, DC, USA), IEEE Computer Society, 2007, p. 41-50.

BK09
G. BUREL ET C. KIRCHNER - «Regaining cut admissibility in deduction modulo using abstract completion», Information and Computation 208 (2010), p. 140-164.

BR09
F. BLANQUI ET C. ROUX - «On the relation between size-based termination and semantic labelling», Tech. report, 2009.

Bur07
G. BUREL - «Unbounded proof-length speed-up in deduction modulo», CSL 2007 (J. Duparc et T. A. Henziger, éds.), Lecture Notes in Computer Science, vol. 4646, Springer-Verlag, 2007, p. 496-511.

CD07
D. COUSINEAU ET G. DOWEK - «Embedding pure type systems in the lambda-pi-calculus modulo», TLCA (S. Ronchi Della Rocca, éd.), Lecture Notes in Computer Science, vol. 4583, Springer-Verlag, 2007, p. 102-117.

DHK01
G. DOWEK, T. HARDIN ET C. KIRCHNER - « HOL-[lambda][sigma]: an intentional first-order expression of higher-order logic», Mathematical Structures in Computer Science 11 (2001), no. 1, p. 21-45.

DHK03
G. DOWEK, T. HARDIN ET C. KIRCHNER - « Theorem proving modulo», Journal of Automated Reasoning 31 (2003), no. 1, p. 33-72.

DM07
G. DOWEK ET A. MIQUEL - «Cut elimination for zermelo set theory», Tech. report, 2007.

DW05
G. DOWEK ET B. WERNER - «Arithmetic as a theory modulo», International Conference on Rewriting Techniques and Applications - RTA'05, Lecture Notes in Computer Science, vol. 3467, Springer-Verlag, 2005, p. 423-437.