sign in
english version rss feed

inria-00160586, version 2

Building Decision Procedures in the Calculus of Inductive Constructions

Frédéric Blanqui () a1, Jean-Pierre Jouannaud b2, Pierre-Yves Strub () b2

16th EACSL Annual Conference on Computer Science and Logic - CSL 2007 4646 (2007)

Abstract: It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P' obtained from P thanks to possibly complex calculations. In this paper, we investigate a new version of the calculus of inductive constructions which incorporates arbitrary decision procedures into deduction via the conversion rule of the calculus. The novelty of the problem in the context of the calculus of inductive constructions lies in the fact that the computation mechanism varies along proof-checking: goals are sent to the decision procedure together with the set of user hypotheses available from the current context. Our main result shows that this extension of the calculus of constructions does not compromise its main properties: confluence, subject reduction, strong normalization and consistency are all preserved.

  • a –  INRIA
  • b –  Polytechnique - X
  • 1:  PROTHEO (INRIA Lorraine - LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • 2:  LOGICAL (INRIA Futurs)
  • INRIA – CNRS : FRE 2653 – Université Paris XI - Paris Sud – Polytechnique - X
  • Domain : Computer Science/Logic in Computer Science
  • Keywords : Calculus of Inductive Constructions – Decision procedures – Theorem provers
  • Available versions :  v1 (2007-07-06) v2 (2007-07-09)
 
  • inria-00160586, version 2
  • oai:hal.inria.fr:inria-00160586
  • From: 
  • Submitted on: Monday, 9 July 2007 15:16:14
  • Updated on: Wednesday, 10 October 2007 15:22:48
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...