Myriam Quatrini and Lorenzo Tortora de Falco. Polarisation des preuves classiques et renversement. Compte-Rendu de l'Académie des Sciences de Paris, 323:113-116, 1996.

We introduce a new constraint on the proofs of the classical sequent calculus LK^eta_pol (eta-constrained and polarized). We obtain a complete and stable fragment for which the P embedding into linear logic is a decoration.

[ bib | .html ]

Back