Symmetric normalisation for intuitionistic logic

Nicolas Guenot; Lutz Straßburger

doi:10.1145/2603088.2603160

Symmetric normalisation for intuitionistic logic

Nicolas Guenot, Lutz Straßburger

Programming Logic and Semantics

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	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
Editors	Thomas A. Henzinger, Dale Miller
Number of pages	10
Publisher	Association for Computing Machinery
Publication date	12 Sept 2014
Pages	45-55
ISBN (Print)	978-1-4503-2886-9
DOIs	https://doi.org/10.1145/2603088.2603160
Publication status	Published - 12 Sept 2014

Keywords

Deep inference
Intuitionistic logic
Cut elimination

Access to Document

10.1145/2603088.2603160

http://doi.acm.org/10.1145/2603088.2603160

Cite this

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

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

@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, 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",

}

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

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 chapter › Article in proceedings › Research › peer-review

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

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 -

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 doi: 10.1145/2603088.2603160

Symmetric normalisation for intuitionistic logic

Abstract

Keywords

Access to Document

Fingerprint

Cite this