Naming Proofs in Classical Propositional Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2004

Naming Proofs in Classical Propositional Logic

Résumé

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.
Fichier principal
Vignette du fichier
A04-R-391.pdf (655.28 Ko) Télécharger le fichier

Dates et versions

inria-00099866 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00099866 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More