Some General Completeness Results for Propositionally Quantified Modal Logics
本文研究命题量化模态逻辑的完全性问题，证明含Barcan模式的正规逻辑在可量化一般框架下强完全，给出公式真值在框架过渡中保持的充分条件，并基于有限多样性得到一类Kripke完全的逻辑及欧几里得框架逻辑的有限公理化。
2024-06-23 cs.LO math.LO
The Polylog-Time Hierarchy Captured by Restricted Second-Order Logic
令$\mathrm{SO}^{\mathit{plog}}$表示二阶逻辑的限制，其中二阶量化在结构的大小中最多为多对数的大小关系上的范围。在这篇文章中，我们调查的问题，这图灵机复杂性类被捕获的布尔查询有序的关系结构，可以表示在这个逻辑。为此，我们定义了一个层次的片段$Σ^{\mathit{plog}}_m$（和$Π^{\mathit{plog}}_m$）定义的公式与交替块的存在和通用的二阶量词在量词前趋范式。我们首先表明，存在片段$Σ^{\mathit{plog}}_1$捕获NPolyLogTime，即布尔查询的类，可以接受的非确定性图灵机与随机访问的时间输入$O((\log n)^k)$的一些$k \ge 0$。使用具有随机访问输入的交替图灵机允许我们还将片段$Σ^{\mathit{plog}}_m$（和$Π^{\mathit{plog}}_m$）表示为具有由交替图灵机接受的最多$m$的二阶量词的交替块的那些布尔查询。因此，$\mathrm{SO}^{\mathit{plog}}$捕获整个多对数时间层次。我们通过数据库理论中的几个问题证明了这种逻辑和复杂性类的相关性。
2018-06-19 cs.LO
On FO2 quantifier alternation over words
我们表明，FO^2[<]中的量词交替层次结构的每一个级别-单词顺序的一阶逻辑的2变量片段-是一种语言。然后，我们使用浓缩等级的概念，一种由Weis和Immerman定义的等级的改进，来产生与量词交替等级交织在一起的变体的可判定等级--并且在理论上与它相等。由此得出，后一等级在一个单位内是可判定的：给定FO^2[<]中的公式alpha，可以有效地计算整数m，使得alpha等价于具有至多m+1个交替量词块的公式，但不等价于仅具有m-1个块的公式。这是一个比FO[<]中的量词交替层次结构更精确的结果，在FO[<]中，除了第一层之外，没有可判定性结果。
2009-04-19 cs.LO
A Modal Characterization of Alternating Approximate Bisimilarity
近年来，交替转移系统被用来描述具有扰动的控制系统及其有限抽象系统。为了捕捉这些系统之间的等价关系，交替近似双相似的概念被引入。本文旨在建立交替近似双相似性的模态特征。此外，基于这一结果，我们提供了一个链接的规范满足控制系统的干扰和他们的有限抽象的样本。
2012-12-19 cs.LO
Ecumenical modal logic
本文扩展Prawitz的普世系统思想至真势K模态，统一经典与直觉主义逻辑连接词，并建立相应的证明论性质。
2020-05-28 cs.LO math.LO
Refinement Modal Logic
Universidad Politécnica de Madrid（马德里理工大学）；LORIA, CNRS – Université de Lorraine（洛林计算机科学与应用数学实验室（法国国家科学研究中心-洛林大学））；University of Western Australia（西澳大利亚大学）；IRISA, University of Rennes（雷恩大学计算机科学与随机系统研究所）
本文提出了{ \em精化模态逻辑}。精化类似于互模拟，不同之处在于从三个关系需求中只需要满足“原子”和“返回”。我们的逻辑包含一个新的操作符“所有”除了标准的模态“框”为每个代理。运算符“all”充当给定模型的所有细化的集合上的量词。作为互模拟量词的一种变体，这个精化运算符或精化量词“all”可以被看作是对一个没有出现在它所约束的公式中的变量进行量化。这种逻辑结合了多智能体模态逻辑的简单性和一元二阶量化的一些能力。我们提出了一个健全的和完整的公理化的多智能体精化模态逻辑。我们还提出了一个扩展的逻辑模态μ演算，和公理化的单代理版本的这个逻辑。例子和应用程序也进行了讨论：软件验证和设计（一套代理也可以被看作是一套行动），并动态认知逻辑。我们进一步给出了详细的结果，可满足性的复杂性，简洁性。
2013-12-25 cs.AI cs.LO
Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics
在过去的几十年里，大量的努力投入到确定一阶逻辑的可判定片段。这种努力产生了，除其他外，两个变量的片段和守卫片段，这取决于对语言公式施加的限制类型。尽管上述逻辑在形式化验证和知识表示等领域取得了成功，但这种一阶片段太弱，无法表达影响网络建模或统计推理所需的最简单的统计约束。在这项工作中，我们研究了这些经典的可判定逻辑与百分比量词的扩展，指定如何频繁的一个公式是满足缩进模型。令人惊讶的是，我们发现，所有提到的可判定的片段成为不可判定下这样的扩展，锐化文献中现有的结果。我们的负面结果补充的决定性的两个变量的守卫片段，甚至更有表现力的计数，即Presburger约束。我们的研究结果可以应用于推断各种模态和描述逻辑，如Presburger模态逻辑与逆向或ALCI，表达基数约束的可判定性。
2021-10-03 cs.LO
On Presburger arithmetic extended with non-unary counting quantifiers
研究扩展了非一元计数量词的Presburger算术，通过量词消去与归约技术证明其满足性在两重指数空间内可判定，并给出不同量词组合下的计算复杂度上界。
2023-07-11 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
LTL with the Freeze Quantifier and Register Automata
一个数据字是一个序列的一个字母从一个有限的字母表和一个元素从一个无限的集合，后者只能比较相等。为了对数据字进行推理，线性时态逻辑通过冻结量词进行扩展，冻结量词将当前字位置的元素存储到寄存器中，用于公式中更深处的相等比较。通过从逻辑转换到带有寄存器的交替自动机，然后转换到计数器可能在任何时候错误地增加的故障计数器自动机，以及从故障和无错误的计数器自动机转换到逻辑，我们获得了一个完整的复杂性表，通过改变时态运算符和寄存器的数量来定义逻辑片段。特别地，具有未来时间算子和1个寄存器的逻辑在有限数据字上是可判定的但不是原始递归的。添加过去时间操作符或多一个寄存器，或切换到无限数据字，会导致不可判定性。
2008-04-03 cs.CC cs.LO
On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts
Institute of Mathematics and Informatics, Bulgarian Academy of Sciences（保加利亚科学院数学与信息学研究所）
本文提出在具有策略上下文的ATL中通过翻译方法处理偏好与量化，以更简洁地表达纳什均衡等博弈解概念，并转化为QCTL进行算法推理。
2026-02-11 cs.LO cs.MA
Logics Meet 2-Way 1-Clock Alternating Timed Automata
本文研究了单时钟交替时间自动机（1-ATA）的扩展，即双向单时钟交替时间自动机（2-Way 1-ATA）。我们证明了具有重置自由循环的2-Way 1-ATA的子类（2-Way 1-ATA-rfl）在表达上等价于用保护度量量词（GQMSO）扩展的MSO[<]。2路1-ATA-rfl（以及因此GQMSO）的空性检查问题通常是不可判定的。我们提出了一个“非准时性”的限制，称为非邻接，2路1-ATA-rfl，也为GQMSO，其中的空（分别满足性）检查成为可判定的。非相邻2路1-ATA是第一类具有交替和2路性的时间自动机，其空性检查是可判定的（并且也具有初等复杂性）。我们还表明，2路1-ATA-rfl，即使与非相邻的限制，可以表达属性是不可识别的使用1-ATA。
2022-02-26 cs.FL cs.LO
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
A Simplest Undecidable Modal Logic
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，它们的可满足性问题的复杂性一直是一个活跃的研究领域。我们证明，即使是非常“简单”的模态逻辑可以是不可判定的：我们表明，有一个不可判定的模态逻辑，可以通过限制允许的模型与一阶公式，其中只有全称量词出现。
2011-05-04 cs.CC cs.LO
A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property
本文证明了一阶模态逻辑捆绑片段中不满足有限模型性质的组合在递增域模型下是可判定的，将原有三分法坍缩为二分法。
2025-06-02 cs.LO
Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations
我们关心的是模态和代数逻辑的公理化问题，对应于各种片段的两个变量的一阶逻辑计数量词。特别是，我们认为模态产品与Diff，命题单峰逻辑的差异运营商。我们证明了二维乘积逻辑Diff x Diff是不可公理化的，但可以被无穷多个Sahlqvist公理公理化.我们还表明，它的“平方”版本（模态对应的替代和平等免费片段的两个变量的一阶逻辑计数为2）是非非线性axiomatisable在Diff x Diff，但可以通过添加无穷多个Sahlqvist公理公理。这些是第一个例子的产品的axiomatisable模态逻辑是不是axiomatisable，但axiomatisable由明确的无限套规范公理。
2020-01-28 cs.LO math.LO
Finite Model Property and Bisimulation for LFD
最近，Baltag和van Benthem arXiv：2103.14946 [cs.LO]引入了一种新的具有局部依赖公式和依赖量词的函数依赖（LFD）可判定逻辑。该语言在依赖模型上进行解释，依赖模型是具有一组可用变量分配的一阶结构对，也称为团队。与依赖模型相关的团队可以被看作是一个标记的转换系统，在这个系统上LFD成为模态逻辑，其中依赖量词成为模态，局部依赖公式被视为特殊原子。在本文中，我们引入适当的互模拟的概念，将LFD（和一些相关的逻辑）表征为一阶逻辑（FOL）的一个片段，并表明它等价于arXiv：2102.10368 [cs.LO]中提出的更标准的互模拟概念，但对于互相似性检查更有效。我们的主要结果是LFD具有有限模型性质（FMP），通过Herwig定理的一个新的应用扩展部分同构。
2021-07-13 cs.LO math.LO
Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
模态公式表示Kripke框架上的一元二阶性质，但在许多重要情况下，它们具有一阶等价物。计算这样的等价物对于逻辑和计算原因都是重要的。另一方面，模态公式的规范性也很重要，因为它意味着用规范公式公理化的逻辑的框架完备性。计算一个模态公式的一阶等价等价物相当于消除二阶量词。二阶量词消去有两种算法：基于约束消解的SCAN算法和基于Ackermann建立的逻辑等价的DLS算法。在本文中，我们介绍了一种新的算法，SQEMA，计算一阶等价物（使用阿克曼引理的模态版本），而且，用于证明规范的模态公式。与SCAN和DLS不同，它直接作用于模态公式，从而避免了Skolemization和随后的unskolemization问题。我们提出的核心算法，并说明它与一些例子。然后，我们证明了它的正确性和规范的所有公式上的算法成功。我们表明，它不仅成功的所有Sahlqvist公式，但也对更大的类的归纳公式，在我们以前的论文中介绍。因此，我们开发了一种纯粹的算法方法来证明模态逻辑中的规范完备性，特别是，建立了模态逻辑中迄今为止最普遍的完备性结果之一。
2006-03-08 cs.LO
Robust Alternating-Time Temporal Logic
本文提出扩展自ATL/ATL*的鲁棒交替时间时序逻辑rATL与rATL*，通过多值语义实现多智能体系统鲁棒策略推理，验证其模型检测与可满足性问题未增加计算复杂度。
2023-07-20 cs.LO
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
本文研究了带计数的两变量一阶逻辑片段中的可定义性与分离问题，证明了在包含逆算子和名义时分离问题不可判定，而去除这些特征时其复杂度降为coNExpTime或2ExpTime完全，并指出可定义性问题通常可多项式归约至有效性问题。
2025-08-15 cs.LO
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
度量时态逻辑（MTL）和时间命题时态逻辑（TPTL）是线性时态逻辑（LTL）的重要实时扩展。在一般情况下，这些扩展的可满足性检查问题是不可判定的，当未来的U和过去的S模态使用。在一个经典的结果中，证明了MTL [U，S]的非准时片段MITL[U，S]的可满足性检验是可判定的，具有EXPSPACE完全复杂性。鉴于这种非准时性的概念在TPTL[U，S]的情况下不能恢复可判定性，我们提出了TPTL[U，S]的非准时性的一个推广，称为\emph{non adjacency}，并专注于它的1-变量片段1-TPTL[U，S].虽然非相邻的1-TPTL[U，S]似乎是一个非常小的片段，但它比MITL更严格地表达。作为我们的主要结果，我们证明了非相邻1-TPTL[U，S]的可满足性检验问题是可判定的，具有EXPSPACE完全复杂性。
2021-09-05 cs.LO
Second-Order Quantifier Elimination and Uniform Interpolation for Bath Path Logic and the Ordered Fragment
The University of Manchester（曼彻斯特大学）；Central European University（中欧大学）
考虑并扩展基本路径逻辑和一阶逻辑有序片段结果。通过引入常量斯柯伦化，将有序片段句子转化为基本路径逻辑，证明相关性质，还刻画了SCAN算法搜索空间并证明其终止性。
2026-07-07 cs.LO
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
本研究开发了面向代数模态不动点逻辑的通用推理器COOL 2，可实例化为多种模态逻辑的推理工具，并在多类基准集上完成了评估。
2023-06-15 cs.FL cs.LO
A Linear Temporal Logic of Frequencies on Series of Events
Universität Tübingen（蒂宾根大学）；University School for Advanced Studies IUSS Pavia（帕维亚高等研究学院）；University of Milan（米兰大学）
本文提出LTLF，一种通过引入测度敏感算子表达事件序列频率属性的时序逻辑，用于形式化监控和控制系统（如机器学习分类器）。
2026-11-03 cs.LO math.LO
Axiomatizations of Team Logics
在一个模块化的方法，我们提升希尔伯特式证明系统的命题，模态和一阶逻辑广义系统为各自的团队为基础的扩展。我们对Väänänen的一阶群逻辑TL的无依赖片段FO（~），命题群逻辑PTL，量化命题群逻辑QPTL，模态群逻辑MTL，以及相应的依赖、独立、包含和排除逻辑，得到了合理而完整的公理化.作为完备性证明的关键步骤，我们证明了上述逻辑在某种意义上承认从公式中消除模态和量词的语义保持性。
2018-03-26 cs.LO
On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic (extended version)
我们介绍了一个多排序分层三段论，称为4LQSR，承认变量的四种和限制形式的量化变量的前三种，并证明它有一个可解的可满足性问题，显示它享有一个小的模型属性。然后，我们考虑4LQSR的片段（4LQSR）^h，它由量词前缀长度以h > 1为界的4LQSR公式组成，满足一定的句法约束，并证明了它们都存在NP完全可满足性问题。最后，我们证明了模态逻辑K45可以用4LQSR ^3表示。
2012-09-10 cs.LO
Lecture Notes on Verifying Graph Neural Networks
ENS de Lyon（里昂高等师范学院）
本文回顾了图神经网络与多种逻辑的联系，提出了一种包含线性不等式中计数模态的模态逻辑以解决图神经网络验证任务，并给出了基于tableau方法扩展的可满足性算法。
2025-10-13 cs.LG cs.LO
Fundamental Logic Through the Lens of Modality
University of California, Berkeley（加州大学伯克利分校）；Chapman University（查普曼大学）
本文利用模态逻辑，通过Gödel-McKinsey-Tarski和Goldblatt翻译，证明了基础逻辑与正交逻辑、直觉主义逻辑之间的完全忠实嵌入关系。
2026-07-24 cs.LO math.LO
First-order Logic: Modality and Intensionality
当代对“内涵”一词的使用源于传统逻辑学的弗雷格-罗素学说，即一个观念（逻辑公式）既有外延又有内涵。从蒙塔古的观点来看，一个观念的意义可以被认为是在不同的可能世界中的特殊扩展。在本文中，我们分析了最小的内涵语义丰富的语法的FOL语言，统一不同的观点：塔斯基外延语义的FOL，模态解释的量词，并推导出塔斯基理论的真理统一语义理论的基础上，一个单一的意义关系。我们发现，并不是所有的模态谓词逻辑是内涵的，并在一个特定的纯扩展模态谓词逻辑（是标准的塔斯基语义的FOL）的结果，在FOL的逻辑量词的等效模态Kripke的解释。这种最小的内涵丰富是通过采用性质、关系和命题理论（PRP）作为FOL的论域或域来获得的，FOL由特殊和普遍（或概念）组成，FOL的两步解释消除了Montague内涵语义学的弱点。从Bealer的内涵FOL出发，我们证明了为了获得FOL的全部内涵性质，不需要引入内涵抽象。本文的最后结果用交换同态图来表示，交换同态图在这个新的内涵FOL的每一个给定的可能世界中成立，从FOL语法的自由代数，到它的内涵概念代数，再到新的外延关系代数（不同于代数），我们表明，它对应于塔斯基的解释标准的扩展FOL在这个可能的世界。
2011-03-03 cs.GL cs.IT cs.LO
Alternation Is Strict For Higher-Order Modal Fixpoint Logic
研究了交替奇偶Krivine自动机（APKA）的表达能力，APKA为高阶模态不动点逻辑（HFL）提供了操作语义。APKA由普通的奇偶自动机扩展的变化Krivine抽象机。我们表明，APKA的优先级的数量和奇偶性形成了一个适当的层次结构的表达能力，在模态μ演算。这也导致了HFL上严格的交替层次结构。证明遵循Arnold（1999）的编码运行到树和随后使用的Banach不动点定理。
2016-09-14 cs.FL cs.LO
Sahlqvist Correspondence Theory for Second-Order Propositional Modal Logic
带有命题量词的模态逻辑（即二阶命题模态逻辑（SOPML））在模态逻辑的早期就被考虑过。它的表达能力和复杂度都很高，并且它的van-Benthem-Rosen定理和Goldblatt-Goldblason定理已经被ten Cate（2006）证明。然而，Sahlqvist理论的SOPML尚未被认为在文献中。在本文中，我们填补了这一空白。我们发展了SOPML的Sahlqvist对应理论，它涵盖并适当地扩展了基本模态逻辑中现有的Sahlqvist公式。我们定义类的Sahlqvist公式SOMPL一步一步的分层方式，其中每个公式被证明有一个一阶对应的Kripke框架有效地计算的算法$ALBA^{SOMPL}$。此外，我们表明，某些$Π_2$规则对应于$Π_2$ -Sahlqvist公式在SOMPL，进一步对应于一阶条件，即使是非常简单的SOMPL Sahlqvist公式，他们可能已经是非规范的。
2021-10-16 cs.LO
Algebraic semantics for one-variable lattice-valued logics
任何一阶逻辑的单变量片段都可以被认为是模态逻辑，其中全称量词和存在量词分别被盒模态和菱形模态所取代。在一些情况下，这些逻辑的代数语义的公理化已经得到：最值得注意的是，分别为一阶经典逻辑和直觉主义逻辑的单变量片段的模态对应物S5和MIPC。然而，在一阶中间逻辑的设置之外，缺乏一种通用的方法。本文提供了这样一种方法的基础上设置的一阶格值逻辑，其中公式解释的代数结构与格约简。特别是，公理化得到的模态对应的一个广泛的家庭这些逻辑的一个变量片段通过推广的功能表示定理Bezhanishvili和哈丁一元Heyting代数。一个替代的证明理论的证明也提供了一个变量片段的一阶子结构逻辑，有一个切自由的插值演算，并承认一定的有界插值性质。
2022-09-18 cs.LO math.LO
Bundled fragments of first-order modal logic: (un)decidability
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
量化模态逻辑为模态态度的推理提供了一种自然的逻辑语言，即使在保留量化的丰富性的同时，也可以引用域上的谓词。但是，在许多模型类上，逻辑的大多数片段都是不可判定的。多年来，只有少数片段（例如单声部）被证明是可判定的。在本文中，我们研究的片段，捆绑量词和模态在一起，知识/为什么/什么的认知逻辑的早期工作的启发。与量化模态逻辑一样，域是否在世界上保持相同会产生重大差异。特别是，我们表明，束$\forall \Box$是不可判定的恒定域的解释，即使只有一元谓词，而$\exists \Box$束是可判定的。另一方面，在增加域解释，我们得到的可判定性与$\forall \Box$和$\exists \Box$束与不受限制的谓词。在这些情况下，我们还获得了在\PSPACE中运行的基于tableau的过程。我们进一步表明，$\exists \Box$束不能区分恒定域和增加域的解释。
2018-03-28 cs.AI cs.LO math.LO
Uniform interpolation with constructive diamond
University of Amsterdam（阿姆斯特丹大学）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
本文通过构造性方法证明构造性K（CK）和Wijesekera的K（WK）具有均匀插值性质，填补了直觉主义模态逻辑中独立box和diamond算子均匀插值研究的空白。
2026-05-27 cs.LO math.LO
Characterising Probabilistic Alternating Simulation for Concurrent Games
概率博弈结构结合了非确定性和随机性，参与者重复地同时采取行动，以进入并发博弈的下一个状态。概率交替模拟是比较不同概率博弈结构行为的重要工具。在本文中，我们提出了一个健全的和完整的模态特性的模拟关系，提出了一个新的逻辑概率分布的基础上。该逻辑使玩家能够在下一个状态或分布中强制执行属性。它的不动点扩张也是模拟关系的特征，在实际应用中可以表达许多有趣的性质。
2019-07-09 cs.LO
A New Modal Framework for Epistemic Logic
Peking University（北京大学）
近年来，非标准认知逻辑（knowingwhether，knowinghow，knowingwhat，knowingwhy等）引起了人们越来越大的兴趣，这些逻辑中引入的新的认知模态在语义上都共享$\exists x \Box ϕ$的一般模式，例如，知道如何实现$ϕ$大致意味着存在一种方法，这样你就知道它是一种方法，以确保$ϕ$。此外，由此产生的逻辑是可判定的。受这些特定逻辑的启发，在这项工作中，我们提出了一个非常通用和强大的框架的基础上，量词自由谓词语言扩展了一个新的模态$\Box^x$，它包完全$\exists x \Box$在一起。我们表明，所得到的语言，虽然更有表现力，共享许多良好的性质的基本命题模态逻辑在任意模型，如有限树模型属性和van Bentham的特征w.r.t.一阶模态逻辑我们公理化的逻辑在S5框架与直观的公理捕捉之间的相互作用$\Box^x$和知道，运营商在认知设置。
2017-07-27 cs.AI cs.LO
Alternating (In)Dependence-Friendly Logic
针对 IF 逻辑的参与者不对称、非确定及排中律失效问题，本文提出 ADIF，并给出组合、Herbrand-Skolem 与博弈论语义，证明其确定性、排中律及二阶逻辑表达力。
2023-04-23 cs.LO math.LO
Graded modal logic and counting message passing automata
本研究探讨分级多模态逻辑与计数消息传递自动机的关联，提出分级多模态类型与推广Weisfeiler-Leman算法的自动机，证明二者识别模型类的等价性，并给出带Härtig量词和最大不动点的一阶逻辑执行该算法的方法。
2024-01-26 cs.DC cs.LO
A proof-theoretic approach to uniform interpolation property of multi-agent modal logic
针对多智能体模态逻辑缺乏证明论进路UIP证明的问题，本文扩展已有证明系统，提出纯句法算法，证明了$\boldsymbol{\text{K}_n}$等三类多智能体模态逻辑的一致插值性质，还给出了无需二阶量词的直接证明。
2025-10-29 cs.LO
The Alternating-Time μ-Calculus With Disjunctive Explicit Strategies
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡弗里德里希-亚历山大大学）；The Australian National University（澳大利亚国立大学）
本文将ATLES扩展为带不动点算子和策略析取的AMCDES，以更灵活刻画公平性等时序性质及受控非确定性承诺，并证明其可满足性检测为ExpTime完全，模型检测在固定解释下为QP与NP∩coNP、开放解释下为NP。
2023-05-30 cs.AI cs.LO
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Bologna（博洛尼亚大学）
本文提出了一种无割的嵌套序列系统，用于处理具有内外域的量模态逻辑，通过可达规则实现域条件的自然定义，并证明了系统的完备性和证明论性质。
2026-04-20 cs.LO math.LO
Uniform Interpolation in Distributed Knowledge Modal Logics
Jinan University（暨南大学）
本文研究了分布式知识模态逻辑中的统一插值性质，通过扩展经典公式和字面消除框架，引入集体p-仿射概念，证明了六种分布式知识模态逻辑的统一插值性质。
2026-03-30 cs.LO
Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
我们提出了一个变体的ATL与分布式知识运营商的基础上同步和完善的召回语义。这种逻辑中的联盟模式是基于对完整历史的部分观察，并结合了联盟成员之间的合作形式，其中代理基于该联盟的系统历史的分布式知识发布其行动。我们表明，模型检验是可判定的这种逻辑。该技术利用两个变种的游戏与不完美的信息和部分可观察的目标，以及一个子集的建设，用于识别状态的历史是无法区分的考虑联盟。
2010-06-08 cs.LO cs.MA
Bicompleteness Theorems for Team Logics with the Dual Negation
University of Padua（帕多瓦大学）
研究独立友好逻辑和依赖逻辑中双重否定的语义不确定性，通过调整不相容概念，为多种模态和命题团队逻辑建立了类似结果，并提出了关于不相容性的表达完备性概念。
2026-06-23 cs.LO math.LO
Continuous Modal Logical Neural Networks: Modal Reasoning via Stochastic Accessibility
Lawrence Berkeley National Laboratory（伯克利劳伦斯国家实验室）
本文提出连续模态逻辑神经网络，通过随机可及性实现模态推理，结合逻辑公式指导神经网络生成符合逻辑属性的解决方案。
2026-03-04 cs.LG cs.LO
Modal Logic with Relations over Paths: a Theoretical Development through Comonadic Semantics
本研究提出路径谓词模态逻辑PPML，通过共单子语义建立其模型论性质，关联DataGL等数据感知逻辑与基本模态逻辑，实现多项式时间归约。
2024-08-14 cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information Theory
本文提出逻辑ATLH，基于哈特利不确定性度量扩展交替时序逻辑，用于量化智能体关于事实的知识不确定性，并证明其与ATLK表达力相同但指数级更简洁。
2023-10-18 cs.LO cs.MA
Parity Games and Automata for Game Logic (Extended Version)
Parikh的游戏逻辑是一个类似PDL的不动点逻辑，它在单调邻域框架上解释，表示玩家在确定的两人游戏中的战略力量。博弈逻辑转化为单调$μ$ -演算的一个片段，而单调模式自动机又在表达上等价于单调模式自动机。奇偶博弈和自动机是处理模态不动点逻辑（如模态$μ$ -演算）中嵌套不动点的组合复杂性的重要工具。本文（1）讨论了邻域结构上博弈逻辑的奇偶博弈语义a，（2）利用这些博弈得到了对应于博弈逻辑的单调$μ$ -演算片段的自动机理论刻画。我们的证明广泛使用的结构，我们称之为语法图，结合了易于使用的语法树的公式与自动机的灵活性和简洁性。它们本质上是一个基于图的观点的交替树自动机，介绍了威尔克在研究模态$μ$ -演算。
2017-09-03 cs.LO
Disjunctive bases: normal forms and model theory for modal logics
本文提出析取基作为余代数模态逻辑的通用范式框架，证明其蕴含模拟定理和Lyndon定理，并探讨其与nabla模态的关系及构造方法。
2022-08-19 cs.LO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.LO
Completeness of Flat Coalgebraic Fixpoint Logics
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性中。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的定点逻辑倾向于用表达性来换取简单性和可读性，事实上，它经常存在于μ演算的单个变量片段中。这种平坦定点逻辑的家族包括，例如，LTL、CTL和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算（如交替时间时序逻辑ATL）的平坦片段，以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
2016-06-09 cs.LO
