We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.

翻译：我们引入一种称为分层相继式演算的Gentzen式框架，用于处理模态逻辑K5及其扩展系统KD5、K45、KD45、KB5和S5，旨在研究均匀林登插值性质（ULIP），该性质蕴含均匀插值性质和林登插值性质。我们为所有逻辑系统获取了复杂度最优的判定过程，并给出了K5的ULIP构造性证明——据我们所知，这是首个此类语法证明。为验证插值项的正确性，我们采用模型论方法，特别是基于文字的双模拟技术。