3532 articles – 5253 Notices  [english version]

hal-00012294, version 1

Naming Proofs in Classical Propositional Logic

François Lamarche () 1, Lutz Strassburger ()

(2005) 434

Résumé : We present a class of objects that denote proofs in classical propositional logic. The general definitions are in terms of a semiring of parameters. We discuss two concrete instances: With the Boolean semiring we get a theory of proof nets for classical logic, that comes with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This allows us to build ``Boolean'' *-autonomous categories that are not posets. 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 particular the NP vs. co-NP problem. The strongly normalizing cut elimination procedure is closely related to the cut elimination process in the calculus of structures, and we also get a ``Boolean'' category.

  • 1 :  CALLIGRAMME (INRIA Lorraine - LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domaine : Mathématiques/Logique
    Informatique/Logique en informatique
  • Mots-clés : Proof Nets – Classical Logic – Normal Forms of Proofs – Sequent Calculi – Cut Elimination – Curry-Howard Isomorphism
  • Commentaire : pages 246--261
 
  • hal-00012294, version 1
  • oai:hal.archives-ouvertes.fr:hal-00012294
  • Contributeur : 
  • Soumis le : Mercredi 19 Octobre 2005, 13:30:09
  • Dernière modification le : Jeudi 20 Octobre 2005, 10:27:45