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

PASTEL :: [pastel-00530424, version 1]
http://pastel.archives-ouvertes.fr/pastel-00530424/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.
...