Lorenzo Tortora de Falco. Denotational semantics for polarized (but non-constrained) LK by means of the additives. In 5th 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 Pa 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 ]


This file has been generated by bibtex2html 1.60       >>> BackToHomePage(Protocollo) <<<