## 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*^{a} 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

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