Skip to Main content Skip to Navigation
Reports

Naming Proofs in Classical Propositional Logic

François Lamarche 1 Lutz Strassburger 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00099866
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:56:42 AM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM
Document(s) archivé(s) le : Friday, November 25, 2016 - 12:08:36 PM

Identifiers

  • HAL Id : inria-00099866, version 1

Collections

Citation

François Lamarche, Lutz Strassburger. Naming Proofs in Classical Propositional Logic. [Intern report] A04-R-391 || lamarche04b, 2004, 15 p. ⟨inria-00099866⟩

Share

Metrics

Record views

116

Files downloads

131