Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Size of Interpolants in Modal Logics

Balder ten Cate, Louwe Kuijer, Frank Wolter

TL;DR

This paper investigates how large Craig interpolants, uniform interpolants, and strongest implicates can be in modal logics, establishing a dichotomy: for tabular logics, these interpolants can be reduced to propositional interpolants in polynomial time, yielding propositional-size bounds, while for a broad class of non-tabular logics containing or contained in $S4$ or $GL$ there are unconditional exponential lower bounds on their sizes. The main contributions include a poly-time reduction from strongest $L(\sigma)$-implicates (and Craig/uniform interpolants when CIP holds) to propositional uniform interpolants, and a corresponding bound transfer to Craig interpolants; a general exponential lower bound for non-tabular logics; and a counterexample Alt_1 showing the dichotomy does not extend to all normal modal logics. The results apply to normal and quasi-normal modal logics with a single modal operator (extensible to polymodal cases) and yield tight size bounds for logics like $K$, $K4$, $S4$, $Grz$, $GL$, and $S5$, with explicit exponential upper bounds and proven optimality. The paper also outlines a broader landscape of interpolant theory in modal logic and provides detailed proofs and constructions in the appendices.

Abstract

We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP $\subseteq$ P$_{/\text{poly}}$. The reduction also holds for Craig interpolants and uniform interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or GL we obtain the following dichotomy: tabular logics have ``propositionally sized'' interpolants while for non-tabular logics an unconditional exponential lower bound holds.

The Size of Interpolants in Modal Logics

TL;DR

This paper investigates how large Craig interpolants, uniform interpolants, and strongest implicates can be in modal logics, establishing a dichotomy: for tabular logics, these interpolants can be reduced to propositional interpolants in polynomial time, yielding propositional-size bounds, while for a broad class of non-tabular logics containing or contained in or there are unconditional exponential lower bounds on their sizes. The main contributions include a poly-time reduction from strongest -implicates (and Craig/uniform interpolants when CIP holds) to propositional uniform interpolants, and a corresponding bound transfer to Craig interpolants; a general exponential lower bound for non-tabular logics; and a counterexample Alt_1 showing the dichotomy does not extend to all normal modal logics. The results apply to normal and quasi-normal modal logics with a single modal operator (extensible to polymodal cases) and yield tight size bounds for logics like , , , , , and , with explicit exponential upper bounds and proven optimality. The paper also outlines a broader landscape of interpolant theory in modal logic and provides detailed proofs and constructions in the appendices.

Abstract

We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP P. The reduction also holds for Craig interpolants and uniform interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or GL we obtain the following dichotomy: tabular logics have ``propositionally sized'' interpolants while for non-tabular logics an unconditional exponential lower bound holds.

Paper Structure

This paper contains 2 sections, 6 theorems, 1 equation, 1 figure, 1 table.

Table of Contents

  1. Overview
  2. Preliminaries

Key Result

Theorem 1

Let $L$ be a tabular quasi-normal modal logic. We can associate to each signature $\sigma$ of propositional variables a companion signature $\widehat{\sigma}$ such that there are poly-time translations such that for every modal formula $\varphi$ and every uniform $\widehat{\tau}$-interpolant $\psi$ of $tr_L(\varphi)$ in propositional logic, $rt_L(\psi)$ is a strongest $L(\tau)$-implicate for $\va

Figures (1)

  • Figure 1: Landscape of non-tabular, pre-tabular, and tabular normal modal logics. To keep the figure simple, not all inclusion relations that hold between the given logics are indicated with edges. The failure of CIP for $\text{EQ}_n$ and for $\text{Alt}_n$ holds for $n>2$. Logics are defined formally in Section \ref{['sec:prelim']} and pointers to the literature and proofs are supplied in Section \ref{['main:notions']} and Appendix \ref{['sec:smallproofs']}.

Theorems & Definitions (6)

  • Theorem 1
  • Corollary 2
  • Theorem 3
  • Corollary 4
  • Theorem 5
  • Theorem 6