From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

Frédéric Blanqui 1, 2 Jean-Pierre Jouannaud 3, 4 Pierre-Yves Strub 3, 4
1 LIAMA - FORMES
2 INRIA Lorraine - LORIA - PAREO
3 LIX - Laboratoire d'informatique de l'école polytechnique [Palaiseau]
4 INRIA Saclay - Ile de France - TYPICAL
Abstract : We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order decision procedures: deduction is still in charge of the CIC kernel, while computation is outsourced to dedicated first-order decision procedures that can be taken from the shelves provided they deliver a proof certificate. The soundness of the whole system becomes an incremental property following from the soundness of the certificate checkers and that of the kernel. A detailed example shows that the resulting style of proofs becomes closer to that of the working mathematician.
Keywords : proof assistants proof lambda-calculus calculus of constructions certification decision procedures first-order theory type theory
Document type :
Conference papers
5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, IFIP. <10.1007/978-0-387-09680-3_24>
https://hal.inria.fr/inria-00275382
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, April 23, 2008 - 3:41:08 PM
Last modification on : Monday, June 6, 2011 - 2:34:16 PM

Files

main.pdf
fileSource_public_author

Identifiers

Collections

CNRS | INRIA | LIX | LIAMA | X-LIX | X-DEP-INFO | X | PARISTECH | LORIA | LORIA-FM

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub. From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures. 5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, IFIP. <10.1007/978-0-387-09680-3_24>. <inria-00275382>

Export

BibTeX | XML | endNote

Share

Metrics

Consultation de
la notice

173

Téléchargement du document

55

Contact


archive-ouverte@inria.fr