Symmetric Normalisation for Intuitionistic Logic

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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01092105
Contributor : Lutz Straßburger <>
Submitted on : Monday, December 8, 2014 - 12:27:45 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Document(s) archivé(s) le : Monday, March 9, 2015 - 11:06:17 AM

File

sjs2-final-with-appendix.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Nicolas Guenot, Lutz Straßburger. Symmetric Normalisation for Intuitionistic Logic. CSL-LICS 2014, Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603160⟩. ⟨hal-01092105⟩

Share

Metrics

Record views

200

Files downloads

91