Number of the records: 1
Uniform interpolation via nested sequents and hypersequents
- 1.
SYSNO ASEP 0582406 Document Type V - Research Report R&D Document Type The record was not marked in the RIV Title Uniform interpolation via nested sequents and hypersequents Author(s) Van Der Giessen, I. (NL)
Jalali, Raheleh (UIVT-O)
Kuznets, R. (AT)Issue data Cornell: Cornell University, 2021 Series arXiv.org e-Print archive Series number arXiv:2105.10930 Number of pages 24 s. Publication form Online - E Language eng - English Country US - United States DOI 10.48550/arXiv.2105.10930 Annotation 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. We then use the know-how developed for nested sequents to apply the same method to hypersequents and obtain the first direct proof of uniform interpolation for S5 via a cut-free sequent-like calculus. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents and hypersequents also uses semantic notions, including bisimulation modulo an atomic proposition. Workplace Institute of Computer Science Contact Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Year of Publishing 2024 Electronic address https://arxiv.org/abs/2201.05106
Number of the records: 1