Sciweavers

Share
CORR
2008
Springer

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

8 years 7 months ago
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.
Frédéric Blanqui, Jean-Pierre Jouann
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
Comments (0)
books