Modal operators on rings of continuous functions
模态代数范畴与描述框架范畴对偶等价是模态逻辑中的一个经典结果。后者是配备有斯通拓扑的Kripke框架，使得二元关系是连续的。这种二重性概括了著名的斯通二重性。我们的目标是进一步推广描述框架，使拓扑是一个任意的紧Hausdorff拓扑。为此，而不是工作的布尔代数的闭子集的石头空间，我们的工作与环的连续实值函数上的一个紧凑的豪斯多夫空间。主要的新颖性是定义一个模态算子在这样一个环上利用一个连续的关系在一个紧凑的Hausdorff空间。我们的出发点是紧致T2空间范畴$KHaus$和一致完备有界阿基米德$\ell$ -代数范畴$ubal$之间著名的Gelfand对偶。我们赋予有界阿基米德$\ell$ -代数一个模态算子，从而得到模态有界阿基米德$\ell$ -代数范畴$mbal$.我们的主要结果建立了$mbal$和范畴$KHK$之间的对偶连接，我们称之为紧凑的Hausdorff框架，也就是说，Kripke框架配备了紧凑的Hausdorff拓扑，使得二元关系是连续的。这个对偶附加限制在$KHK$和由$mbal$的一致完备对象组成的$mbal$的反射子范畴$mubal$之间的对偶等价。这推广了Gelfand对偶和模态代数的对偶。
2020-08-12 math.GN math.LO
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.LO
Interpolation for the two-way modal mu-calculus
本文为双向模态 μ-演算引入非良基与循环证明演算，利用迹原子应用 Vardi 自动机证明其可靠性与完备性，并据此确立 Craig 插值与 Beth 可定义性。
2025-08-11 cs.LO math.LO
The Distributive Full Lambek Calculus with Modal Operators
本文研究了在非交换条件下，考虑$\Box$和$\Diamond$的带有模态算子的有界分配剩余格的逻辑。我们为这样的子结构模态逻辑引入关系语义。通过离散对偶和正则扩张证明了任何正则逻辑都是Kripke完备的。也就是说，我们表明，一个模态扩展的分配充分Lambek演算是其框架的逻辑，如果它的品种是封闭的规范下的扩展。在此基础上，我们建立了剩余分配模态代数与基于Priestley空间的拓扑Kripke结构之间的Priestley式对偶。
2020-05-31 math.CT math.LO math.RA
Succinctness in subsystems of the spatial mu-calculus
本文系统地探讨了空间推理中使用的模态逻辑的简洁性问题。我们表明，封闭算子，尽管是表达较少，是指数更简洁的极限点算子，和$μ$ -演算是指数更简洁的比相等的表达纠缠极限算子。这些结果适用于包含至少一个拥挤度量空间或包含所有以低于$ω^ω$的序数为基础的空间的任何一类空间，具有通常的极限算子。我们还表明，这些结果继续举行，即使我们丰富了不简洁的语言与普遍的方式。
2017-08-12 math.LO
Cut elimination for the alternation-free modal mu-calculus
University of Gothenburg（哥德堡大学）；University of Amsterdam（阿姆斯特丹大学）
本文为模态μ-演算的无交替片段提出一种基于循环证明系统的语法切消去过程，利用多切和良拟序理论直接将带切证明转换为无切证明并保证终止。
2026-10-23 cs.LO math.LO
Bounded game-theoretic semantics for modal mu-calculus
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检查游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检查。
2020-05-21 cs.LO math.LO
Deciding some displayable modal logics
本文利用显示演算证明了正规模态逻辑K及其若干扩张的可判定性。
2023-12-25 math.LO
A Finitely Supported Frame for the Turing Schmerl Calculus
在arXiv：1604.08705中，我们介绍了命题模态逻辑$\textbf{TSC}$（代表图灵-施梅尔演算），它充分描述了不同类型的图灵级数之间的可证明的相互关系。在arXiv：1709.04715中，我们定义了一个模型$\mathcal{J}$，它被证明是$\textbf{TSC}$的一个万有模型，它基于深入研究的Ignatiev的$\textbf{GLP}$（Gödel Löb的多模态可证明性逻辑）的闭合片段的万有模型。在本文中，我们提出了一个新的通用框架$\mathcal{H}$，这是一个轻微的修改$\mathcal{J}$，其域允许一个模态定义的每个世界。
2018-04-27 math.LO
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
模态逻辑S4可以通过Curry-Howard风格的对应关系来使用，以获得一个模态演算。模态（盒装）类型被直观地解释为“演算的封闭语法”。这种模式演算被称为模态类型论--这是更一般的上下文模态类型论或CMTT的基本情况。CMTT从来没有被赋予一个指称语义，其中模态类型被赋予作为封闭语法的指称。我们展示了如何确实可以做到这一点，与扭曲。我们还利用这个表示证明了系统的一些性质。
2012-02-04 cs.LO math.LO
The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
Institute of Sciece Tokyo, Japan（东京科学研究所）
本文研究基于构造模态逻辑CK的μ-演算变种，定义了游戏语义并证明其等价于双关系李普克内语义，进而利用游戏语义证明了完全标记的非良基证明系统的正确性与完备性，并探讨如何将其扩展到其他非经典模态逻辑的μ-演算。
2026-04-25 cs.LO math.LO
Decomposition Theorems and Model-Checking for the Modal $μ$-Calculus
我们证明了一个一般的分解定理的模式$μ$ -演算$L_μ$的精神Feferman和Vaught的定理不相交的工会。特别是，我们表明，如果一个结构（即，转换系统）由两个子结构$M_1$和$M_2$加上从$M_1$到$M_2$的边组成，则在$M$中的节点处的公式真仅取决于在相应子结构中的公式真，其意义在下面进行精确说明。因此，我们证明了$L_μ$的模型检测问题是固定参数易处理的（FPT）类结构的有界凯利宽度或有界DAG宽度。据我们所知，这些是$L_μ$的第一个FPT结果，它不遵循嵌入到一元二阶逻辑中。
2014-05-09 cs.LO math.LO
The G4i analogue of a G3i calculus
Utrecht University（乌得勒支大学）
本文提出一种为一大类直觉主义模态逻辑构造终止分析演算的方法，将 Dyckhoff 针对直觉主义命题逻辑的 G4ip 工作扩展至直觉主义模态逻辑，修正了早期版本的定理错误。
2026-08-24 math.LO
Esakia's theorem for the amended monadic intuitionistic calculus
New Mexico State University（新墨西哥州立大学）；University of Milan（米兰大学）
该研究证明修正的单子直觉逻辑M^+IPC的Esakia定理成立，揭示了其与修正的单子Grzegorczyk逻辑之间的关系。
2025-12-19 math.LO
Intuitionistic Monotone Modal Logic: Proof Theory and Semantics
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Bern（伯尔尼大学）
研究直觉主义单调模态逻辑IM，通过构造性邻域模型刻画其自然扩展族，提出基于经典单调模态逻辑M的结构演算，证明IM的可判定性，揭示M与K的构造性和直觉主义变体之间的类比。
2026-07-01 cs.LO math.LO
Strong standard completeness theorems for S5-modal Lukasiewicz logics
本文研究基于Łukasiewicz t-范数的逻辑的S5模态扩张，通过构造有穷命题演算并引入无穷规则，借助monadic MV-代数的函数表示与有限嵌入性质，证明了有限强完备性与强完备性定理，并推广到有界论域模型。
2024-08-08 math.LO
Failure of Esakia's theorem in the monadic setting
New Mexico State University（新墨西哥州立大学）；University of Milan（米兰大学）
单子设定下，直觉谓词演算的一元片段不存在最大模态陪从，推翻了Esakia定理。
2026-08-18 math.LO
Game semantics for the constructive $μ$-calculus
本文为构造性$μ$-演算提出博弈语义，证明其与双关系语义等价，并借此证明$μ$-演算在$\mathsf{IS5}$上坍缩为模态逻辑，同时给出扩展不动点算子的$\mathsf{IS5}$完备性。
2024-10-01 cs.LO math.LO
Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
我们提出了一种允许非良基证明的模态Grzegorczyk逻辑Grz的演算，并通过构造作用于这些证明的连续割消映射，得到了它的割消定理。
2017-04-11 math.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
Non-Well-Founded Proofs for the Grzegorczyk Modal Logic
我们提出了一个Grzegorczyk模态逻辑Grz允许循环和其他非良基证明，并通过构造一个连续的切割消除映射作用于这些证明，得到它的切割消除定理。作为应用，我们从理论上证明了逻辑Grz的Lyndon插值性质。
2018-04-03 math.LO
Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs
我们提出了一个弱Grzegorczyk逻辑Go允许非良基证明和切消定理，它通过构造一个连续的切消映射作用于这些证明。
2018-04-03 math.LO
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
在本文中，我们介绍了一个一般家庭的序列式演算的模态语言及其片段，以捕捉所有建设性的可接受的系统的本质。称这些演算为\emph{constructive}，我们表明，任何足够强的建设性的微积分，满足一个温和的技术条件，可行地承认所有的Visser规则，即，有一种多项式时间算法，它读取维塞尔规则的前提的证明，并为其结论提供证明。作为一个积极的应用，我们证明了Visser规则在直觉模态逻辑的几个演算中的可行容许性，这些演算包括$\mathsf{CK}$，$\mathsf{IK}$及其由模态公理$T$，$B$，$4$，$5$，有界宽度和深度的模态公理以及命题逻辑的扩展。在消极的一面，我们表明，如果一个足够强大的直觉模态逻辑（满足一个温和的技术条件）不承认至少一个Visser的规则，那么它不能有一个建设性的逻辑演算。因此，除了$\mathsf{IPC}$之外，没有中间逻辑具有构造性的构造演算。
2022-10-16 cs.LO math.LO
Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies
在以前的文件中，已经提出了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作扩展了这样的演算多模态逻辑与传递关系和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。所考虑的逻辑的终止，声音和完整的演算的存在证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑产生可判定的逻辑。
2013-12-10 cs.LO math.LO
$\aleph_1$ and the modal $μ$-calculus
本文研究模态 μ-演算公式的 κ-连续性，定义片段 C_ℵ₁(x)，证明其所有公式 ℵ₁-连续，并给出判定准则，进而刻画闭包序数，证明 ω₁ 是闭包序数且闭包序数对加法封闭。
2019-10-03 cs.LO math.LO
A note on the incompleteness of Afshari & Leigh's system Clo
本文针对 Afshari 与 Leigh 为模态 μ-演算提出的循环无切割证明系统 Clo，构造一个有效但不可证明的矢列，从而证明该系统不完备。
2023-07-13 math.LO
Choice-Free de Vries Duality
De Vries对偶将布尔代数和Stone空间之间的Stone对偶推广到了de Vries代数（具有满足某些公理的从属关系的完备布尔代数）和紧T2空间之间的对偶。这种对偶性允许代数方法来处理与无点拓扑不同的基于区域的空间理论。在Bezhanishvili和Holliday最近提出的Stone对偶的无选择版本的基础上，建立了de Vries代数与一类de Vries空间之间的无选择对偶.我们还调查了连接与Vietoris函子的类别紧凑的T2空间和类别的紧凑的正则框架在点自由拓扑，我们提供了一个替代的，选择自由的拓扑语义的对称严格蕴涵演算Bezhanishvili等人。
2022-06-27 math.LO
A realization theorem for the modal logic of transitive closure $\mathsf{K}^+$
本文为传递闭包模态逻辑 $\mathsf{K}^+$ 构造对应的证成逻辑，并借助允许非良基证明的矢列演算建立了正规实现定理。
2024-09-27 math.LO
Infinitary provability logic
Ghent University（根特大学）；Steklov Mathematical Institute of the Russian Academy of Sciences（俄罗斯科学院列别捷夫数学研究所）
本文研究Gödel-Löb可证性逻辑的无穷性对应物，提出非良基深层推理系统$\dgla$，证明其相对于良基传递Kripke框架的可靠性与完备性，并借助Kripke-Platek集合论建立无穷可证性解释，表明Hilbert式变体可靠，且在某些条件下无穷可证性逻辑介于两者之间。
2026-09-22 math.LO
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.LO
On the foundations of logic and probability, II. Modal probability spaces
University of Durham（杜伦大学）
本文引入并研究一类凸显概率演算内在逻辑而非将概率赋予语句的模型，推进逻辑与概率基础的相关研究。
2026-10-21 math.LO math.PR
Categorical and Algebraic Aspects of the Intuitionistic Modal Logic $\operatorname{IEL}^{-}$ and its predicate extensions
直觉模态逻辑系统${\bf IEL}^{-}$是S. Artemov和T. Protopescu作为信念逻辑\cite{Artemov}的直觉主义版本。我们构造的模态lambda演算是Curry-Howard同构的${\bf IEL}^{-}$作为应用计算的类型理论表示广泛的功能性编程。我们还提供了一个范畴的解释，这模态lambda演算考虑coalgebras与一个monoidal函子上的一个carbohydrate闭范畴。最后，我们研究了Heyting代数和具有相应算子的locale。这种运算符也用于无点拓扑中。我们使用Goldblatt \cite{goldblatt2011cover}引入的Dedekind-MacNeille完备化和模态覆盖系统研究${\bf IEL}^{-}$及其相关逻辑的谓词扩展的完全Kripke-Joyal风格语义。本文扩展了发表在LFCS'20卷\cite{rogozin2020modal}的会议论文。
2020-12-07 math.CT math.LO
Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
UCLA Department of Philosophy（加州大学洛杉矶分校哲学系）
本文提出结合模态逻辑与简单类型λ演算的参数化系统λ_θ，通过组合逻辑给出其模型刻画，并证明λ_θ与最大系统λ_ω之间的语义守恒与可表达性结果。
2026-07-14 cs.LO math.LO
Spatial logic of modal mu-calculus and tangled closure operators
该研究将McKinsey和Tarski的拓扑模态逻辑成果拓展至模态μ演算与缠结算子逻辑，证明二者在拓扑空间上表达力等价，建立了相关逻辑的有限模型性质，拓展了剖分引理，得到多种语言在自稠密度量空间上的完备性与可靠性结果。
2016-03-05 cs.LO math.LO
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
2014-11-05 cs.LO math.LO
Complete and Terminating Tableau Calculus for Undirected Graph
本文针对无向图构造混合逻辑的表列方法，证明其完备性与终止性，并由此得出该逻辑的可判定性。
2024-11-25 cs.LO math.LO
Uniform Lyndon interpolation for intuitionistic monotone modal logic
本文证明了直觉单调模态逻辑$\mathsf{iM}$具有一致Lyndon插值性质性质（ULIP）.逻辑$\mathsf{iM}$是一种基于直觉的非正规模态逻辑，而ULIP属性是插值的加强，其中插值只依赖于蕴涵的前提或结论，并尊重命题变元的极性。我们的方法来证明ULIP产生明确的一致插值，并利用了一个终止的微积分$\mathsf{iM}$，我们已经为此目的开发。据我们所知，$\mathsf{iM}$具有ULIP和一个终止的逻辑演算的结果是第一个直觉非正规模态逻辑的结果。然而，而不是证明这些特定的结果，我们的目的是显示的建设性证明理论方法，我们用来证明ULIP的灵活性。它在过去几年中得到了发展，并已被应用于子结构，中间，经典（非）正规模态和直觉正规模态逻辑。根据这些结果，直觉非正规模态逻辑似乎是一个自然的下一类尝试应用该方法，我们在这方面迈出了第一步。
2022-08-09 cs.LO math.LO
Curry-Howard-Lambek Correspondence for Intuitionistic Belief
本文介绍了一个自然演绎演算的直觉主义逻辑信念$\mathsf{IEL}^{-}$，它很容易变成一个模态$λ$演算给出了一个计算语义的演绎$\mathsf{IEL}^{-}$。利用这种解释，还证明了$\mathsf{IEL}^{-}$具有良好的证明理论性质。演绎和类型化的条款之间的对应关系，然后扩展到一个类别语义的身份证明$\mathsf{IEL}^{-}$显示这样一个模态的一般结构的信念在直觉框架。
2020-12-15 cs.LO math.LO
Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
本文证明终止的半分析演算蕴含一致插值性质（UIP），为多种逻辑提供了统一的 UIP 证明方法，并指出模态逻辑 K4 和 S4 不存在终止的半分析演算。
2025-06-26 cs.LO math.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
