hal-00012294, version 1
Naming Proofs in Classical Propositional Logic
(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 :
- 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
- http://hal.archives-ouvertes.fr/hal-00012294
- 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


Exporter