sign in
english version rss feed

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 () 12, Jean-Pierre Jouannaud () a34, Pierre-Yves Strub () a34

5th IFIP International Conference on Theoretical Computer Science - TCS 2008 273 (2008)

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.

  • Domain : Computer Science/Logic in Computer Science
  • Keywords : proof assistants – proof – lambda-calculus – calculus of constructions – certification – decision procedures – first-order theory – type theory
 
  • inria-00275382, version 1
  • oai:hal.inria.fr:inria-00275382
  • From: 
  • Submitted on: Wednesday, 23 April 2008 15:41:08
  • Updated on: Monday, 6 June 2011 14:34:16
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...