Building Decision Procedures in the Calculus of Inductive Constructions

Frédéric Blanqui 1 Jean-Pierre Jouannaud 2 Pierre-Yves Strub 2
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Keywords : Calculus of Inductive Constructions Decision procedures Theorem provers
Type de document :
Communication dans un congrès
Jacques Duparc and Thomas Henziger. 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. Springer Verlag, 4646, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74915-8_26〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00160586
Contributeur : Pierre-Yves Strub <>
Soumis le : lundi 9 juillet 2007 - 15:16:14
Dernière modification le : jeudi 10 mai 2018 - 01:32:34
Document(s) archivé(s) le : mardi 21 septembre 2010 - 13:39:05

Fichiers

cccnat.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | X | PARISTECH | UMR8623 | LORIA | UNIV-LORRAINE

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub. Building Decision Procedures in the Calculus of Inductive Constructions. Jacques Duparc and Thomas Henziger. 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. Springer Verlag, 4646, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74915-8_26〉. 〈inria-00160586v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

396

Téléchargements de fichiers

104

Contact


archive-ouverte@inria.fr