Paper anouncement
Lutz Strassburger <lutz-F/[email protected]>
| Newsgroups | gmane.science.mathematics.frogs |
|---|---|
| Message-ID | <[email protected]> |
Hi Frogs, since there was a recent discussion on cut elimination and proof nets for classical logic, there might be some interest in the following paper that we submitted to TLCA'05: Title: Naming Proofs in Classical Propositional Logic Authors: Francois Lamarche and Lutz Strassburger Abstract: We present a theory of proof denotations in classical propositional logic. The abstract definition 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. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. 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, and we get ``Boolean'' categories which are not posets. The paper is available on the web at http://www.ps.uni-sb.de/%7elutz/papers/namingproofsCL.pdf Comments are welcome. Best regards, Lutz