Complexity results for modal logic with recursion via translations and tableaux
CoRR(2023)
摘要
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 μ-calculus and modal
logic, which allow us to transfer known upper and lower bounds. We also use
these translations to introduce a terminating tableau system for the logics we
study, based on Kozen's tableau for the μ-calculus, and the one of Fitting
and Massacci for modal logic. Finally, we show how to encode the tableaux we
introduced into μ-calculus formulas. This encoding provides upper bounds
for the satisfiability checking of the few logics we previously did not have
algorithms for.
更多查看译文
关键词
modal logic,complexity,recursion,translations
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要