Lorenzo Tortora de Falco. Denotational semantics for polarized (but non-constrained) LK by means of the additives. In 5^th Kurt Goedel Colloquium KGC'97, computational logic and proof theory, volume 1289 of Lecture Notes in Computer Science, pages 290-304, 1997.

Following the idea that a classical proof is a superimposition of `constructive' proofs, we use the linear connective ``&'' to define an embedding P<sup>a</sup> of polarized but non-constrained LK in linear logic, which induces a denotational semantics. A classical cut-elimination step is now a cut-elimination step in one of the `constructive slices' superimposed by the classical proof.

[ bib | .html ]

Back