The Size of Interpolants in Modal Logics
This work provides a systematic complexity analysis of interpolant sizes in modal logics, establishing a dichotomy between tabular and non-tabular logics for researchers in logic and computational complexity.
The paper investigates the size of Craig interpolants, uniform interpolants, and strongest implicates in modal logics. It shows that for tabular modal logics, these can be reduced to propositional logic, implying polynomial size iff NP ⊆ P/poly, while for non-tabular logics, an unconditional exponential lower bound holds.
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.