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.

翻译：我们系统研究了（拟）正规模态逻辑中Craig插值项、统一插值项及最强蕴含式的大小问题。主要上界表明：对于表格型模态逻辑，最强蕴含式的计算可在多项式时间内归约为经典命题逻辑中的统一插值项计算。因此，其多项式有向无环图大小当且仅当NP ⊆ P/poly。若表格型模态逻辑满足Craig插值性质，该归约同样适用于Craig插值项与统一插值项。主要下界揭示了几乎覆盖所有非表格型标准正规模态逻辑的Craig插值项与最强蕴含式的无条件指数下界。对于包含或包含于S4或GL的正规模态逻辑，我们得到如下二分结构：表格型逻辑具有“命题规模”的插值项，而非表格型逻辑则存在无条件指数下界。