PSPACE Reasoning for Graded Modal Logics
本文给出了一个判定阶化模态逻辑Gr（K_R）可满足性的PSPACE算法，它是命题模态逻辑K_R通过计数表达式的自然推广，在知识表示领域中起着重要作用。该算法采用了tableaux的方法，是第一个已知的算法，满足问题的复杂性下限。因此，我们准确地解决了问题的复杂性，并驳斥了ExpTime-hardness猜想。我们将结果推广到逻辑Gr（K_（R \cap I））上，用逆关系和可达关系的交扩充了Gr（K_R）.这建立了一种“理论基准”，所有算法方法都可以根据它来衡量。
2000-05-08 cs.AI cs.CC cs.DS
PSPACE-completeness of bimodal transitive weak-density logic
本文利用窗口方法并结合双模态K算法，证明在弱密度逻辑中添加传递性后，其可满足性与有效性均为PSPACE完全。
2025-07-20 cs.LO
The Complexity of Temporal Logic over the Reals
本文证明了实数时间上具有until和since连接词的时态逻辑的判定问题是PSPACE完全的。
1999-10-13 cs.CC cs.LO
DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE
证明了命题控制动态逻辑DL-PA和命题控制委托联合逻辑DCL-PC的模型检验和可满足性问题都是在PSPACE中进行的。我们解释了为什么（Balbiani，Herzig，Troquard，2013）中提出的DL-PA的模型检验问题的EXPTIME-硬度证明是错误的。我们还解释了为什么在PSPACE的成员证明的模型检验问题的DCL-PC（van der Hoek，Walther，Wooldridge，2010）是错误的。
2014-11-28 cs.LO
Deciding FO-rewritability of regular languages and ontology-mediated queries in Linear Temporal Logic
我们关心的问题是，确定的数据复杂度回答本体中介查询（OMQ）制定的线性时序逻辑LTL在（Z，<），并决定是否是一个FO（<）-查询，可能与一些额外的谓词。首先，我们观察到，与正则语言的电路复杂性和FO可定义性一致，AC^0、ACC^0和NC^1中的OMQ回答分别与使用一元谓词x \equiv 0（mod n）的FO（<，\equiv）可重写性、使用关系原语递归的FO（<，MOD）可重写性和FO（RPR）可重写性一致。我们证明了，与已知的识别正则语言的FO（<）-可定义性的PSPACE-完全性类似，判定FO（<，\equiv）-和FO（<，MOD）-可定义性也是\PSPACE -完全的（除非ACC^0 = NC^1）。然后，我们使用这个结果表明，决定FO（<），FO（<，\equiv）和FO（<，MOD）的可重写性的LTL OMQ是EXPSPACE完全的，这些问题成为PSPACE完全的OMQ与线性霍恩本体和原子查询，以及积极的查询的情况下，FO（<）和FO（<，\equiv）的可重写性。此外，我们考虑了具有二进制子句本体的OMQ的FO（<）-可重写性，并确定了OMQ类，确定其是PSPACE-，Pi_2^p-和coNP-完全的。
2023-01-09 cs.CC cs.LO
The Complexity of Poor Man's Logic
受描述逻辑的启发，我们研究了如果我们只允许从字面量、$\wedge$、$\Diamond$和$\Box$构建公式，模态可满足性问题的复杂性会发生什么。以前，唯一已知的结果是K的可满足性问题的复杂性从PSPACE完全下降到coNP完全（Schmidt-Schauss和Smolka，1991和Donini等人，1992年）。在本文中，我们表明，不是所有的模态逻辑的行为像K。特别是，我们表明，可满足性问题的复杂性，其中每个世界至少有一个继任者的帧下降PSPACE-完整的P，但相比之下，可满足性问题的类的帧中，每个世界最多有两个继任者仍然PSPACE-完整的。作为后者的结果的推论，我们也解决了开放的问题，从Donini等人。描述逻辑的复杂性分类（Donini等人，1997年）。在最后一节中，我们对K的可满足性问题的复杂性进行了分类，对于算子集的所有其他限制。
2005-12-24 cs.CC cs.LO
Generalized Modal Satisfiability
众所周知，模态可满足性是PSPACE完备的（Ladner 1977）。然而，如果我们限制所使用的命题运算符的集合，复杂度可能会降低。请注意，存在无限数量的命题运算符，因为命题运算符只是一个布尔函数。我们对命题算子的每一个有限集合的模态可满足性的复杂性进行了完全分类，即，与以前工作相比，我们对无限数量的问题进行了分类。我们表明，根据命题算子的集合，模态可满足性是PSPACE-完全的，CONP-完全的，或在P.我们得到这个分割不仅为模态公式，但也为他们更简洁的表示使用模态电路。我们考虑了单模态和多模态的情况，并研究了有效性的对偶问题。
2008-04-17 cs.CC cs.LO
Closing a Gap in the Complexity of Refinement Modal Logic
精化模态逻辑（Refinement Modal Logic，RML），最近由Bozzelli等人提出，模态逻辑是经典模态逻辑的扩展，它允许人们对变化的模型进行推理。在本文中，我们研究与此逻辑相关的计算复杂性问题，解决了许多悬而未决的问题。具体来说，我们研究的复杂性，满足性的存在片段的RML，Bozzelli，范Ditmarsch和Pinchinat提出的问题。我们的主要结果是一个紧PSPACE上界这个问题，我们通过引入一个新的表系统实现。作为一个直接的后果，我们得到了严格的表征的复杂性RML可满足的任何固定数量的交替的细化量词。此外，通过一个简单的减少，我们建立RML的模型检验问题是PSPACE完全的，即使是一个单一的量词的公式。
2013-09-20 cs.CC cs.LO
The complexity of admissible rules of Łukasiewicz logic
研究了无穷值命题逻辑中推理规则的可容许性的计算复杂性。在[13]中，证明了在PSPACE中可检验的是在PSPACE中的可容许性。我们确定这个结果是最优的，即，可容许规则是PSPACE完备的。与此相反，可导出的规则是coNP-完全的。
2012-02-28 cs.CC cs.LO math.LO
Shallow Models for Non-Iterative Modal Logics
DFKI-Lab Bremen（不来梅德国人工智能研究中心实验室）；Universität Bremen（不来梅大学）；Imperial College London（帝国理工学院）
用于建立模态逻辑PSPACE界的方法大致可以分为两类：语法驱动方法建立了可以在多项式空间中执行的穷举证明搜索，而语义方法直接构建浅层模型。在本文中，我们遵循后一种方法，并建立通用PSPACE界的一个大的和异构类的模态逻辑的共代数框架。特别是，没有完整的公理化的逻辑审查是必要的。这不仅在概念上补充了我们先前的句法方法，而且还涵盖了各种各样的新例子，这些新例子很难通过纯粹的句法手段加以利用。除了重新证明已知的复杂性界限的各种各样的结构不同的逻辑，我们应用我们的方法来获得以前未知的PSPACE界限Elgesem的逻辑机构和分级模态逻辑自反框架。
2008-04-03 cs.AI cs.CC cs.LO
The complexity of linear-time temporal logic over the class of ordinals
我们考虑的时间逻辑与因为和直到模态。这种时态逻辑在表达上等价于一阶逻辑的坎普定理。我们证明了它有一个PSPACE-完全可满足性问题的序数类。在我们的证明的后果，我们表明，给定的代码的一些可数序数α和一个公式，我们可以在PSPACE中决定是否有一个模型的α公式。为了证明这些结果，我们引入了一类简单的序数自动机，作为表达Büchi序数自动机。通过将时态逻辑的可满足性问题归结为简单有序自动机的非空性问题，得到了时态逻辑可满足性问题的PSPACE上界。
2010-12-21 cs.LO
Non-Expansive Fuzzy Coalgebraic Logic
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）
本文提出非扩展共代数模糊模态逻辑，提供PSpace中可判定的标准，并为多种定量模态逻辑提供新的PSpace上界。
2026-02-12 cs.LO
Yet another argument in favour of NP=CoNP
本文给出了NP=CoNP$的另一个证明。在上一篇文章中，我们证明了NP=PSPACE，并且由此我们可以立即得出NP=CoNP的结论。前一个证明展示了如何对所有纯蕴涵极小逻辑重言式获得多项式和多项式时间可检验的Dag样证明。从最小蕴涵逻辑是PSPACE完备的这一事实出发，证明了NP=PSPACE。这是NP=CoNP的第一个证明，使用了序列演算最小蕴涵逻辑证明高度的Hudelmaier线性上限。在NP=PSPACE证明的附录中，我们观察到我们不需要使用Hudelmaier上界，因为任何图的非Hamilton性的任何证明都是线性上界的。利用非哈密顿性的CoNP-完备性，得到了NP=CoNP，作为第一个证明的推论.在这篇文章中，我们展示了CoNP=NP的第三个证明，还提供了多项式大小和多项式可验证的证书。它们是从正常的自然演绎证明中生成的，线性高度上限也是如此，通过去除冗余，即，重复的部分。重复部分的存在性是纯蕴涵最小逻辑中超多项式证明族的冗余定理的一个推论。这是强制性的阅读至少两个以前的文章，以获得这里提出的证明的细节。这篇文章证明了冗余定理，这篇文章展示了如何删除正常自然演绎证明的重复部分，以获得最小蕴涵逻辑重言式的多项式Dag证书。
2020-12-28 cs.CC cs.LO
Recursive windows for grammar logics of bounded density
本文推广有限窗口提出递归窗口方法，研究有界密度多模态逻辑，证明其可满足性问题是 PSPACE-完全的，并证明密度单模态逻辑属于 para-PSPACE。
2025-08-08 cs.LO
Rules with parameters in modal logic II
分析了传递模态逻辑中带参数的可容许性和可统一性的计算复杂性。簇可扩展（clx）逻辑类在本系列文章的第一部分中介绍过。我们完全分类的复杂性，统一性或不容许在任何clx逻辑是完整的$Σ^{\exp}_2$，NEXP，coNEXP，PSPACE，或$Π^p_2$。除了允许任意参数的主要情况外，我们还考虑了由常数约束的参数数量的限制问题，以及无参数的情况。我们的上界是特定的CLX逻辑，但我们也包括类似的结果有界的深度和宽度的逻辑。相比之下，我们的下限是非常普遍的：它们适用于一类所有的传递逻辑，其框架允许某些有限子帧的发生。我们还讨论了可导性复杂性的基本问题：对于每个clx逻辑，它是coNP完全的或PSPACE完全的。特别是，我们证明了PSPACE-硬度的可导性广泛的传递逻辑，包括所有的逻辑与析取属性。
2020-05-03 cs.LO math.LO
On the Complexity of Dynamic Epistemic Logic
尽管动态认知逻辑（DEL）是一个很有影响力的逻辑框架，用于表示和推理信息变化，但很少有人知道其相关决策问题的计算复杂性。事实上，我们只知道，对于公告逻辑，一个片段的DEL，可满足性问题和模型检查问题分别是PSPACE-完全的，并在P.我们有助于填补这一空白，证明了事件模型的DEL语言，模型检查问题，令人惊讶的是，PSPACE-完全的。此外，我们证明了可满足性问题是NEXPTIME-完全的。在此基础上，我们给出了一个可靠的、完备的判定可满足性问题的表方法。
2013-10-23 cs.LO
Computational Aspects of Dependence Logic
本文主要研究模态依赖逻辑.它是由Jouko Vääanänen在2007年引入的，作为一阶的扩展（分别为。模态）逻辑的依赖运算符=（）。一阶（resp.）命题）变量x_1，...，x_n，=（x_1，...，x_n）直观地说明x_n的值由x_1，.，x_n-1。我们认为片段的模态依赖逻辑通过限制允许模态和命题连接词的集合。我们对这些片段的可满足性和模型检查问题的复杂性进行了分类。对于可满足性，我们获得了从P over NP，Sigma_P^2和PSPACE到NEXP的复杂度，而对于模型检查，我们只根据它们的易处理性对片段进行分类，即我们在P中显示NP-完全性或包含性。对于这个扩展，我们再次分类的复杂性模型检查问题的片段。在这里，我们获得了从P over NP和coNP到PSPACE的复杂度。最后，我们分析了一阶依赖逻辑、独立友好逻辑及其二元片段。我们证明了两个变量的依赖逻辑的可满足性是NEXP-完全的，而两个变量的独立友好的逻辑，它是不可判定的，并使用这一点来证明，后者也比前者更有表现力。
2012-06-20 cs.CC cs.LO
Proof equivalence in MLL is PSPACE-complete
MLL证明等价是判断乘法线性逻辑中的两个证明是否通过一系列推理置换而相关的问题。它也被称为星自治范畴的词问题。以前的工作已经表明，这个问题是相当于一个重新布线问题的证明网络，这是不规范的充分MLL由于存在的两个单位。从最近的工作重新配置问题，在本文中，它表明，MLL证明等价是PSPACE完全的，使用减少不确定性约束逻辑。结果的一个重要后果是，一个令人满意的概念MLL与单位的证明网的存在被排除（在目前的复杂性假设）。PSPACE-硬度的结果扩展到等价的范式在MELL没有单位，指数的削弱规则诱导一个类似的重布线问题。
2016-03-01 cs.LO
Parameterized complexity of n-dense modal logics
University of Toulouse - IRIT - CNRS（图卢兹大学 - IRIT - 法国国家科学研究中心）
本文研究了n-密集模态逻辑的可满足性问题复杂度，通过参数化复杂度分析证明其属于para-PSPACE，并引入递归窗口工具进行扩展。
2026-04-13 cs.LO
Complexity Jumps In Multiagent Justification Logic Under Interacting Justifications
证明逻辑（英语：Logic of Proofs），LP，及其后继者，证明逻辑（英语：Justification Logic），是模态逻辑对认识论方法的一种改进，其中考虑了证明/证明。在2000年，库兹涅茨证明了LP的可满足性是在多项式层次的第二层，这一结果已经成功地重复了所有其他单智能体证明逻辑的复杂性是已知的。我们引入了一个家庭的多代理的理由逻辑与代理之间的相互作用的理由，通过扩展和推广的两个代理版本的证明的逻辑Yavorskaya在2008年。对于这种多代理的情况，调整了来自单代理调整设置的已知概念和工具。我们目前的Tableau规则和一些初步的复杂性结果。在某些情况下，这些逻辑的可满足性问题仍然在多项式层次的第二层，而对于其他人来说，它是PSPACE或EXP-hard。此外，这个问题变得PSPACE硬，即使某些两个代理逻辑，而有三个代理的EXP硬逻辑。
2014-04-26 cs.LO
On the Computational Complexity of Model Checking for Dynamic Epistemic Logic with S5 Models
Institute for Logic, Language and Computation University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）
动态认知逻辑（DEL）是一个逻辑框架，用于表示和推理多个代理的知识变化。在这个框架中的一个重要的计算任务是模型检验问题，这已被证明是PSPACE硬，即使是S5模型和两个代理-在其他功能的存在下，如多点模型。我们回答开放的问题，在文献中这个问题的复杂性，在更受限制的设置。我们提供了一个详细的复杂性分析的模型检验问题的DEL，在那里我们考虑各种组合的限制，如代理的数量，无论是单点或多点的模型，以及是否后置条件允许在更新。特别是，我们证明了这个问题已经是PSPACE困难的（1）一个代理的情况下，多点S5模型，没有后置条件，和（2）两个代理的情况下，只有单点S5模型，没有后置条件。此外，我们还研究了只允许半私有公告作为更新的设置。我们表明，在这种情况下，问题已经是PSPACE-硬时，限制到两个代理和三个命题变量。我们在本文中获得的结果有助于勾勒出确切的边界的限制设置的模型检验问题的DEL是计算上易于处理的。
2020-09-18 cs.AI cs.CC cs.LO
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
IIT Bombay（印度理工学院孟买分校）；MPI-SWS（马克斯·普朗克软件系统研究所）
本文证明多变量单侧区间TPTL的可满足性检验为PSPACE完全，且其表达力严格强于MITL，但检验复杂度更低，通过归约到新的非点式交替定时自动机子类实现。
2023-09-01 cs.CL cs.FL cs.LO
The temporal logic of two-dimensional Minkowski spacetime with slower-than-light accessibility is decidable
我们的工作主要与克里普克框架组成的二维闵可夫斯基时空与非自反可达性关系“可以达到一个慢于光的信号”。我们表明，在基本的时态语言，在这个框架的有效性集是可判定的。然后，我们将其细化为PSPACE完成。在这两种情况下，对应的自反框架的相同结果立即跟随。随着更多的工作，我们获得PSPACE-完整性的有效性的Halpern-Shoham逻辑的时间间隔的两种不同的组合方式在真正的线。
2018-06-26 cs.LO math.LO
A Closer Look at Some Recent Proof Compression-Related Claims
Gordeev和Haeusler [GH 19]认为，极小命题逻辑的每个重言式$ρ$都可以用$|ρ|$中的大小多项式的自然演绎来证明.这建立在Hudelmaier [Hud93]的工作之上，该工作为直觉主义命题逻辑找到了类似的结果，但对于该结果，只有证明的高度是多项式有界的，而不是整体大小。他们通过将Hudelmaier的微积分中的证明转换为Prawitz的自然演绎系统中的等价树型证明，然后将树型证明压缩为等价的DAG型证明，使得高度和基础上的多项式约束意味着整体大小上的多项式约束。然而，我们的论文观察到，这种构造只在最小蕴涵逻辑上进行，我们证明它比他们声称结果的最小命题逻辑弱（见4.2节）。简单地扩展用于覆盖最小命题逻辑的逻辑系统不足以恢复论文的结果，因为它会完全破坏对证明主要结果至关重要的一些定理的证明。在很大程度上依赖于他们的上述工作，Gordeev和Haeusler [GH 20]声称建立NP=PSPACE。论证集中依赖于最小命题逻辑中证明大小的多项式界。由于我们证明了这个界限并没有被他们正确地建立起来，他们所谓的证明并没有正确地建立NP=PSPACE。
2022-12-23 cs.CC cs.LO
The complexity of positive first-order logic without equality
本文研究了在固定的有限结构B上求一阶逻辑无正等同性语句的复杂性。这可以被看作是非均匀量化的约束满足问题QCSP（B）的自然推广。我们引入满射超自同态，并使用它们来证明一个伽罗瓦连接，其特征在于可定义的正等式自由FO。通过代数方法，我们得出一个完整的复杂性分类为我们的问题B范围的大小最多为3的结构。具体来说，每个问题要么是在对数空间中，要么是NP完全的，要么是共NP完全的，要么是P空间完全的。
2010-03-03 cs.CC cs.LO
Complexity of some modal logics of density (extended version)
本文通过选择性过滤论证和类表方法，分别证明了稠密性单模态逻辑的可满足性问题属于$EXPTIME$，以及弱稠密性双模态逻辑的可满足性问题属于$PSPACE$。
2025-07-15 cs.LO
The Complexity of Generalized Satisfiability for Linear Temporal Logic
在1985年的一篇开创性论文中，Sistla和Clarke证明了线性时态逻辑（Linear Temporal Logic，LTL）的可满足性要么是NP-完全的，要么是PSPACE-完全的，这取决于所使用的时态运算符的集合。相反，如果命题算子的集合是有限的，复杂性可能会降低。本文系统地研究了LTL公式在命题算子和时间算子的限制集上的可满足性。因为每个命题算子对应于一个布尔函数，所以存在无穷多个命题算子。为了系统地覆盖它们的所有可能集合，我们使用波斯特格。在它的帮助下，我们确定的计算复杂性的LTL可满足性的所有组合的时间运营商和所有，但两类命题功能。这些无穷多个问题中的每一个都被证明是PSPACE完全的，NP完全的，或者在P中。
2009-03-23 cs.LO
Formula size game and model checking for modal substitution calculus
Mathematics Research Centre, Tampere University（坦佩雷大学数学研究中心）
本文通过公式大小游戏研究了MSC及其扩展的表达能力和模型检验复杂度，证明其与图灵机、mu演算等的复杂度关系，并建立了相关逻辑的复杂度分类。
2026-10-22 cs.LO
Expressivity within second-order transitive-closure logic
二阶传递闭包逻辑SO（TC）是一种表达性声明语言，它捕获了复杂性类PSPACE。它的一元片段MSO（TC）已经允许以自然和优雅的方式表达各种NP困难甚至PSPACE困难的问题。由于SO（TC）提供了一个有吸引力的框架，用于在声明式指定的计算方面表达属性，因此理解语言的不同特征的表达性是很有趣的。本文重点讨论片段MSO（TC），以及纯存在片段SO（2 TC）（E）;在2 TC中，TC算子仅绑定关系变量的元组。我们建立，关于表达能力，SO（2 TC）（E）崩溃到存在一阶逻辑。此外，我们还研究了MSO（TC）与具有计数特征的MSO（TC）的扩展（CMSO（TC））以及与阶不变MSO的关系。我们发现CMSO（TC）和MSO（TC）的表达能力是一致的。此外，我们建立，在一元词汇表，MSO（TC）严格包含顺序不变的MSO。
2018-04-16 cs.LO
Branching-time model checking of one-counter processes
单计数器进程（OCP）是下推进程，只对一元堆栈字母表进行操作。研究了基于OCP的模型检验计算树逻辑（CTL）的计算复杂性。一个PSPACE上界是继承自该问题的模态μ演算。首先，我们分析的周期性行为的CTL在OCP和推导出一个模型检验算法，其运行时间是指数的控制位置和语法概念的公式，我们称之为直到深度。因此，模型检验固定OCP对CTL公式与一个固定的深度，直到在P。这概括了第一作者，Mayr，和到CTL的片段EF的表达复杂性的结果。其次，我们证明了在一定的OCP上，CTL模型检验是PSPACE困难的。第三，我们表明，已经存在一个固定的CTL公式，模型检验的OCP是PSPACE困难的。对于后者，我们使用了复杂性理论的两个结果：（i）将中国余数表示中的自然数转换为二进制表示是在对数空间一致的NC ^1中;（ii）PSPACE是AC ^0-可串行化的。我们证明，我们的方法可以用来回答进一步的开放性问题。
2010-02-03 cs.CC cs.LO
A Simplest Undecidable Modal Logic
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，它们的可满足性问题的复杂性一直是一个活跃的研究领域。我们证明，即使是非常“简单”的模态逻辑可以是不可判定的：我们表明，有一个不可判定的模态逻辑，可以通过限制允许的模型与一阶公式，其中只有全称量词出现。
2011-05-04 cs.CC cs.LO
Model Checking for Modal Dependence Logic: An Approach Through Post's Lattice
在本文中，我们研究了一个扩展版本的模态依赖逻辑，允许任意布尔连接词。模态依赖逻辑最近由Jouko Väänänen通过依赖原子dep（.）扩展模态逻辑而引入。本文研究了模型检验问题的计算复杂性。对于任意布尔函数的完整分类，我们使用Emil Post介绍的Lattice方法。对逻辑语言的所有片段进行这种分类，允许模态$\Diamond$和$\Box$、依赖原子和任意布尔函数的逻辑符号。
2013-03-26 cs.CC cs.LO
Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
我们研究基本模态逻辑，即模态逻辑考虑一阶可定义类的框架。模态逻辑的经典语义允许无限结构，但实际应用往往要求我们将注意力限制在有限结构上。初等模态逻辑的许多可判定性和不可判定性结果分别在一般可满足性和有限可满足性下得到了证明[11，12，16，17]。在本文中，我们表明，有一个原因，我们必须分别处理这两种可满足性-我们证明，有一个通用的一阶公式，定义了一个基本模态逻辑与可判定的（整体）可满足性问题，但不可判定的有限可满足性问题，反之亦然，存在一个普适公式，它定义了一个具有可判定的有限可满足性问题但具有不可判定的一般可满足性问题的初等模态逻辑。
2012-10-09 cs.CC cs.LO
The Completeness Problem for Modal Logic
我们介绍了模态逻辑的完备性问题，并研究其复杂性。对于公式的完备性定义，给定模态逻辑的一个公式，完备性问题询问该公式对于该逻辑是否完备。我们发现，完整性和有效性具有相同的复杂性-除了某些例外，一般来说，没有完整的公式。为了证明上界，我们提出了一个非确定性的多项式时间的过程与预言PSPACE相结合的表格和互模拟测试，并确定公式是否是完整的。
2017-09-19 cs.LO
Residuated Basic Logic II. Interpolation, Decidability and Embedding
证明了剩余基本逻辑$\mathsf{RBL}$的逻辑演算$\mathsf{L_{RBL}}$具有强有限模型性质，并证明了直觉主义逻辑可以嵌入到基本命题逻辑$\mathsf{BPL}$中.因此，$\mathsf{RBL}$是可判定的。证明了剩余基本代数类具有有限可嵌入性，$\mathsf{BPL}$是PSPACE完备的，直觉主义逻辑可以嵌入模态逻辑$\mathsf{K4}$ .
2014-02-24 cs.LO math.LO
Spatial logics with connectedness predicates
我们考虑量化器自由空间逻辑，设计用于定性空间表示和推理在AI中，并扩展它们的手段来表示区域的拓扑连通性和限制其连接组件的数量。我们调查这些逻辑的计算复杂性，并表明，连接性约束可以增加复杂性从NP到PSpace，ExpTime，如果组件计数是允许的，NExpTime。
2010-10-18 cs.LO
Complexity of Łukasiewicz Modal Probabilistic Logics
Aix Marseille Univ, CNRS, LIS（艾克斯-马赛大学，法国国家科学研究中心，信息系统实验室）；The Czech Academy of Sciences, Institute of Computer Science（捷克科学院，计算机研究所）
本文研究了扩展的Łukasiewicz模概率逻辑的复杂性，证明了局部后果问题的两个变种具有PSPACE完全性。
2025-11-27 cs.LO
A Modal Logic for Explaining some Graph Neural Networks
Université de Rennes（雷恩大学）
本文提出一种计数模态出现在线性不等式中的模态逻辑，并证明其与图神经网络可互相转换，且可满足性问题可判定，部分变体属于PSPACE。
2023-07-11 cs.AI cs.LO
Minimal modal logics, constructive modal logics and their relations
提出一族对应经典模态逻辑的极小模态逻辑，通过两种独立但等价的方法定义，并揭示其与构造性模态逻辑CK的紧密关系，进而衍生出一族构造性模态逻辑。
2023-09-05 cs.LO
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
本文提出了一种“模态线性逻辑”，它将直觉模态逻辑S4（IS 4）用线性逻辑来表示，建立了从IS 4到它的Girard翻译的S4-版本。它对模态逻辑的扩展是非-这是微不足道的，因为S4模态和指数模态的简单组合导致两种模态之间的不期望的相互作用。为了解决这个问题，我们引入了一个扩展的直觉乘法指数线性逻辑与模态相结合的S4模态和指数模态，并表明它承认从IS 4的声音翻译。通过Curry-Howard对应，我们进一步得到了Pfenning和Davies为分阶段计算所提出的模态微积分的交互几何机器语义。
2019-04-24 cs.LO
Axiomatization and complexity of modal logic with knowing-what operator on model class K
标准认知逻辑研究的是命题知识，但许多其他类型的知识，如“知道是否”，“知道什么”，“知道如何”，在日常生活中以及学术领域中经常和广泛使用。在王、范的“条件知道什么”中，给出了具有规则“知道那个”算子和“条件知道什么”算子的认识逻辑的公理化。这种逻辑的可判定性和复杂性决定了我们的研究方向。本文将注意力从认知模型转移到任意模型上，从而使问题更加清楚，并给出了任意Kripke模型上具有相同算子的模态逻辑的公理化和表。给定这个逻辑的表，这个逻辑的可满足性问题的复杂性是PSPACE-完全的。
2016-11-25 cs.LO
Propositional modal logic with implicit modal quantification
命题项模态逻辑在具有无限多的可达性关系的Kripke结构上解释，因此语法允许变量索引模态和量化。这种逻辑是不可判定的，我们考虑一个变量自由命题的双模态逻辑与隐量化。因此，$[\forall] α$断言所有可及性关系上的必然性，而$[\exists] α$是某些可及性关系上的经典必然性。该逻辑是与一个自然的互模拟模型的关系，我们表明，该逻辑正是一个两个排序的一阶逻辑的互模拟不变片段。该逻辑很容易被看作是可判定的，并且承认有效公式的完全公理化。此外，决策过程自然地延伸到“捆绑片段”的完整术语模态逻辑。
2018-12-29 cs.LO
From Hybrid Modal Logic to Matching Logic and Back
建立在我们以前的工作混合多元模态逻辑，我们确定模态逻辑等价匹配逻辑，程序规范和验证的逻辑。这提供了一种严格的方法来在两种方法之间传输结果，这对两个系统都有好处。
2019-09-04 cs.LO
Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
Two variable fragment of Term Modal Logic
项模态逻辑（TML）是具有无限多模态的模态逻辑，在模态指数上量化，因此我们可以有$\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$形式的公式。像一阶模态逻辑一样，TML也是“臭名昭著的”不可判定的，在这个意义上，即使是非常简单的片段也是不可判定的。在本文中，我们证明了一个有趣的片段，即两个变量TML的可判定性。这与二变量一阶模态逻辑相反，二变量一阶模态逻辑是不可判定的。
2019-06-27 cs.LO
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
TU Dresden（德累斯顿工业大学）
针对 GL 逻辑在树-超矢列系统 CSGL 中的可判定性证明和 PSPACE 证明搜索算法问题，提出线性化方法，仅构建单分支推导和树矢列，实现 PSPACE 最优复杂度，并提取有限反模型验证算法正确性。
2026-08-11 cs.LO math.LO
Intuitionistic modal logic LIK4 is decidable
Faculty of Arts and Sciences Istanbul Aydın University（伊斯坦布尔阿因大学文理学院）；Faculty of Mathematics and Informatics Sofia University St. Kliment Ohridski（索非亚大学克利门特·奥赫里德斯基数学与信息学院）
本文证明了直觉模态逻辑LIK4的可判定性。
2025-12-04 cs.LO
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
我们提出了一个句法抽象方法，通过使用标准一阶逻辑和命题模态逻辑的定理证明器来推理一阶模态逻辑。
2014-09-12 cs.LO
Explicit non-normal modal logic
针对道义模态的超内涵性问题，本文提出作为非正规模态逻辑超内涵对应物的新型证成逻辑，证明其可靠性与完全性，并研究实现问题。
2023-08-11 cs.LO
Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
我们研究了有限森林上的两个模态逻辑的表达性和计算复杂性，这些模态逻辑配备了算子来推理子模型。逻辑ML（|）用复合运算符扩展了基本模态逻辑ML|而ML（*）包含来自分离逻辑的分离合取 *。虽然这两个算子都是二阶的性质，我们表明，ML（|）与分级模态逻辑GML（在有限树上）一样具有表达性，而ML（*）严格位于ML和GML之间。此外，我们建立了ML（*）的可满足性问题是塔完全的，而ML（|）是（仅）AExpPol-complete。作为一个副产品，我们解决了几个开放的姐妹逻辑，如静态环境逻辑，模态分离逻辑，有限树上的二阶模态逻辑的问题。
2020-07-16 cs.LO
Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK
本研究整合模态逻辑终止表方法与直觉主义模态逻辑IK的有穷框架性质，为FIK和LIK给出更简洁的全新可判定性证明。
2025-03-24 cs.LO
On the Complexity of Team Logic and its Two-Variable Fragment
本文研究了具有团队语义的一阶逻辑的无限制布尔否定扩展--FO（~）逻辑。它最近被证明是可公理化的，但在计算复杂性的问题上还没有得到太多的关注。本文考虑它的二元片段FO 2（~），证明了它的可满足性问题是可判定的，并且对于最近引入的非初等类TOWER（poly）是完全的.此外，我们还对FO（~）的模型检验的复杂性进行了分类，并证明了PSPACE-完备性和ATIME-ALT（exp，poly）-完备性之间的二分法。为了实现下界，我们提出了从模态团队逻辑MTL到FO 2（~）的转换，该转换扩展了从模态逻辑ML到FO 2的众所周知的标准转换。对于上界，我们转换为二阶逻辑的一个片段。
2018-04-13 cs.LO
Counting Computations with Formulae: Logical Characterisations of Counting Complexity Classes
本文提出基于两步语义的定量逻辑，并证明其片段可刻画#P的子类SpanL和TotP，以及FPSPACE和SpanPSPACE，解决了计数问题描述复杂性中的开放问题。
2023-05-16 cs.LO
