# Publication details

##
Naming Proofs in Classical Propositional Logic

François Lamarche, Lutz Straßburger

Submitted., 2004

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.

Download PDF
Show BibTeX

@UNPUBLISHED{LamStrNaming,
title = {Naming Proofs in Classical Propositional Logic},
author = {François Lamarche and Lutz Straßburger},
year = {2004},
note = {{Submitted.}},
}

Login to edit

Legal notice, Privacy policy