| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
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.
Cited literature [21 references]
https://hal.inria.fr/inria-00275382
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, April 23, 2008 - 3:41:08 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Friday, May 28, 2010 - 5:23:09 PM
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, April 23, 2008 - 3:41:08 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Friday, May 28, 2010 - 5:23:09 PM
Files
main.pdf
Files produced by the author(s)