ITU

Symmetric normalisation for intuitionistic logic

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

Symmetric normalisation for intuitionistic logic. / Guenot, Nicolas; Straßburger, Lutz.

Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. ed. / Thomas A. Henzinger; Dale Miller. Association for Computing Machinery, 2014. p. 45-55.

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Harvard

Guenot, N & Straßburger, L 2014, Symmetric normalisation for intuitionistic logic. in TA Henzinger & D Miller (eds), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. Association for Computing Machinery, pp. 45-55. https://doi.org/10.1145/2603088.2603160

APA

Guenot, N., & Straßburger, L. (2014). Symmetric normalisation for intuitionistic logic. In T. A. Henzinger, & D. Miller (Eds.), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014 (pp. 45-55). Association for Computing Machinery. https://doi.org/10.1145/2603088.2603160

Vancouver

Guenot N, Straßburger L. Symmetric normalisation for intuitionistic logic. In Henzinger TA, Miller D, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. Association for Computing Machinery. 2014. p. 45-55 https://doi.org/10.1145/2603088.2603160

Author

Guenot, Nicolas ; Straßburger, Lutz. / Symmetric normalisation for intuitionistic logic. Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. editor / Thomas A. Henzinger ; Dale Miller. Association for Computing Machinery, 2014. pp. 45-55

Bibtex

@inproceedings{917e5f124f77421b86aaadd2f1fdd64a,
title = "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.",
keywords = "Deep inference, Intuitionistic logic, Cut elimination",
author = "Nicolas Guenot and Lutz Stra{\ss}burger",
year = "2014",
month = sep,
day = "12",
doi = "10.1145/2603088.2603160",
language = "English",
isbn = "978-1-4503-2886-9",
pages = "45--55",
editor = "Henzinger, {Thomas A.} and Dale Miller",
booktitle = "Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014",
publisher = "Association for Computing Machinery",
address = "United States",

}

RIS

TY - GEN

T1 - Symmetric normalisation for intuitionistic logic

AU - Guenot, Nicolas

AU - Straßburger, Lutz

PY - 2014/9/12

Y1 - 2014/9/12

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 - Deep inference

KW - Intuitionistic logic

KW - Cut elimination

U2 - 10.1145/2603088.2603160

DO - 10.1145/2603088.2603160

M3 - Article in proceedings

SN - 978-1-4503-2886-9

SP - 45

EP - 55

BT - Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014

A2 - Henzinger, Thomas A.

A2 - Miller, Dale

PB - Association for Computing Machinery

ER -

ID: 79278572