The Size of Interpolants in Modal Logics

TL;DR

This paper investigates the size of various interpolants in modal logics, establishing polynomial bounds for tabular logics and exponential lower bounds for non-tabular logics, revealing fundamental complexity differences.

Contribution

It provides the first systematic analysis of interpolant sizes in modal logics, including polynomial bounds for tabular logics and exponential lower bounds for non-tabular ones.

Findings

Polynomial-time reduction of strongest implicates to propositional uniform interpolants in tabular modal logics.

Exponential lower bounds on Craig interpolants and strongest implicates in non-tabular modal logics.

Dichotomy in interpolant sizes for modal logics related to S4 and GL.

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 is included in P/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.