Preuves constructives de complétude et contrôle délimité
Motivés par la facilitation du raisonnement sur des méta-théories logiques à l'intérieur de l'assistant de preuve Coq, nous étudions les versions constructives de certains théorèmes de complétude. Nous commençons par l'analyse des preuves de Krivine et Berardi-Valentini qui énoncent q...
| Main Author: | |
|---|---|
| Language: | ENG |
| Published: |
Ecole Polytechnique X
2010
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00529021 http://tel.archives-ouvertes.fr/docs/00/52/90/21/PDF/thesis-danko-ilik.pdf http://tel.archives-ouvertes.fr/docs/00/52/90/21/ANNEX/slides.pdf |