一句话：通过翻译与 tableau 统一经典模态逻辑及其递归扩展的复杂度，并给出通用的 2EXP 可满足性上界。
本文研究经典模态逻辑及其带不动点算子扩展的复杂度，重点针对多智能体逻辑。作者通过建立这些逻辑与 μ-演算、模态逻辑之间的翻译，转移已知的上界与下界，从而得到一系列复杂度结果。基于 Kozen 的 μ-演算 tableau 以及 Fitting 和 Massacci 的模态逻辑 tableau，文中还引入终止与非终止 tableau 系统，并用 μ-演算公式刻画这些 tableau，将各逻辑的可满足性问题归约到 μ-演算的可满足性，最终给出通用的 2EXP 上界。
This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $\mu$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $\mu$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $\mu$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $\mu$-calculus, resulting in a general 2EXP upper bound for satisfiability testing.
@article{paperbot2735,
title = {Complexity results for modal logic with recursion via translations and tableaux},
author = {Luca Aceto and Antonis Achilleos and Elli Anastasiadi and Adrian Francalanza and Anna Ingólfsdóttir},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:14)2024}
}