inria-00275382, version 1
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
Frédéric Blanqui
1, 2Jean-Pierre Jouannaud a, 3, 4Pierre-Yves Strub a, 3, 4
5th IFIP International Conference on Theoretical Computer Science - TCS 2008 273 (2008)
Résumé : 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.
- a – Polytechnique - X
- 1 : FORMES (LIAMA)
- INRIA – Tsinghua University / Beijing – LIAMA
- 2 : PAREO (INRIA Lorraine - LORIA)
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- 3 : Laboratoire d'informatique de l'école polytechnique (LIX)
- CNRS : UMR7161 – Polytechnique - X
- 4 : TypiCal (INRIA Saclay - Ile de France)
- INRIA – CNRS : UMR – Polytechnique - X
- Domaine : Informatique/Logique en informatique
- Mots-clés : proof assistants – proof – lambda-calculus – calculus of constructions – certification – decision procedures – first-order theory – type theory
- inria-00275382, version 1
- http://hal.inria.fr/inria-00275382
- oai:hal.inria.fr:inria-00275382
- Contributeur : Frédéric Blanqui
- Soumis le : Mercredi 23 Avril 2008, 15:41:08
- Dernière modification le : Lundi 6 Juin 2011, 14:34:16
Documents associés
Exporter