Strub, Pierre-Yves (2008) Type Theorie and Decision Procedures. PhD thesis Informatique, Informatique, EP/X p.101.
Full text available as:
|
|
Abstract
The goal of this thesis is to develop a logical system in which formal proofs of mathematical statements can be carried out in away which is close to mathematical practice.
Our main contribution is the definition and study of a new calculus, the Calculus of Congruent and Inductive Constructions, an extension of the Calculus of Inductive Constructions (CIC) integrating in its computational part the entailment relation - via decision procedures - of a first order theory over equality. A major technical innovation of this work lies in the computational mechanism: goals are sent to the decision procedure together with a set of user hypotheses available from the current context.
Our main results show that this extension of CIC does not compromise its main properties: confluence, strong normalization, consistency and decidability of proof checking are all preserved (as soon as the incorporated theory is itself decidable). As such, our calculus can be seen as a decidable restriction of the Extensional Calculus of Constructions. It can therefore serve as the basis for an extension of the Coq proof assistant.
| Item Type: | PhD Thesis (PhD) |
|---|---|
| PhD Supervisor: | Jouannaud, Jean-Pierre |
| Date: | 02 July 2008 |
| Board of examiners: | Barthe, Gilles and Meseguer, José and Shanjar, Natarajan |
| Ecole Doctorale: | ED 447 ECOLE DOCTORALE DE L'ECOLE POLYTECHNIQUE |
| Discipline: | Informatique |
| Collection (Fonds): | Ecole Polytechnique (EP/X) |
| Institution: | EP/X |
| Department: | Informatique |
| Subjects: | 1. Mathematics and Applications |
| ID Code: | 4678 |
| Deposited By: | Pierre-Yves Strub |
| Deposited On: | 09 February 2009 |
Repository Staff Only: edit this item