Completeness for Game Logic
游戏逻辑是由Rohit Parikh在20世纪80年代引入的，作为命题动态逻辑（propositional dynamic logic，PDL）的推广，用于推理玩家在确定的2人游戏中可以强制执行的结果。从语义上讲，从程序到游戏的概括是通过从Kripke模型到单调邻域模型来反映的。Parikh提出了一个自然的PDL风格的希尔伯特系统，它很容易被证明是合理的，但它的完备性迄今为止仍然是一个开放的问题。在本文中，我们介绍了一个切免费的游戏逻辑的mu演算，和两个切免费的mu演算，操作注释公式，一个游戏逻辑和一个单调的μ演算，多模态μ演算的变体，其中的语义是由单调邻域模型，而不是Kripke结构。我们表明这些系统是健全的和完整的，帕里克的公理化的完整性如下。我们的方法建立在Afshari & Leigh（LICS 2017）最近的想法和结果的基础上，我们通过系统之间的一系列证明转换来获得完整性。一个关键的要素是从博弈逻辑到单调μ演算的有效性保持翻译。
2019-04-30 cs.LO math.LO
Kripke Semantics for Martin-Löf's Extensional Type Theory
众所周知，简单类型论对于非标准集值模型是完备的。标准模型的完备性仅适用于某些扩展类的模型，例如，闭范畴类。类似地，依赖类型论对于局部carnival闭范畴也是完备的。然而，通常很难建立依赖类型论解释的连贯性，即，来证明平等表达的解释确实是平等的。已经使用了几类模型来解决这个问题。我们的调查作出贡献，给出了一个语义，是标准的，连贯的，并足够普遍的完整性，同时保持相对容易计算。我们的模型解释类型的马丁-洛夫的外延依赖类型论作为集索引的偏序集，或等价地，作为纤维化的偏序集。这种语义可以看作是对Kripke模型中直觉一阶逻辑解释的依赖类型论的推广。这就产生了一个简单的连贯的模型理论，相对于它，简单的和依赖的类型论是健全的和完备的。
2011-09-26 cs.LO math.CT math.LO
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
2009-02-12 cs.LO
Combining intermediate propositional logics with classical logic
在[17]中，我们介绍了一种模态逻辑，称为$L$，它结合了直觉命题逻辑$IPC$和经典命题逻辑$CPC$，并且是完全的w.r.t.代数语义学然而，对于Kripke风格的语义来说，$L$似乎太弱了。在本文中，我们增加了积极和消极的内省，并表明，由此产生的逻辑$L5$有一个Kripke语义。对于中间逻辑$I$，我们考虑$L5$的参数化版本$L5(I)$，其中$IPC$被$I$取代。$L5(I)$可以看作是$I$中关于真值推理的经典模态逻辑。从我们的研究结果，我们得出一个简单的方法来确定代数和Kripke语义的一些特定的中间逻辑。我们讨论了一些计算机科学感兴趣的例子，即这里和那里的逻辑，哥德尔-达米特逻辑和扬科夫逻辑。我们的方法提供了新的证明的完整性定理，由于Hoclane，Dummett/Horn和Jankov，分别。
2015-10-19 cs.LO
An algebraic generalization of Kripke structures
经典命题正规模态逻辑的Kripke语义是通过将Kripke结构嵌入到更大类的点稳定支撑量子中来代数化的。这种代数语义包含了传统的代数语义的基础上格与一元运算符，它提出了自然的解释模态逻辑，可能感兴趣的应用，在结构中出现的几何和分析，如叶状流形和算子代数，通过拓扑群胚和逆半群。我们研究了系统K，T，K4，S4和S5的基于Quantale的语义的完备性，特别是获得了S5的公理化，它不使用否定或模态必要性算子。作为额外的例子，我们描述直觉命题模态逻辑，程序PDL的逻辑，和分歧的时态逻辑CTL。
2007-04-14 cs.LO math.LO math.RA
Cover Semantics for Intuitionistic Modalities
School of Informatics University of Edinburgh（爱丁堡大学信息学院）
研究直觉模态逻辑的语义问题，提出关系覆盖语义的保守扩展，减轻限制便于模型构建，通过在Agda中形式化语义并建设性证明完备性，为直觉模态逻辑研究提供新方法。
2026-10-15 cs.LO cs.PL
Abstract Model Repair
给定一个Kripke结构M和CTL公式$φ$，其中M不满足$φ$，模型修复问题是得到一个新的模型M'，使得M'满足$φ$ .此外，为了导出M'而对M所做的改变相对于所有这样的M'应该是最小的。在模型检验中，状态爆炸使得对具有无限甚至大状态空间的模型进行模型修复几乎不可能。在本文中，我们提出了一个模型修复的框架，使用抽象细化，以解决状态爆炸。我们的框架的目的是修复Kripke结构模型的基础上Kripke模态转换系统的抽象和CTL的3值语义。我们引入了一个抽象模型修复算法，我们证明了合理性和半完备性，我们研究了它的复杂性类。此外，一个原型实现，以说明抽象模型修复的实际效用的自动开门系统模型和安德鲁文件系统1协议的模型。
2015-09-16 cs.LO
Graded modal logic and counting bisimulation
本文将互模拟不变片段的刻画定理推广到分级多模态逻辑，证明其在所有及有限点态 Kripke 结构上恰好对应计数互模拟等价下保持的一阶性质。
2023-07-18 cs.LO math.LO
Verified completeness in Henkin-style for intuitionistic propositional logic
本文在Lean定理证明器中形式化并验证了Troelstra和van Dalen提出的直觉主义命题逻辑Henkin式完备性证明，是该方法下首个经机械验证的同类成果，源码已开源。
2023-10-03 cs.LO
Generalized Strong Preservation by Abstract Interpretation
标准的抽象模型检验依赖于抽象Kripke结构，该结构通过将不可区分的状态粘合在一起来近似具体模型，即通过具体状态空间的划分。规约语言L的强保持性描述了L中公式的具体和抽象模型检验的等价性。我们展示了如何抽象的解释可以用来设计抽象模型，更一般的抽象Kripke结构。相应地，强保持被推广到基于抽象解释的模型，并与抽象解释中的完整性概念精确相关。最小化精化抽象模型以使其对某种语言L强保持的问题可以表述为抽象解释中的最小域精化以获得w.r.t. L的逻辑/时态运算符。结果表明，这个精炼的强保持抽象模型总是存在的，并且可以被刻画为一个最大不动点。因此，一些著名的行为等价，如互模拟，模拟和口吃，以及它们相应的分区细化算法可以优雅地在抽象解释为完整性属性和细化。
2006-03-14 cs.LO cs.PL
Awareness Logic: A Kripke-based Rendition of the Heifetz-Meier-Schipper Model
Center for Information and Bubble Studies, University of Copenhagen（哥本哈根大学信息与泡沫研究中心）
Heifetz，Meier和Schipper（HMS）提出了意识的晶格模型。HMS模型是无语法的，这排除了依赖于形式语言来诱导格的简单选择，并且用一个纠缠的构造来表示不确定性和无意识，使得难以评估任何一个的属性。在这里，我们提出了一个模型的基础上格的Kripke模型，诱导原子子集列入，其中的不确定性和无意识是分开的。我们证明了模型是等价的，通过定义它们之间的转换，保持公式的满足，并通过我们和HMS的结果获得完整性。
2020-12-23 cs.AI cs.LO cs.MA
A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version
双直觉主义逻辑是直觉主义逻辑的推广，它具有一个与蕴涵有关的联结对偶。双直觉逻辑是由Rauszer作为具有代数和Kripke语义的Hilbert演算引入的。但她随后对BiInt的"无切“演算最近被Uustalu证明是失败的。我们提出了一个新的切割免费的BiInt演算，并证明它的声音和完整的Kripke语义。确保完整性是复杂的含义和它的对偶之间的相互作用，类似于未来和过去的时态逻辑模态。我们的演算处理这种相互作用，使用扩展序列传递信息的前提下的结论，使用实例化的变量在失败的派生树的叶子。我们简单的终止论证允许我们的演算用于自动演绎，尽管这不是它的主要目的。
2007-04-17 cs.LO
Weak Completeness of Coalgebraic Dynamic Logics
我们提出了Fischer和Ladner的命题动态逻辑（PDL）和Parikh的游戏逻辑（GL）的共代数概括。在早期的工作中，我们证明了一个通用的强完备性结果的余代数动态逻辑没有迭代。这些程序的共代数语义由单子T给出，模态通过谓词提升来解释，其转置是从T到邻域单子的单子态射。在本文中，我们表明，如果单子T进行了一个完整的半格结构，那么我们可以定义一个迭代构造，和适当的概念菱形和框状的谓词提升，允许定义的公理化参数在T中，pixel和一组选定的逐点程序操作。作为我们的主要结果，我们表明，如果逐点操作是“负自由”和Kleisli组合左分布在诱导加入Kleisli箭头，那么这个公理化是弱完全的标准模型类。作为特例，我们恢复了PDL和双自由博弈逻辑的弱完备性。作为一个适度的新的结果，我们获得了完整的双自由GL扩展与交叉（恶魔的选择）的游戏。
2015-09-10 cs.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO math.LO
On Logic of Formal Provability and Explicit Proofs
1933年，哥德尔考虑了两种描述可证明性的模态方法。一个捕获了形式可证明性，并导致了逻辑GL和Solovay的完备性定理。另一种是以模态逻辑S4为基础，发展出阿特莫夫的证明逻辑LP。本文研究了作者提出的逻辑GLA，它是GL和LP语言的结合体。GLA具有Kripke风格的语义和相应的完备性定理。建立了GLA关于算术可证性语义的可靠性和完备性。
2014-05-11 cs.LO math.LO
Intuitionistic Propositional Logic in Lean
该研究在Lean证明助手中形式化直觉主义命题逻辑，验证其两份完备性证明，探究Kripke与代数两种语义范式的关系，还证明了大量定理及演绎规则。
2024-10-31 cs.LO
Clausal Resolution for Modal Logics of Confluence
我们提出了一个子句解析为基础的方法，正常的多模态逻辑的融合，其Kripke语义的基础上，其特征在于适当的教会-罗瑟属性的实例框架。在这里，我们限制注意八个家庭这样的逻辑。我们展示了如何正常的逻辑汇流的推理规则，可以系统地获得从参数化公理，这些系统。我们讨论的方法的可靠性，完整性和终止。特别地，完备性可以通过显示每个新添加的推理规则的结论确保框架上的相应条件成立来模块化地证明。为了说明该方法的使用，给出了一些例子。
2014-05-01 cs.LO
Terminating Calculi for Propositional Dummett Logic with Subformula Property
本文给出了两个满足子公式性质的命题Dummett逻辑的终止表演算。我们演算的思想依赖于Dummett逻辑的线性有序Kripke语义。第一个演算在两个语义层面上工作：现在和下一个可能世界。第二个演算采用通常的对象语言的Tableau系统，并利用一个属性的建设的完整性定理，引入一个检查，这是一种替代循环检查机制。
2012-06-20 cs.LO
Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics
双直觉稳定时态逻辑（英语：Bi-Intuitionistic Stable Tense Logics）是一种具有克里普克语义的时态逻辑，其中框架中的世界配备有前序以及相对于该前序“稳定”的可达性关系。BIST逻辑是在超图的语义背景下产生的逻辑BiSKt的扩展，因为预序的特殊情况可以表示超图的关联结构。在本文中，我们提供了，第一次，一个希尔伯特式公理化的BISKt和证明强完备性的BiSKt。我们继续证明强完备性的一类BIST逻辑得到的BiSKt由一定形式的公式扩展。此外，我们还证明了一类BIST逻辑的有限模型性质和可判定性。
2017-03-07 cs.LO math.LO
Awareness Logic: Kripke Lattices as a Middle Ground between Syntactic and Semantic Models
Center for Information and Bubble Studies, University of Copenhagen（哥本哈根大学信息与泡沫研究中心）
关于认知建模的文献包括无语法和基于语法的框架。Heifetz，Meier \& Schipper（HMS）提出了一个无语法的意识格模型。虽然他们的格方法是优雅和直观的，但它排除了依赖形式语言来归纳格的简单选择，并且没有明确区分不确定性和无意识。与此相反，最突出的基于语法的解决方案，Fagin-Halpern（FH）模型，解释了这种区别，并提供了一个简单的意识表示，但缺乏格结构的直观性。在这里，我们结合这两种方法，通过提供一个格的Kripke模型，诱导原子子集包含，其中不确定性和无意识是分开的。我们证明了我们的模型等价于HMS和FH模型，通过定义它们之间的转换，保留了显式知识的语言公式的满意度，并通过我们和HMS的结果获得完整性。最后，我们证明了Kripke格模型可以被证明等价于FH模型（当意识是命题确定的），也相对于语言的一般意识的逻辑，FH模型最初提出。
2021-06-24 cs.AI cs.LO cs.MA
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
An expressive completeness theorem for coalgebraic modal mu-calculi
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。然后，我们考虑下的行为等价的MSO公式的不变性。更具体地说，我们调查是否coalgebraic μ演算是一元二阶语言的一个给定的函子的bisimulation不变的片段。使用automatatattheoretic技术和建设最近的结果由第三作者，我们表明，为了提供这样的表征结果，它足以找到我们所谓的一个足够的一致建设的coalgebraic型函子。作为这个结果的直接应用，我们获得了部分新的证明的Janin-Walukiewicz定理的模态μ演算，避免使用语法范式，和互模拟不变的结果袋函子（分级模态逻辑）和所有指数多项式函子（包括"游戏函子"）。作为一个更复杂的应用程序，涉及额外的非平凡的想法，我们还得到了一个单调模态μ演算的特征定理，相对于自然的一元二阶语言单调邻域模型。
2017-06-30 cs.LO
Towards a Proof Theory of Gödel Modal Logics
针对基本模态模糊逻辑的盒形和菱形片段引入了分析证明演算，该演算将模态逻辑K的Kripke语义与哥德尔逻辑的多值语义相结合.演算用于建立这些片段的完整性和复杂性结果。
2011-05-14 cs.LO math.LO
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
2018-01-22 cs.LO
Complete and Terminating Tableau Calculus for Undirected Graph
本文针对无向图构造混合逻辑的表列方法，证明其完备性与终止性，并由此得出该逻辑的可判定性。
2024-11-25 cs.LO math.LO
Named Models in Coalgebraic Hybrid Logic
DFKI（德国人工智能研究中心）；Universität Bremen（不来梅大学）；Imperial College London（伦敦帝国理工学院）
混合逻辑扩展了模态逻辑，支持对由所谓的名词指定的各个状态进行推理。我们在共代数语义的广泛背景下研究混合逻辑，其中Kripke框架被替换为给定函子的共代数，从而涵盖了广泛的推理原则，包括，例如，概率、分级、默认或联合运算符。具体而言，我们建立通用标准，一个给定的共代数混合逻辑承认命名的规范模型，随后的完整性证明纯扩展一方面，和扩展的混合语言与本地绑定的其他。我们用一些例子来实例化我们的框架。值得注意的是，我们证明了具有局部约束的分次混合逻辑的完备性。
2010-02-03 cs.AI cs.LO
Spatial logic of modal mu-calculus and tangled closure operators
该研究将McKinsey和Tarski的拓扑模态逻辑成果拓展至模态μ演算与缠结算子逻辑，证明二者在拓扑空间上表达力等价，建立了相关逻辑的有限模型性质，拓展了剖分引理，得到多种语言在自稠密度量空间上的完备性与可靠性结果。
2016-03-05 cs.LO math.LO
Completeness for Flat Modal Fixpoint Logics
本文给出了一类模态不动点逻辑完备性的一般统一证明方法。给定形式为γ（x，p1，. . ., pn），其中x只在γ中出现，语言L \sharp（Γ）是通过对每个γε在多模态逻辑语言中增加一个连接词\sharp \_γ而得到的.术语\sharp \_γ（\varphi 1，. . ., \varphin）的最小不动点应解释为项γ（x，φ1，. . .,φn）。本文考虑如下问题：给定Γ，构造一个公理系统，它对于语言L \sharp（Γ）在Kripke框架上的具体解释是可靠的和完备的.我们证明了两个结果，解决这个问题。首先，令K \sharp（Γ）是通过为每个不动点连接符\sharp \_γ添加Kozen-Park型不动点公理和最小不动点规则而从基本多峰K获得的逻辑。只要每个标引公式γ满足在x中不捆绑的句法准则，我们证明了这个公理系统是完备的.其次，在一般情况下，证明了K_ \sharp（Γ）的扩张K ~+（Γ）的可靠性和完备性.这种扩展是通过一个有效的过程获得的，给定索引公式γ作为输入，返回\sharp \_γ的公理和推导规则的有限集合，其大小由γ的长度限制。因此，公理系统K+（Γ）是有限的，只要Γ是有限的。
2008-12-12 cs.LO math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics
Technische Universität Wien（维也纳技术大学）
本文是Berkel和Lyon于2019年发表的论文“时态STIT逻辑的免切演算和关系语义”的附录。给出了基本STIT逻辑Ldm（相对于非自反的时态Kripke STIT框架）的完备性证明，并推导了逻辑Xstit的主体独立性公理.
2019-02-18 cs.AI cs.LO
Explicit Evidence Systems with Common Knowledge
本文开发了一种包含个体与公共知识证据项的多智能体证明逻辑，定义了 Kripke 风格语义并证明其可靠性与完备性，同时分析了其与 S4 的关系及协调攻击问题。
2010-05-04 cs.LO math.LO
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
2025-07-09 cs.LO math.LO
Pointed Modal Abelian Logic, Algebraically
Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机研究所）；Department of Algebra, Faculty of Mathematics and Physics, Charles University（查理大学数学物理学院代数系）
本文研究实数的点态模态逻辑，通过有界赋值建立克里普克语义，并引入负点态模态阿贝尔l-群簇，利用无穷阿基米德规则证明无穷代数完备性。
2026-08-04 cs.LO math.LO
Modal meet-implication logic
本文扩展命题直觉主义逻辑的 meet-implication 片段，引入保持 meet 的模态，基于半格给出语义并建立对偶性，获得完备性，识别共同模态片段，并证明其为 dialgebraic 逻辑，进而获得某处可表达性。
2022-07-13 cs.LO math.LO
Hypergraph Semantics for Doxastic Logics
CNRS, IRIT, University of Toulouse（法国图卢兹大学）；Institute of Computer Science, University of Bern（瑞士伯尔尼大学计算机科学研究所）
本文提出基于超图的信念逻辑语义，能够描述代理的信念，并提供两种信念系统及公理化体系的完备性证明。
2025-12-28 cs.LO
The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
Institute of Sciece Tokyo, Japan（东京科学研究所）
本文研究基于构造模态逻辑CK的μ-演算变种，定义了游戏语义并证明其等价于双关系李普克内语义，进而利用游戏语义证明了完全标记的非良基证明系统的正确性与完备性，并探讨如何将其扩展到其他非经典模态逻辑的μ-演算。
2026-04-25 cs.LO math.LO
On semantics of first-order justification logic with binding modalities
Steklov Mathematical Institute of Russian Academy of Sciences（俄罗斯科学院斯捷克洛夫数学研究所）
本文提出一种结合证明术语和绑定模态的第一次序逻辑证明系统，并建立了其相对于Kripke式语义的正确性和完备性。
2025-12-08 cs.LO math.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
Intuitionistic Layered Graph Logic: Semantics and Proof Theory
该文提出直觉主义分层图逻辑ILGL，给出其语义与证明论，证明可判定性及Stone对偶，并扩展至谓词版本，用于建模复杂系统的分层结构。
2018-10-29 cs.LO
Stone-Type Dualities for Separation Logics
本文系统建立了分离逻辑及其变体的Stone型对偶定理，统一处理BI、BBI及多种扩展逻辑，首次证明了DMBI等逻辑的可靠性与完备性，为资源语义提供了范畴论框架。
2019-03-13 cs.LO
Many-Valued Modal Logic
本文提出一种基于有限线性序真值集和真值表联结词的多值极小正规模态逻辑，给出矢列演算并证明其可靠性与强完全性，还证明了有限模型性质并讨论其扩张及与多值直觉主义逻辑的关系。
2024-12-31 cs.LO
Modal Measurable Logics via a Modal Loomis-Sikorski Representation Theorem
University of Amsterdam（阿姆斯特丹大学）；University of Bern（伯尔尼大学）；Indiana University（印第安纳大学）
提出一种带模态的无穷可数合取与析取逻辑，用于动力系统和点自由遍历理论的测度论工作，并通过Jonsson-Tarski对偶和Loomis-Sikorski定理证明其相对于新Kripke语义的完备性。
2026-07-01 cs.LO math.LO
A General (Uniform) Relational Semantics for Sentential Logics
University of Thessaly（色萨利大学）
本文提出了一种通用的关系语义学框架，通过公理化和结构的调整，为经典和非经典逻辑提供统一语义，并利用广义Sahlqvist-van Benthem算法进行对应结果计算。
2025-11-23 cs.LO math.LO
Intuitionistic Justification Logic, Semantically
University of Birmingham（伯明翰大学）
本文为直觉主义辩护逻辑（含满足子项）提出两类语义模型，证明其可靠性与完全性，并通过实现定理建立与直觉主义模态逻辑的联系。
2026-07-01 cs.LO
T-BAT semantics and its logics
本文研究表达非形式可证明性的T-BAT非确定四值逻辑，通过真值转换证明其可定义逻辑的完备性，并利用Kripke语义考察公理，最终给出直观公理化。
2025-10-16 cs.LO
First-order Logic with Being a Thesis Modal Operator
将“是一个论题”模态算子引入一阶逻辑，实现Carnap思想，证明完备性并展示其强度为S5的真扩展，可句法定义逻辑蕴涵和一致性。
2024-06-25 cs.LO math.LO
Bounded Modal Logic: Explicit Scope Dependencies in Multi-Stage Programming
Kyoto University（京都大学）
有界模态逻辑通过结合直觉和模态转换，提供细粒度资源控制的理论支持。
2026-07-21 cs.LO
Possibility Frames and Forcing for Modal Logic
University of California, Berkeley（加州大学伯克利分校）
该文基于部分“可能性”发展正规模态逻辑模型理论，其可能性框架基于带可达关系的偏序集，公式解释为正则开集，标准世界框架是其特殊情况，还开展了对偶、可定义性/对应及完全性理论的初步研究。
2026-07-24 cs.LO math.LO
Positive fragments of coalgebraic logics
正模态逻辑是Dunn在1995年的一篇有影响力的论文中作为标准模态逻辑的正片段而引入的。他的完备性结果包括一个公理化，导出所有模态公式，这些公式在所有Kripke框架上都是有效的，并且只从原子命题、合取、析取、盒子和菱形中构建。本文对这一定理进行了余代数分析，不仅给出了基于对偶理论的概念性证明，而且将Dunn的结果从Kripke框架推广到了弱拉回保函子的余代数.为了便于这种分析，我们证明了一些范畴理论的结果函子的范畴$\mathsf{Set}$的集和$\mathsf{Pos}$的偏序集：每个函子$\mathsf{Set} \to \mathsf{Pos}$有一个$\mathsf{Pos}$丰富的左Kan扩展$\mathsf{Pos} \to \mathsf{Pos}$。以这种方式产生的函子被称为在离散态中有表示。在$\mathsf{Set} \to \mathsf{Pos}$实际上是$\mathsf{Set}$ -值的情况下，我们称相应的左Kan扩张$\mathsf{Pos} \to \mathsf{Pos}$为它的置位.一个$\mathsf{Set}$ -函子保持弱回调当且仅当它的定态保持正合平方。表示为离散点的$\mathsf{Pos}$ -函子保持满射.包涵体$\mathsf{Set} \to \mathsf{Pos}$致密。一个函子$\mathsf{Pos} \to \ma…
2015-09-21 cs.LO math.CT
Dynamic Cantor Derivative Logic
本文将基于Cantor导数算子的d-逻辑引入动力系统框架，提出了wK4C、K4C和GLC等逻辑，证明了其有限模型性质及在相应动态拓扑语义下的可靠性与完备性，并奠定了动态拓扑d-逻辑的一般证明方法基础。
2023-12-15 cs.LO math.LO
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
2014-11-05 cs.LO math.LO
Modal Logic for Stratified Becoming: Actualization Beyond Possible Worlds
本文提出分层现实化逻辑（SAL），以本体论稳定性层级索引模态，替代可能世界语义，并证明其可靠性与完全性，应用于时间生成、量子退相干及模态形而上学。
2025-06-12 cs.AI cs.LO
Modal Logic for Reasoning About Uncertainty and Confusion
The Czech Academy of Sciences（捷克科学院）；Rensselaer Polytechnic Institute（伦斯勒理工学院）；Aix Marseille Univ, CNRS, LIS（艾克斯-马赛大学，法国国家科学研究中心，信息学实验室）
本文提出了一种扩展的模态逻辑KG_inv，用于处理不确定性与困惑的推理，并展示了其在PSPACE中的完备性。
2025-11-27 cs.LO math.LO
Essence and accident modalities meet Belnapian truth values
University of Lodz（罗兹大学）
本文在贝尔纳普-邓恩四值逻辑FDE上推广本质与偶然模态，定义本质/偶然真、假、不一致和不确定模态，给出四值S5克里普克语义及无切超相继式演算，并证明嵌入定理，获得可靠、完全和切消除结果。
2026-10-07 cs.LO math.LO
