补全图片：带有逆向操作的分级模态逻辑的复杂性
摘要：关于传统帧类的分级模态语言的局部和全局可满足性问题的复杂性已经进行了完整的分类。所谓的“传统”帧类是指那些由反身性、序列性、对称性、传递性和欧几里德性质的任何正组合所表征的帧类。在本文中，我们填补了具有分级逆模态的分级模态语言类的分类中存在的缺漏。特别地，我们在欧几里德帧类上展示了该语言的NExpTime完备性，从而表明在这个帧类上，考虑的语言比没有分级模态或没有逆模态的语言更难。我们还考虑了不允许分级逆模态，但仍允许基本逆模态的变体。对于这个变体，我们最重要的结果是确认了一个早期的猜想，即它在传递帧上是可判定的。这与具有分级逆模态的语言的不可判定性形成了对比。
作者：Bartosz Bednarczyk, Emanuel Kiero''nski, Piotr Witkowski
论文ID：1812.04413
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22