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 -