Elimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction.


Jean Quilbeuf, . 12 juillet 2007 10:15 limd 2:00:00
Abstract:

Je présente la preuve de Prawitz de la faible normalisation de l'élimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction. On déduit ensuite la propriété de la sous-formule et la décidabilité de ce système. Il s'agit du travail fait lors de mon stage M1.