关于 Maslov 类 $\overline{\text{K}}$ 的复杂度

Maslov 类 $\overline{\text{K}}$ 是已知具有可判定满足性问题的第一阶逻辑的表达丰富片段，其准确复杂度至今未被确立。我们证明 $\overline{\text{K}}$ 拥有指数大小的模型属性，因其满足性问题为 NExpTime-complete。此外，我们获得了文献中相关片段的新的复杂度结果，并提出了一个新的可判定的均匀一维片段扩展（无等号）。我们的方法涉及针对 $\overline{\text{K}}$ 的满足性游戏以及悖论性锦标图的新颖应用。