Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TLCA

2005

Springer

2005

Springer

Abstract. We present a theory of proof denotations in classical propologic. The abstract deﬁnition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This gives us a “Boolean” category, which is not a poset. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identiﬁed. Though a “real” sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures.

Related Content

Added |
28 Jun 2010 |

Updated |
28 Jun 2010 |

Type |
Conference |

Year |
2005 |

Where |
TLCA |

Authors |
François Lamarche, Lutz Straßburger |

Comments (0)