Uniform interpolation via nested sequents

Iris van der Giessen; Raheleh Jalali; Roman Kuznets

doi:10.1007/978-3-030-88853-4_21

Uniform interpolation via nested sequents

Iris van der Giessen, Raheleh Jalali, Roman Kuznets^*

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Downloads (Pure)

Abstract

A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics K, D, and T. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents also uses semantic notions, including bisimulation modulo an atomic proposition.

Original language	English
Title of host publication	Logic, Language, Information, and Computation
Subtitle of host publication	27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings
Publisher	Springer
Pages	337-354
Number of pages	18
ISBN (Electronic)	9783030888534
ISBN (Print)	9783030888527
DOIs	https://doi.org/10.1007/978-3-030-88853-4_21
Publication status	Published - 6 Oct 2021

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13038
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

Uniform interpolation
Modal logic
Nested sequents

Access to Document

10.1007/978-3-030-88853-4_21

vdGiessenI2023Logic_AAM
This version of the article has been accepted for publication in WoLLIC 2021, Lecture Notes in Computer Science, vol. 13038, after peer review and is subject to Springer Nature’s AM terms of use, but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: https://doi.org/10.1007/978-3-030-88853-4_21
Accepted author manuscript, 446 KBLicence: Other (please specify with Rights Statement)

Cite this

@inproceedings{9e3b059781ba493089c93a0c44d47f8a,

title = "Uniform interpolation via nested sequents",

abstract = "A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics K, D, and T. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents also uses semantic notions, including bisimulation modulo an atomic proposition.",

keywords = "Uniform interpolation, Modal logic, Nested sequents",

author = "{van der Giessen}, Iris and Raheleh Jalali and Roman Kuznets",

year = "2021",

month = oct,

day = "6",

doi = "10.1007/978-3-030-88853-4_21",

language = "English",

isbn = "9783030888527",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "337--354",

booktitle = "Logic, Language, Information, and Computation",

}

Uniform interpolation via nested sequents. / van der Giessen, Iris; Jalali, Raheleh; Kuznets, Roman.
Logic, Language, Information, and Computation: 27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings. Springer, 2021. p. 337-354 (Lecture Notes in Computer Science; Vol. 13038).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Uniform interpolation via nested sequents

AU - van der Giessen, Iris

AU - Jalali, Raheleh

AU - Kuznets, Roman

PY - 2021/10/6

Y1 - 2021/10/6

N2 - A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics K, D, and T. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents also uses semantic notions, including bisimulation modulo an atomic proposition.

AB - A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics K, D, and T. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents also uses semantic notions, including bisimulation modulo an atomic proposition.

KW - Uniform interpolation

KW - Modal logic

KW - Nested sequents

U2 - 10.1007/978-3-030-88853-4_21

DO - 10.1007/978-3-030-88853-4_21

M3 - Conference contribution

SN - 9783030888527

T3 - Lecture Notes in Computer Science

SP - 337

EP - 354

BT - Logic, Language, Information, and Computation

PB - Springer

ER -

Uniform interpolation via nested sequents

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this