Paper anouncement

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