Uniform interpolation via nested sequents and hypersequents

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F25%3A00604120" target="_blank" >RIV/67985807:_____/25:00604120 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1093/logcom/exae053" target="_blank" >https://doi.org/10.1093/logcom/exae053</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1093/logcom/exae053" target="_blank" >10.1093/logcom/exae053</a>

Result language

angličtina

Original language name

Uniform interpolation via nested sequents and hypersequents

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Journal of Logic and Computation

ISSN

0955-792X

e-ISSN

1465-363X

Volume of the periodical

35

Issue of the periodical within the volume

6

Country of publishing house

GB - UNITED KINGDOM

Number of pages

23

Pages from-to

exae053

UT code for WoS article

001380316500001

EID of the result in the Scopus database

2-s2.0-105012041251