From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
| dc.creator | Blanqui, Frédéric | |
| dc.creator | Jouannaud, Jean-Pierre | |
| dc.creator | Strub, Pierre-Yves | |
| dc.date | 2008-04-23 | |
| dc.date.accessioned | 2026-07-07T12:18:27Z | |
| dc.date.available | 2026-07-07T12:18:27Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/0804.3762 | |
| dc.identifier | http://arxiv.org/abs/0804.3762 | |
| dc.identifier | Dans TCS 2008 5th IFIP International Conference on Theoretical Computer Science (2008) | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/212417 | |
| dc.subject | Logic in Computer Science | |
| dc.title | From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures | |
| dc.type | text |