Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Extensions of K5: Proof Theory and Uniform Lyndon Interpolation

Iris van der Giessen, Raheleh Jalali, Roman Kuznets

TL;DR

The paper addresses the uniform Lyndon interpolation property (ULIP) for the normal modal logics built on $K5$ and its extensions, introducing layered sequent calculi to support a constructive ULIP proof. The approach yields complexity-optimal decision procedures—co-NP—for all logics and provides the first syntactic ULIP proof for $K5$, using model-theoretic techniques such as bisimulation modulo literals to certify interpolants. Key contributions include a modular, proof-theoretic method that derives UIP/ULIP for multiple logics and an algorithm to extract uniform Lyndon interpolants syntactically from proof search. The work has practical impact for automated reasoning and knowledge representation by enabling explicit, polarity-respecting interpolants.

Abstract

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.

Extensions of K5: Proof Theory and Uniform Lyndon Interpolation

TL;DR

The paper addresses the uniform Lyndon interpolation property (ULIP) for the normal modal logics built on and its extensions, introducing layered sequent calculi to support a constructive ULIP proof. The approach yields complexity-optimal decision procedures—co-NP—for all logics and provides the first syntactic ULIP proof for , using model-theoretic techniques such as bisimulation modulo literals to certify interpolants. Key contributions include a modular, proof-theoretic method that derives UIP/ULIP for multiple logics and an algorithm to extract uniform Lyndon interpolants syntactically from proof search. The work has practical impact for automated reasoning and knowledge representation by enabling explicit, polarity-respecting interpolants.

Abstract

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.
Paper Structure (3 sections, 2 theorems, 2 equations, 1 figure, 3 tables)

This paper contains 3 sections, 2 theorems, 2 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Layered Sequents

Key Result

theorem 1

Any normal modal logic containing ${\sf K5}$ is sound and complete w.r.t. a class of finite Euclidean Kripke frames $(W, R)$ of one of the following forms: $(a)$$W = \{\rho\}$ consists of a singleton root and $R=\varnothing$, $(b)$ the whole $W$ is a cluster (any world can be considered its root), o

Theorems & Definitions (7)

  • definition 1: Logic ${\sf K5}$
  • definition 2: Kripke semantics
  • theorem 1: nag
  • definition 3: UIP and ULIP
  • theorem 2
  • proof
  • definition 4: Layered sequents