The Complexity of Defining and Separating Fixpoint Formulae in Modal Logic
TU Dortmund University（多特蒙德工业大学）；University of Warsaw（华沙大学）
研究模态不动点公式的模态可分离性问题，证明在不同模型类上其复杂度从PSpace-完全到TwoExpTime-完全不等，并给出分离子的有效构造算法。
2026-08-12 cs.LO
A Proof System with Names for Modal Mu-calculus
不动点是语义学、抽象解释和程序逻辑中的一个重要组成部分。它们添加到逻辑中可以增加相当大的表达能力。一个普遍的问题是如何定义这种逻辑的证明系统。在这里，我们将研究模态逻辑与不动点的证明系统。我们提出了一个Tableau证明系统，用于检查公式的有效性，它使用名称来跟踪不动点变量的展开，如Jungteerapanich所设计的。
2013-09-20 cs.LO
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
A Categorical Approach to Coalgebraic Fixpoint Logic
本文提出一种基于序充实范畴的框架，将无交替不动点逻辑纳入余代数模态逻辑的对偶伴随体系，并证明最小解语义与初始代数语义等价，同时涵盖余代数$\mu$-演算、PDL及概率动态模态逻辑。
2024-04-30 cs.LO
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
本研究开发了面向代数模态不动点逻辑的通用推理器COOL 2，可实例化为多种模态逻辑的推理工具，并在多类基准集上完成了评估。
2023-06-15 cs.FL cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof
本文提出一个更简单易懂的Kozen模态μ演算公理化系统完备性证明，基于Walukiewicz的原始证明进行改进。
2026-09-24 cs.FL cs.GT cs.LO
The Complexity of Model Checking Higher-Order Fixpoint Logic
高阶不动点逻辑（Higher-Order Fixpoint Logic，HFL）是简单类型λ演算和模态λ演算的混合。这使得它成为一个高度表达的时态逻辑，能够表达模态λ演算中无法表达的程序的各种有趣的正确性属性。本文给出了其模型检验问题的复杂性结果。特别是，我们认为这些片段的HFL只使用类型的有界阶k和arity m。我们建立k倍指数时间完备性的模型检验每个这样的片段。对于上界，我们使用不动点消除，以获得可达性游戏，是单指数的大小的公式和k倍指数的大小的底层过渡系统。这些博弈可以在确定性线性时间内求解。作为一个简单的结果，我们得到一个指数时间上界的表达复杂性的每个这样的片段。下界是由交替（k-1）重指数空间有界图灵机的字问题的一个简化而建立的。由于有固定的机器的类型，其字的问题已经很难相对于k倍指数时间，我们得到，作为一个推论，k倍指数时间完整性的数据复杂性的片段的HFL，提供m超过3。这也产生了表达能力的层次结构。
2007-06-29 cs.LO
Differential Equations as Fixpoints and Games
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
研究通过证明一阶博弈逻辑GL与一阶模态μ-演算L_mu等表达且等价，统一博弈与不动点。还证明了微分方程扩展dGL和微分模态μ-演算的等表达性与等价性，可对常微分方程完全公理化，通过证明搜索判定其性质，有理博弈得出dGL的强算术完备性定理。
2026-09-21 cs.LO
Asynchronous Distributed Automata: A Characterization of the Modal Mu-Fragment
我们建立了一类异步分布式自动机和一个小片段的最小不动点逻辑之间的等价性，当限制到有限有向图。更具体地说，我们考虑的逻辑是模态$μ$的片段（的变体）-允许最少固定点但禁止最大固定点的演算。相应的自动机模型使用相同的有限状态机网络，这些有限状态机以异步方式进行通信，并且其状态图必须是非循环的，除了自循环。利用与逻辑的连接，我们还证明了这些机器的表达能力是独立的消息是否可以丢失。
2017-03-06 cs.DC cs.FL cs.LO
Filtration and canonical completeness for continuous modal mu-calculi
连续模态μ演算是模态μ演算的一个片段，其中不动点算子的应用仅限于其函数解释是斯科特连续的公式，而不仅仅是单调的。通过博弈论的手段，我们表明，这个相对表现力的片段仍然允许基本模态逻辑，这是出了名的失败的充分模态μ演算：过滤和规范模型的两个重要技术。特别是，我们证明了过滤定理的公式在语言中的连续模态μ演算。因此，我们得到了有限的模型属性在广泛的模型类。此外，我们证明了，如果一个基本模态逻辑L是标准的和类的L-框架允许过滤，那么通过添加连续不动点算子L得到的逻辑是健全的和完整的关于类的L-框架。这概括了最近的结果严格较弱的片段的模态μ演算，即PDL。
2021-09-17 cs.LO
Completeness and incompleteness of basic matching logic
Intent Computing, Inc.（意图计算有限公司）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
该研究证明了单类有限签名上不含不动点的基础匹配逻辑的全局完备性，指出加入名签后对应良基演算不再全局完备，而含不动点时有效性非递归可枚举。
2026-08-14 cs.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
基于Lifschitz的最小知识否定失败逻辑的混合知识库是将描述逻辑和逻辑程序设计的表达能力结合在一种语言中的成功方法。它们的语法由Motik和Rosati定义，不允许函数符号。为了给MKNF HKB定义一个有根据的语义，Knorr等人定义了一个出现在其中的模态原子的划分，称为交替不动点划分。在本文中，我们提出了一个迭代不动点语义的HKB函数符号。我们证明，我们的语义扩展Knorr等。的，因为对于无函数的HKB，它与其交替不动点划分一致。所提出的语义适合于概率扩展与分布语义的方法，这是未来工作的主题。
2022-08-05 cs.LO
Strong completeness of modal logics over 0-dimensional metric spaces
我们证明了一些模态逻辑的强完备性结果与普遍的模态，关于他们的拓扑语义在0维稠密的度量空间。我们还使用紧性的失败来证明，对于某些语言和空间，没有标准的模态演绎系统是强完备的。
2019-11-28 cs.LO math.LO
Disjunctive bases: normal forms and model theory for modal logics
本文提出析取基作为余代数模态逻辑的通用范式框架，证明其蕴含模拟定理和Lyndon定理，并探讨其与nabla模态的关系及构造方法。
2022-08-19 cs.LO
Cyclic Proofs for iGL via Corecursion
本文通过余递归方法，为直觉主义模态逻辑 iGL 的标准演算与循环演算的等价性提供了一种替代证明。
2025-11-04 cs.LO math.LO
Fixpoint 3-valued semantics for autoepistemic logic
本文提出了一种自认知逻辑（AEL）的构造性不动点语义。这个不动点刻画了一个自认知理论的唯一但可能是三值的信念集。它可以是三值的，因为对于公式F的子类，不动点可能不指定F是否被相信。本文提出了一种自认知逻辑（AEL）的构造性三值语义。我们引入了一个派生操作符，并定义其最小不动点的语义。语义是3值的，在这个意义上，对于某些公式，最小不动点并不指定它们是否被相信。我们证明了导子算子的完全不动点对应于Moore稳定展开式。在逻辑程序的模态表示的情况下，我们的最小不动点语义表示良基语义或3值Fitting-Kunen语义（取决于所使用的嵌入）。我们表明，在计算上，我们的语义是简单的摩尔提出的语义（假设多项式层次结构不崩溃）。
1999-01-12 cs.AI cs.LO
Parity Games and Automata for Game Logic (Extended Version)
Parikh的游戏逻辑是一个类似PDL的不动点逻辑，它在单调邻域框架上解释，表示玩家在确定的两人游戏中的战略力量。博弈逻辑转化为单调$μ$ -演算的一个片段，而单调模式自动机又在表达上等价于单调模式自动机。奇偶博弈和自动机是处理模态不动点逻辑（如模态$μ$ -演算）中嵌套不动点的组合复杂性的重要工具。本文（1）讨论了邻域结构上博弈逻辑的奇偶博弈语义a，（2）利用这些博弈得到了对应于博弈逻辑的单调$μ$ -演算片段的自动机理论刻画。我们的证明广泛使用的结构，我们称之为语法图，结合了易于使用的语法树的公式与自动机的灵活性和简洁性。它们本质上是一个基于图的观点的交替树自动机，介绍了威尔克在研究模态$μ$ -演算。
2017-09-03 cs.LO
Importing soundness and completeness in modal logics
Scuola Normale Superiore di Pisa（比萨高等师范学院）
提出从表达能力更强的模态语言向较弱语言传递可靠性与完全性的通用策略，统一了多种算子可定义性概念，并通过语义不敏感性和保真翻译实现。
2026-06-24 cs.LO math.LO
Simpler completeness proofs for modal logics with intersection
有一个显着的兴趣，扩大各种模态逻辑与交叉，最突出的例子是知识和doxastic逻辑与分布式知识。这种逻辑的完备性证明往往是复杂的，特别是在标准认知逻辑中的模型类，如S5，主要是由于标准模态逻辑中模态的交集的不可定义性。在[8]中概述了S5情况的标准证明方法，后来在[13]中更详细地解释，使用“解开折叠方法”的情况来实现树状模型以处理不可定义性问题。然而，由于细节水平和对S5的依赖，这种方法不容易适应其他逻辑。在本文中，我们提出了一个更简单的证明技术，通过建立一个树状规范模型直接，这避免了复杂的过程中解开和折叠。我们证明了技术，通过显示正常模态逻辑K，D，T，B，S4和S5扩展与交叉模态的完整性。此外，这些树型规范模型是兼容的Fischer-Ladner风格的闭包，我们结合的方法来显示所提到的逻辑的完整性进一步扩展与传递关闭的联合模态PDL或认知逻辑。其中一些完备性结果是新的。
2020-04-05 cs.LO math.LO
Lewisian Fixed Points I: Two Incomparable Constructions
我们的论文是第一次研究什么可以称之为“反向数学的显式不动点”。我们研究了两种方法来构造这样的公式，其主要连接是直观的刘易斯箭头不动点。我们的主要动机来自元理论的建设性算术，但系统的问题允许几个自然语义。这些方法中的第一种，受到de Jongh和Visser的启发，结果产生了一个很好理解的模态系统。德容和桑宾的第二个理论，看起来更简单，导致了一个模态理论，证明更难以优雅的方式公理化。除了表明这两个理论是无与伦比的，我们公理化他们的加入和调查几个子理论，其公理是作为简单公式的不动点。我们还证明了它们是扩张稳定的，即它们在一个给定数论的相应非变性逻辑中的有效性转移到它的有限扩张上。
2019-05-23 cs.LO
Cut-free Completeness for Modular Hypersequent Calculi for Modal Logics K, T, and D
我们调查了最近的建议，模态hyperlipidic结石。关系超序列的解释包括沿超序列的可及性关系。这些系统给出了与Lellman的线性嵌套序列相同的超序列解释，但由Restall独立开发用于S5，并由Parisi扩展到其他正常模态逻辑。由此产生的系统遵循Dosen原则：模态规则在不同的模态逻辑中是相同的。不同的模态系统只在外部结构规则的存在或不存在方面有所不同。除了S5之外，这些系统都是模块化的，因为不同的结构规则捕获了可访问性关系的不同属性。我们提供了第一个直接的语义无割完备性证明K，T，和D，并展示了这种方法是如何失败的情况下B和S4。
2021-11-05 cs.LO math.LO
Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics
我们建立了一个通用的上限ExpTime的推理与全球的假设（也称为TBoxes）在共代数模态逻辑。与以前的结果不同，这种情况下，我们的界限不需要一个易于处理的一组Tableau规则的实例逻辑，使结果适用于更广泛的类的逻辑。例子是Presburger模态逻辑，它扩展了等级模态逻辑与后继数的线性不等式，以及概率模态逻辑与概率的多项式不等式。我们使用类型消除算法建立理论上界。我们还提供了一个全局缓存算法，潜在地避免了建立整个指数大小的候选状态空间，从而为实际推理提供了基础。该算法仍然涉及频繁的不动点计算，我们展示了如何有效地处理这些问题，在一个具体的算法建模刘和Smolka的线性时间不动点算法。最后，我们证明了上复杂度界是保持下添加名的逻辑，即在共代数混合逻辑。
2021-11-27 cs.LO
Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion
出于最近的兴趣在模型的保护（共）递归，我们研究其方程的性质。我们制定公理守护不动点算子推广的公理的迭代理论的布卢姆和Esik。这些公理的模型包括标准的（例如，基于CPO的）模型的迭代理论和模型的保护递归，如完整的度量空间或拓扑的树研究Birkedal等人。我们表明，标准的结果满足所有康威公理的一个独特的匕首操作推广到保护设置。我们还在范畴上引入了保护迹算子的概念，并证明了保护迹算子与保护不动点算子是一一对应的。我们的研究结果的目的是作为第一步，导致的分类理论的描述守护递归，因此完整性的结果涉及我们的公理守护不动点算子在未来的工作。
2013-09-04 cs.LO
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
2021-02-11 cs.LO math.LO
Light Logics and Optimal Reduction: Completeness and Complexity
初等和轻仿射逻辑中的非线性项的分类（分别为EAL，LAL）已经研究了两个不同的原因：一方面，使用LAL（EAL，resp.）证明网承认一个有保证的多项式（分别是初等的）另一方面，这些术语也可以通过使用Lamping算法的抽象版本的最优约简来评估。第一个约简是全局的，而第二个约简是局部的和异步的。我们证明，对于LAL（EAL，resp.）类型的条款，兰坪的抽象算法也承认一个多项式（小学，分别）。绑定我们还显示了它的健全性和完整性（EAL和LAL类型不动点），通过使用一个简单的几何交互模型（上下文语义）。
2007-04-19 cs.LO cs.PL
The Completeness Problem for Modal Logic
我们介绍了模态逻辑的完备性问题，并研究其复杂性。对于公式的完备性定义，给定模态逻辑的一个公式，完备性问题询问该公式对于该逻辑是否完备。我们发现，完整性和有效性具有相同的复杂性-除了某些例外，一般来说，没有完整的公式。为了证明上界，我们提出了一个非确定性的多项式时间的过程与预言PSPACE相结合的表格和互模拟测试，并确定公式是否是完整的。
2017-09-19 cs.LO
Some General Completeness Results for Propositionally Quantified Modal Logics
本文研究命题量化模态逻辑的完全性问题，证明含Barcan模式的正规逻辑在可量化一般框架下强完全，给出公式真值在框架过渡中保持的充分条件，并基于有限多样性得到一类Kripke完全的逻辑及欧几里得框架逻辑的有限公理化。
2024-06-23 cs.LO math.LO
The Arity Hierarchy in the Polyadic $μ$-Calculus
多进μ演算是一种模态不动点逻辑，其公式定义了节点的关系，而不仅仅是标记转移系统中的集合。它可以精确地表示有限图上的多项式时间可计算和互模拟不变的查询。在本文中，我们展示了一个层次结构的结果，就表达能力内的polyadic μ演算：对于每一个层次的不动点交替，更大的arity的关系产生更高的表达能力。证明使用了对角化论证。
2015-09-10 cs.LO
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
2009-02-12 cs.LO
Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach
该研究基于伴随框架，从刻画行为一致性的模态逻辑推导不动点方程，将其实例化到共代数场景，还得到线性时间下简洁的逻辑与不动点方程，并在分支、线性时间场景中验证了理论。
2024-01-31 cs.LO
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.LO
Completeness for the coalgebraic cover modality
本文研究了L.莫斯这种逻辑的语法，这是统一介绍的coalgebraic类型函子，需要保持弱回调，扩展了经典命题逻辑与所谓的coalgebraic覆盖模态依赖于类型函子。它的语义定义在一个范畴定义的关系提升操作。作为本文的主要贡献，我们引入了一个导子系统，并证明了它为余代数有效的不等式集合提供了一个可靠而完整的公理化。我们的健全性和完整性证明是代数的，我们采用帕丁森的分层方法，表明我们的推导系统可以分层在可数层，对应于所涉及的公式的模态深度。在主要结果的证明中，我们提出了一些新的概念，并得到了一些独立的辅助结果。我们调查性质的概念，关系提升，诱导一个任意的，但固定的集函子。引入了布尔代数表示范畴，并建立了它与布尔代数表示范畴之间的一个连接。由于我们的推导系统只涉及深度为1的公式，因此可以将其编码为布尔代数上的内函子。我们证明了这个函子是有限的，并保持嵌入，我们证明了我们的逻辑的Lindenbaum-Tarski代数可以确定与初始代数这个函子。
2012-07-29 cs.LO math.LO
Completeness-via-canonicity for coalgebraic logics
本论文旨在提供一套技术来产生具有任意秩公理的共代数逻辑的完备性结果。我们已经选择了调查的可能性，以推广什么可以说是最成功的方法之一，证明完整性的结果在“经典”模态逻辑，即完整性通过规范。这种技术特别适合于一个coalgebraic的推广，因为它的清洁和抽象的代数形式主义。
2015-10-30 cs.LO math.LO
Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility
Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen（格罗宁根大学伯努利数学、计算机科学与人工智能研究所）；Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）
本文提出多值余格动态逻辑框架，通过可约性证明安全性与强完备性，应用于PDL和游戏逻辑的扩展。
2026-08-14 cs.LO math.LO
Many-Valued Coalgebraic Modal Logic: One-step Completeness and Finite Model Property
本文利用谓词提升方法研究了多值形式的余代数模态逻辑。余代数，被理解为一般的转移系统，可以作为各种模态逻辑的语义结构。在余代数模态逻辑中，一个著名的结果是它的完备性可以在一步水平上确定。利用正则模型的构造方法，我们将结果推广到多值情形。我们证明了基于三种不同多值代数结构的余代数模态逻辑的结果，这三种多值代数结构包括：有限值Rukasiewicz代数，用正则常数和Baaz Delta展开的交换积分Full-Lambek代数（FL $_{ew}$ -代数），以及用赋值运算展开的FL $_{ew}$ -代数.此外，我们还利用过滤技巧证明了多值余代数模态逻辑的有限模型性质。
2022-06-15 cs.LO
An infinitary model of linear logic
在本文中，我们构造了线性逻辑关系模型的无限变体，其中指数模态被解释为有限或可数多集的集合。我们解释如何解释在这个模型中的不动点算子Y作为一个康威算子交替定义在一个归纳或共归纳的方式。然后，我们扩展的关系语义的颜色或优先级的意义上的奇偶性游戏的概念。这种扩展使我们能够定义一个新的不动点算子Y结合归纳和共归纳的政策。最后，我们勾勒出的结果模型之间的联系，递归和高阶模型检查的演算。
2015-01-28 cs.LO
Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators
University of Oxford（牛津大学）；Birkbeck, University of London（伦敦大学伯贝克学院）；Institute for Information Transmission Problems（信息传输问题研究所）；Moscow Institute of Physics and Technology（莫斯科物理技术学院）；King’s College London（伦敦国王学院）；Kyushu Sangyo University（九州产业大学）；University of Liverpool（利物浦大学）
本文研究严格正模态逻辑在meet-半格上的Kripke完备性，探讨两种语义是否定义相同后果关系。
2019-03-22 cs.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
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
A Henkin-style completeness proof for the modal logic S5
本文提出了一个最近的形式化的Henkin风格的完整性证明的命题模态逻辑S5使用精益定理证明。形式化的证明接近于Hughes和Cresswell的证明，但是这个系统基于不同的公理选择，更好地描述为一个Mendelson系统，增加了K，T，S4和B的公理方案，以及必要性规则作为推理规则。该语言有假和蕴涵作为唯一的原始逻辑连接词和必要性作为唯一的原始模态算子。完整的源代码可以在www.example.com上获得，并且已经使用Lean 3.4.2进行了类型检查。
2021-10-23 cs.LO
Modal meet-implication logic
本文扩展命题直觉主义逻辑的 meet-implication 片段，引入保持 meet 的模态，基于半格给出语义并建立对偶性，获得完备性，识别共同模态片段，并证明其为 dialgebraic 逻辑，进而获得某处可表达性。
2022-07-13 cs.LO math.LO
Nested Sequents
我们看到如何嵌套序列，超序列的自然概括，使我们能够开发一个系统的模态逻辑证明理论。与其他突出的形式主义，如显示演算和标记序列相反，嵌套序列留在模态语言中，并允许在字面意义上享受子公式属性的证明系统。在第一部分中，我们研究了一套系统的嵌套系统的所有正常模态逻辑形成的一些组合的公理的序列性，自反性，对称性，传递性和欧几里德。我们建立健全性和完整性和他们的一些良好的性质，如可逆的所有规则，结构规则的可接受性，终止证明搜索，以及句法切割消除。在第二部分中，我们研究了常识逻辑，一种具有不动点模态的模态逻辑。我们期待在两个无穷证明系统，这种逻辑：现有的一个普通序列的基础上，没有语法切割消除程序是已知的，和一个新的嵌套序列的基础上。我们看到如何嵌套的序列，在普通的序列相比，允许句法削减消除，从而使我们能够获得一个序数上限的长度证明。
2010-04-11 cs.LO math.LO
Towards a Proof Theory of Gödel Modal Logics
针对基本模态模糊逻辑的盒形和菱形片段引入了分析证明演算，该演算将模态逻辑K的Kripke语义与哥德尔逻辑的多值语义相结合.演算用于建立这些片段的完整性和复杂性结果。
2011-05-14 cs.LO math.LO
Topological Modal Logics with Difference Modality
我们考虑带有两个模态算子$\Box$和$\D$的命题模态逻辑。在拓扑语义中，$\Box$被解释为内部算子，而$\D$被解释为差。我们表明，一些重要的拓扑性质是在这种语言中表达。此外，我们提出了一些逻辑和证明f.m.p.和完备性定理。
2010-11-25 cs.LO math.LO
Distributed Automata and Logic
分布式自动机是在有限有向图上运行的有限状态机。作为同步分布式算法，它们使用它们的输入图作为一个网络，在这个网络中，相同的处理器可能进行无限次的同步轮通信。对于这些自动机的局部变体，其中轮数由常数限定，Hella等人（2012，2015）已经根据基本模态逻辑建立了逻辑表征。在这篇论文中，我们为两个更具表现力的分布式自动机类提供了类似的逻辑刻画。第一类扩展了具有全局接受条件的局部自动机，并能够在不确定性和并行计算之间交替。我们证明了它等价于图上的一元二阶逻辑。通过限制转换是不确定性或确定性的，我们也得到了两个严格较弱的变体，空性问题是可判定的。我们的第二个类的异步算法的标准概念转移到非局部分布式自动机的设置。由此产生的机器被证明是等价于一个小片段的最小不动点逻辑，更具体地说，到一个受限制的变种的模态μ演算，允许最少的不动点，但禁止最大的不动点。利用与逻辑的连接，我们还证明了这些异步自动机的表达能力是独立的消息是否可以丢失。
2018-05-16 cs.DC cs.FL cs.LO
On Guarded Transformation In The Modal Mu-Calculus
保护范式要求μ演算公式中的不动点变量在模态算子的作用域下出现。文献中包含的保护变换有效地将μ演算公式转化为保护范式。我们发现，已知的守护变换可能会导致公式大小的指数爆破，与现有的多项式行为的索赔。我们还证明了对于更宽松的向量形式的μ演算公式，任何多项式保护变换都可以得到奇偶对策的多项式解算法，其存在性是一个公开问题.我们还研究了μ演算，向量形式和层次方程系统之间的转换，这是交替奇偶树自动机的另一种语法。
2013-12-20 cs.LO
Expressiveness and Completeness in Abstraction
我们研究了在模型检验的抽象理论中出现的两个表达性概念，发现它们在一般情况下是不可比较的。特别是，我们表明，根据最广泛使用的概念，类的Kripke模态转换系统是严格的表达比类的广义Kripke模态转换系统（一个广义的变种Kripke模态转换系统配备hypertransitions）。此外，我们调查的抽象框架的能力，证明一个公式与有限的抽象模型，一个属性被称为完整性。我们从一般的角度来解决完整性问题：它依赖于某些抽象参数的方式，以及它与表达性的关系。
2012-08-14 cs.LO
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
Mathematical Institute, University of Bern（伯尔尼大学数学研究所）；School of Computer Science, University of Birimingham（伯明翰大学计算机学院）；School of Computing, The Australian National University（澳大利亚国立大学计算学院）
本文研究了构造模态逻辑CK的语义学，建立代数与双关系语义的对偶性，并由此证明了萨尔奎维斯特类型的对应性和完备性结果，以及戈德布拉特-托马森类型的框架类可定义性定理。
2026-04-13 cs.LO math.LO
Graded modal logic and counting bisimulation
本文将互模拟不变片段的刻画定理推广到分级多模态逻辑，证明其在所有及有限点态 Kripke 结构上恰好对应计数互模拟等价下保持的一阶性质。
2023-07-18 cs.LO math.LO
Logics for Epistemic Actions: Completeness, Decidability, Expressivity
我们考虑动态版本的认知逻辑，如Baltag和Moss的“认知程序的逻辑”（2004）中所阐述的。这篇论文提出了一种动态认知逻辑的逻辑语言（实际上是由动作签名参数化的语言家族）。已有研究表明，该语言的有效性是Pi-1-1-完备的，因此不存在递归公理化的完备逻辑系统，而本文则证明了无动作迭代的片段的弱完备性结果，以及无动作迭代的片段和常识的强完备性结果。我们的工作涉及到术语重写理论的迂回。该论点使用模态过滤，因此我们得到有限的模型属性，因此可判定性。我们也给我们最大的语言翻译成PDL，从而获得第二个证明的可判定性。本文最后给出了一些关于表达能力的结果。这些主要涉及比较动作迭代自由语言与模态逻辑增强传递闭包运算符。我们回答了一个自然的问题，我们通过不同的动作签名获得的语言：我们证明了一个逻辑语言与运营商的私人公告更有表现力比一个公共公告。
2022-03-13 cs.LO math.LO
Axiomatizing Propositional Dependence Logics
通过扩展已有的命题逻辑和模态逻辑的公理化，给出了命题依赖逻辑（PD）、模态依赖逻辑（MDL）和扩展模态依赖逻辑（EMDL）的完备的希尔伯特式公理化.此外，我们给新的标记tableau演算PD，MDL，和EMDL。我们证明了每一个标记的结石的合理性，完整性和终止。
2014-10-19 cs.LO math.LO
Quantum modal logic
本文形式化了最简形式的基于量子逻辑的模态逻辑，给出其关系语义与矢列演算并证明二者间的可靠性和完全性定理，为构建量子逻辑上的各类模态逻辑提供基础框架。
2025-11-13 cs.LO math.LO
