模态逻辑中插值器的大小

我们系统性地调查了Craig插值、统一插值和最强蕴含式在（准）正规模态逻辑中的大小。我们的主要上界表明，对于表格模态逻辑，最强蕴含式的计算可在多项式时间内归约到经典命题逻辑中的统一插值计算。因此它们的 dag 大小当且仅当 NP 包含在 P/poly 中。该归约也适用于Craig插值和统一插值，如果该表格模态逻辑具有Craig插值属性。我们的主要下界显示，对于几乎所有非表格标准正规模态逻辑，Craig插值和最强蕴含式的大小都具有指数下界。对于包含或包含 S4 或 GL 的正规模态逻辑，我们获得以下二分法：表格逻辑具有“命题大小”插值，而对于非表格逻辑则存在不可避免的指数下界。