Preuves constructives de complétude et contrôle délimité

TEL :: [tel-00529021, version 1]
http://tel.archives-ouvertes.fr/tel-00529021/fr/
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 que la logique classique est constructivement complète au regard des modèles booléens relaxés, ainsi que l'analyse de l'algorithme de cette preuve.
...