Computer Science – Logic in Computer Science
Scientific paper
2008-04-23
Dans TCS 2008 5th IFIP International Conference on Theoretical Computer Science (2008)
Computer Science
Logic in Computer Science
Scientific paper
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.
Blanqui Frédéric
Jouannaud Jean-Pierre
Strub Pierre-Yves
No associations
LandOfFree
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-105310