Symmetric Normalisation for Intuitionistic Logic

Nicolas Guenot 1 Lutz Straßburger 2, 3
3 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first is a direct adaptation of the standard sequent calculus to the deep inference setting, and we describe a procedure for cut elimination, similar to the one from the sequent calculus, but using a non-local rewriting. The second system is the symmetric completion of the first, as normally given in deep inference for logics with a DeMorgan duality: all inference rules have duals, as cut is dual to the identity axiom. We prove a generalisation of cut elimination, that we call symmetric normalisation, where all rules dual to standard ones are permuted up in the derivation. The result is a decomposition theorem having cut elimination and interpolation as corollaries.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01092105
Contributeur : Lutz Straßburger <>
Soumis le : lundi 8 décembre 2014 - 12:27:45
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : lundi 9 mars 2015 - 11:06:17

Fichier

sjs2-final-with-appendix.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Nicolas Guenot, Lutz Straßburger. Symmetric Normalisation for Intuitionistic Logic. CSL-LICS 2014, Jul 2014, Vienna, Austria. 〈http://lics.rwth-aachen.de/csl-lics14/〉. 〈10.1145/2603088.2603160〉. 〈hal-01092105〉

Partager

Métriques

Consultations de la notice

147

Téléchargements de fichiers

59