TY - GEN
T1 - Symmetric normalisation for intuitionistic logic
AU - Guenot, Nicolas
AU - Straßburger, Lutz
PY - 2014/1/1
Y1 - 2014/1/1
N2 - 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.
AB - 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.
KW - Cut elimination
KW - Deep Inference
KW - Intuitionistic Logic
U2 - 10.1145/2603088.2603160
DO - 10.1145/2603088.2603160
M3 - Conference contribution
AN - SCOPUS:84905966882
SN - 9781450328869
T3 - Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
BT - Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
PB - Association for Computing Machinery
T2 - Joint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014
Y2 - 14 July 2014 through 18 July 2014
ER -