Uniform Interpolation in Coalgebraic Modal Logic
一个逻辑有统一的插值，如果它的公式可以向下投影到给定的子签名，保留所有的逻辑后果，不提及删除的符号;较弱的属性（克雷格）插值允许投影公式-插值-是不同的每个逻辑后果的原始公式。这些性质是重要的，例如，逻辑理论的模块化。我们研究插值的上下文中的共代数模态逻辑，即模态逻辑公理化秩1，限制为清晰的情况下，许多模态。这种逻辑的例子包括模态逻辑K和KD，邻域逻辑及其单调变体，有限幺半群加权逻辑和联合逻辑。我们引入了一步（均匀）插值的概念，它只指一个限制逻辑没有嵌套的模态，并证明了一个共代数模态逻辑有均匀插值，如果它有一步插值。此外，我们确定保存有限的满射弱回调作为一个充分的，在单调的情况下，必要的一步插值的条件。因此，我们证明或reprove均匀插值的大多数例子上面列出的。
2022-05-01 cs.LO
An Inductive Construction for Many-Valued Coalgebraic Modal Logic
在本文中，我们提出了一个抽象的框架，多值模态逻辑的原子命题和模态算子的解释为谓词提升余代数上的一个endofunctor的集合范畴。它将Pattinson的共形模态逻辑分层方法推广到多值情形。与规范模型构造和过滤的标准技术相比，该方法采用归纳原理来证明逻辑的可靠性、完备性和有限模型性质。因此，我们可以解除对先前方法的限制~ \cite{Lin2022}，该方法要求底层语言必须具有内在化元级真值赋值操作的表达能力。
2022-10-24 cs.LO
A Categorical Approach to Coalgebraic Fixpoint Logic
本文提出一种基于序充实范畴的框架，将无交替不动点逻辑纳入余代数模态逻辑的对偶伴随体系，并证明最小解语义与初始代数语义等价，同时涵盖余代数$\mu$-演算、PDL及概率动态模态逻辑。
2024-04-30 cs.LO
An expressive completeness theorem for coalgebraic modal mu-calculi
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。然后，我们考虑下的行为等价的MSO公式的不变性。更具体地说，我们调查是否coalgebraic μ演算是一元二阶语言的一个给定的函子的bisimulation不变的片段。使用automatatattheoretic技术和建设最近的结果由第三作者，我们表明，为了提供这样的表征结果，它足以找到我们所谓的一个足够的一致建设的coalgebraic型函子。作为这个结果的直接应用，我们获得了部分新的证明的Janin-Walukiewicz定理的模态μ演算，避免使用语法范式，和互模拟不变的结果袋函子（分级模态逻辑）和所有指数多项式函子（包括"游戏函子"）。作为一个更复杂的应用程序，涉及额外的非平凡的想法，我们还得到了一个单调模态μ演算的特征定理，相对于自然的一元二阶语言单调邻域模型。
2017-06-30 cs.LO
Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi
本文在更一般的假设下证明了余代数μ-演算可满足性检查的指数时间上界，通过通用全局缓存算法实现，并直接支持无保护公式，应用于带多项式不等式的分级μ-演算和概率μ-演算扩展。
2024-07-22 cs.LO
Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas
行为等价可以通过互模拟、模态逻辑和破坏者-复制者游戏来表征。在本文中，我们工作的一般设置的余代数，并专注于通用算法计算双方球员在互模拟游戏的获胜策略。然后将扰流器的获胜策略（如果存在）转化为区分给定非双相似状态的模态公式。公式所需的模态也是动态合成的，我们提出了一个配方，用于用不同的模态重新编码公式，由一组单独的谓词提升给出。游戏和判别公式的生成都已经在一个名为T-BEG的工具中实现。
2020-10-14 cs.LO
Non-Expansive Fuzzy Coalgebraic Logic
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）
本文提出非扩展共代数模糊模态逻辑，提供PSpace中可判定的标准，并为多种定量模态逻辑提供新的PSpace上界。
2026-02-12 cs.LO
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
Coalgebraic Modal Logic for Dynamic Systems with Uncertainty
本文提出一类包含多种不确定性测度的多项式函子，用于构造表示不确定进程的余代数，并给出相应模态逻辑的公理、推理规则及基于典范余代数的完备性证明。
2024-04-01 cs.LO math.LO
Fibred Coalgebraic Logic and Quantum Protocols
受应用于量子系统建模的启发，我们引入了一种新的余代数逻辑。我们的方法扩展了传统的谓词提升语义与额外的模态相关的条件不同的纤维。由于该构造的设置通常会涉及多个签名函子，因此该逻辑包含模态的演算，从而能够使用各种组合操作来构造新的模态。我们扩展的语义的共代数逻辑的设置，并证明这种扩展尊重行为等价。我们展示了如何在组合操作下保留模态的语义属性，然后应用我们的逻辑的计算方面来产生一组表达模态，用于推理量子系统，从更简单的组件构建这些模态。然后，我们展示了这些模态如何描述一些标准的量子协议。我们的逻辑的新功能，以允许统一的描述幺正演化，并支持本地推理，如“爱丽丝的量子位满足条件”是常见的讨论量子协议时。
2014-12-30 cs.LO quant-ph
Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics
Kyoto University（京都大学）；University of Southampton（南安普顿大学）
本文提出延续语义用于固定点模态逻辑和计算树逻辑，证明其与合取语义等价，并重新定义了 CTL* 的模型结构。
2026-02-27 cs.LO
Coalgebraic Fuzzy geometric logic
Jadavpur University（贾达布尔大学）；Indian Statistical Institute（印度统计研究所）
本文旨在通过在模糊几何逻辑语言中加入模态来建立一个共代数模糊几何逻辑的框架。利用余代数的方法，用模糊几何逻辑的语言引入模态算子。为了定义模态算子，我们引入了模糊开谓词提升的概念。基于模糊拓扑空间和模糊连续映射范畴$\textbf{Fuzzy-Top}$上的闭函子$T$的余代数，建立了模糊几何逻辑的余代数模型。在这项工作中讨论了定义的模型的互模拟。
2022-09-07 cs.AI cs.LO
A Coalgebraic Semantics for Intuitionistic Modal Logic
本文利用 Esakia 空间到 Priestley 空间包含的右伴随，为带 $\Box$ 的直觉主义模态逻辑建立余代数语义，并应用于互模拟、自由模态 Heyting 代数对偶及余代数直觉主义逻辑理论。
2024-06-15 cs.LO math.LO
Simulations and Bisimulations For Coalgebraic Modal Logics
我们定义了一个概念的Lambda模拟的共代数模态逻辑，参数的选择Lambda的谓词提升函子T。我们证明了这个概念在几个方面是足够的：i）它保留了正公式的真值，ii）对于Lambda，单调谓词提升的分离集，Lambda-互模拟的相关概念对应于T-行为等价（此外Lambda-n-互模拟对应于T-n-行为等价），以及iii）事实上，对于Lambda-分离和T保持弱回调，双功能Lambda-互模拟是T-互模拟。从本质上讲，我们得到了一个模块化的等价概念，当与一组单独的单调谓词提升一起使用时，与T-行为等价一致，而不管T是否保留弱回调（与T-双相似性的概念不同）。
2013-04-11 cs.LO math.LO
Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations
模态逻辑的拓扑解释为拓扑空间的点的推理提供了描述语言和证明系统。最近的工作一直致力于模型检验的空间逻辑离散空间结构，如有限的图形和数字图像，在各种案例研究，包括医学图像分析的应用。这些最近的发展需要一个推广的步骤，从拓扑空间封闭空间。在这项工作中，我们开始研究的双相似性和最小化算法是一致的封闭空间的语义。为此，我们采用共代数模型。我们提出了一个coalgebraic定义的双相似性准离散模型，这是足够的空间逻辑与可达性运营商，补充有限模型的免费和开源的最小化工具。我们还讨论了非准离散的情况下，通过提供一个概括的著名的拓扑双相似性集理论的概念，和一个范畴的定义，在相同的精神作为coalgebraic渲染的邻域框架，但采用协变功率集函子，而不是逆变的。我们证明了它的充分性无穷模态逻辑。
2020-05-12 cs.LO
Optimal Satisfiability Checking for Arithmetic $μ$-Calculi
共代数$μ$演算为不动点逻辑提供了一个通用的语义框架，其分支类型超出了标准的关系设置，例如概率，加权或基于博弈。以前的工作的coalgebraic $μ$ -演算包括指数时间上界的可满足性检查，但需要一个良好的表规则的下一步模态。这样的规则并不是在所有感兴趣的情况下都可用，特别是那些涉及整数权重的情况，如分级$μ$ -演算，或者实值权重与非线性算术的组合。在本文中，我们证明了相同的复杂性上限更一般的假设下，特别是关于（更简单）的可满足性问题的复杂性的基本所谓的一步逻辑，大致描述为嵌套的下一个步骤片段的逻辑。我们还提出了一个通用的全局缓存算法，是适合于实际使用，并支持对飞行可满足性检查。示例应用包括在具有Presburger算术的分级$μ$ -演算的扩展中用于可满足性检查的新指数时间上界，以及（二值）概率$μ$ -演算的扩展与多项式不等式。作为一个副结果，我们还得到了一个新的上限$\mathcal{O}(((nk)!)^2)$的最小模型大小的可满足的公式，所有的共代数$μ$ -演算，其中$n$是大小的公式和$k$的交替深度。
2019-01-15 cs.LO
Disjunctive bases: normal forms and model theory for modal logics
本文提出析取基作为余代数模态逻辑的通用范式框架，证明其蕴含模拟定理和Lyndon定理，并探讨其与nabla模态的关系及构造方法。
2022-08-19 cs.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
Completeness for the coalgebraic cover modality
本文研究了L.莫斯这种逻辑的语法，这是统一介绍的coalgebraic类型函子，需要保持弱回调，扩展了经典命题逻辑与所谓的coalgebraic覆盖模态依赖于类型函子。它的语义定义在一个范畴定义的关系提升操作。作为本文的主要贡献，我们引入了一个导子系统，并证明了它为余代数有效的不等式集合提供了一个可靠而完整的公理化。我们的健全性和完整性证明是代数的，我们采用帕丁森的分层方法，表明我们的推导系统可以分层在可数层，对应于所涉及的公式的模态深度。在主要结果的证明中，我们提出了一些新的概念，并得到了一些独立的辅助结果。我们调查性质的概念，关系提升，诱导一个任意的，但固定的集函子。引入了布尔代数表示范畴，并建立了它与布尔代数表示范畴之间的一个连接。由于我们的推导系统只涉及深度为1的公式，因此可以将其编码为布尔代数上的内函子。我们证明了这个函子是有限的，并保持嵌入，我们证明了我们的逻辑的Lindenbaum-Tarski代数可以确定与初始代数这个函子。
2012-07-29 cs.LO math.LO
Coalgebraic trace semantics via forgetful logics
我们使用模态逻辑作为一个框架，共代数迹语义，并显示了具体的例子，如加权，交替和树自动机的语言语义的方法的灵活性，和生成概率系统的迹语义。我们提供了一个充分条件下，通过一个给定的确定性建设获得的逻辑语义符合跟踪语义。最后，我们考虑一个条件，保证存在一个规范的确定过程，是正确的，相对于一个给定的逻辑语义。这个过程与Brzozowski的最小化算法密切相关。
2016-12-27 cs.LO
The positivication of coalgebraic logics
我们提出了积极的共代数逻辑在充分的一般性，并展示了如何获得一个积极的共代数逻辑从布尔之一。在模型方面，这涉及到从内函子$T: Set\to Set$规范地计算内函子$T': Pos\to Pos$，在第二作者等人先前定义的称为posetification的过程中。在语法方面，它涉及到从一个语法构建函子$L: BA\to BA$规范地计算一个语法构建函子$L': DL\to DL$，在一个我们称为正化的对偶过程中。这些操作是有趣的，在自己的权利，我们明确计算的情况下，几个模态逻辑的positionifications和positivications。我们展示了如何的语义的布尔代数逻辑可以规范地解除定义其积极的片段的语义，弱完整性转移从布尔的情况下，积极的情况下。
2018-12-18 cs.LO
(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
行为等价可以通过互模拟、模态逻辑和破坏者-防御者博弈来表征。在本文中，我们回顾了这三个角度在一个coalgebraic设置，这使我们能够概括从特定的分支类型的过渡系统。我们感兴趣的定性概念（经典互模拟）以及定量概念（互模拟度量）。我们的第一个贡献是在经典的情况下，介绍了一个破坏者-防御者互模拟游戏的余代数。其次，我们介绍了这种游戏的度量的情况下，并进一步定义了一个实值模态共代数逻辑，从中我们可以得出的策略的扰流板。对于这个逻辑，我们展示了Hennessy-Milner定理的一个定量版本。
2021-04-19 cs.LO
Completeness-via-canonicity for coalgebraic logics
本论文旨在提供一套技术来产生具有任意秩公理的共代数逻辑的完备性结果。我们已经选择了调查的可能性，以推广什么可以说是最成功的方法之一，证明完整性的结果在“经典”模态逻辑，即完整性通过规范。这种技术特别适合于一个coalgebraic的推广，因为它的清洁和抽象的代数形式主义。
2015-10-30 cs.LO math.LO
Duality for Fitting's Multi-valued Modal logic via bitopology and biVietoris coalgebra
本文通过扩展双拓扑对偶性并调整双Vietoris构造至成对布尔空间范畴，为Fitting多值模态逻辑建立了双拓扑与余代数对偶性，证明了其可靠性与完备性，并确立了Hennessy-Milner性质。
2025-11-01 cs.LO
Completeness of Flat Coalgebraic Fixpoint Logics
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性中。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的定点逻辑倾向于用表达性来换取简单性和可读性，事实上，它经常存在于μ演算的单个变量片段中。这种平坦定点逻辑的家族包括，例如，LTL、CTL和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算（如交替时间时序逻辑ATL）的平坦片段，以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
2016-06-09 cs.LO
Neighbourhood Structures: Bisimilarity and Basic Model Theory
邻域结构是用于推理非正规模态逻辑的标准语义工具。所有邻域模型的逻辑称为经典模态逻辑。在余代数术语中，邻域框架是与自身合成的逆变幂集函子的余代数，记为2^2。我们使用这个coalgebraic模型来推导邻域结构之间的等价概念。2^2-双相似性和行为等价是众所周知的共代数概念，它们是不同的，因为2^2不保持弱回调。我们引入第三个，中间的概念，其见证关系，我们称之为预同余（基于推出）。我们给出了2^2-互模拟和预同余的来回式特征，我们证明了在单个余代数上，预同余捕获行为等价，并且在邻域结构之间，预同余是比2^2-互模拟更好的行为等价近似。我们还引入了邻域模型的模态饱和度的概念，并研究了它与可定义性和图像有限性的关系。我们证明了一个Hennessy-Milner定理模态饱和和图像有限邻域模型。我们的主要结果是一个类似的范Benthem的特征定理和模型理论证明克雷格插值的经典模态逻辑。
2009-04-20 cs.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
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
Towards a Coalgebraic Interpretation of Propositional Dynamic Logic
用Kripke模型解释命题动态逻辑要求解释Kripke模型的关系密切地观察模态算子的句法。这对通过随机Kripke模型解释PDL提出了重大挑战，因为程序的操作并不总是在随机关系集中有自然的对应物。我们使用重写规则来建立PDL的解释。它表明，每个程序对应于一个基本上是唯一的不可约树，这反过来又被分配一个谓词提升，作为程序的解释。本文建立并研究了这一解释。它讨论了概率模型的表达PDL和相关的属性，如逻辑和行为的等价性或双相似性的Kripke模型的一个密切相关的Hennessy-Milner类型的非动态逻辑的相应属性。
2011-09-16 cs.LO
Named Models in Coalgebraic Hybrid Logic
DFKI（德国人工智能研究中心）；Universität Bremen（不来梅大学）；Imperial College London（伦敦帝国理工学院）
混合逻辑扩展了模态逻辑，支持对由所谓的名词指定的各个状态进行推理。我们在共代数语义的广泛背景下研究混合逻辑，其中Kripke框架被替换为给定函子的共代数，从而涵盖了广泛的推理原则，包括，例如，概率、分级、默认或联合运算符。具体而言，我们建立通用标准，一个给定的共代数混合逻辑承认命名的规范模型，随后的完整性证明纯扩展一方面，和扩展的混合语言与本地绑定的其他。我们用一些例子来实例化我们的框架。值得注意的是，我们证明了具有局部约束的分次混合逻辑的完备性。
2010-02-03 cs.AI cs.LO
Many-valued coalgebraic logic over semi-primal varieties
本文研究基于半本原真值度代数的多值余代数逻辑，提出将布尔代数簇上的自函子及经典余代数逻辑系统提升为多值逻辑的方法，并证明完备性与表达性保持，最终应用于经典模态逻辑。
2024-07-16 cs.LO math.CT math.LO
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
本研究开发了面向代数模态不动点逻辑的通用推理器COOL 2，可实例化为多种模态逻辑的推理工具，并在多类基准集上完成了评估。
2023-06-15 cs.FL cs.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
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
PSPACE Bounds for Rank-1 Modal Logics
由于缺乏适用于各种逻辑的通用算法方法，为给定的模态逻辑建立复杂性界限通常是一项艰巨的任务。目前的工作是一个一般理论的复杂性模态逻辑的一步。我们的主要结果是，所有秩1逻辑享有浅模型属性，因此，在温和的假设下，其axiomatisation格式，在PSPACE。这导致了一个统一的推导紧PSPACE边界的一些逻辑，包括K，KD，联盟逻辑，分级模态逻辑，多数逻辑和概率模态逻辑。此外，我们的通用算法发现，见证愉快的证明理论的性质，包括一个弱子公式属性的Tableau证明。这种普遍性是由一个coalgebraic语义，方便地抽象的细节，一个给定的模型类，从而允许覆盖范围广泛的逻辑在一个统一的方式。
2007-06-27 cs.CC cs.LO
Quantitative Graded Semantics and Spectra of Behavioural Metrics
本文提出定量分级语义框架，统一处理行为度量谱，并给出实值模态逻辑刻画行为距离的一般准则，应用于模糊度量转移系统获得新的迹距离特征逻辑。
2025-01-27 cs.LO
Explaining Behavioural Inequivalence Generically in Quasilinear Time
我们提供了一个通用的算法，用于构建公式，区分行为上不等价的状态，在系统中的各种过渡类型，如不确定性，概率或加权;通用性的过渡类型是通过与一组函子在通用余代数的范式与余代数。对于给定系统中的每个行为等价类，我们构造一个公式，该公式恰好在该类中的状态下成立。该算法实例化到确定性有限自动机，过渡系统，标记马尔可夫链，和许多其他类型的系统。环境逻辑是一种模态逻辑，其特征是从函子中提取的模态;这些模态可以在后处理步骤中系统地转换为自定义模态集。新算法建立在现有的共代数划分细化算法。它在具有$n$状态和$m$跃迁的系统上运行时间$\mathcal{O}((m+n) \log n)$，并且相同的渐近界适用于它构造的公式的dag大小。与以前的算法相比，这提高了运行时间和公式大小的界限，甚至对于以前已知的特定实例，即过渡系统和马尔可夫链;特别是，过渡系统的最佳前界是$\mathcal{O}(m n)$。
2021-09-28 cs.LO
Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence
本文提出一种通用余代数算法，在拟线性时间O((m+n) log n)内为多种转移系统构造区分行为不等价状态的模态公式，显著优于先前O(mn)的界限。
2023-11-17 cs.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
Logic-Induced Bisimulations
对于由逻辑连接给出的共代数模态逻辑，我们定义了一个新的逻辑诱导的互模拟概念（称为$ρ$ -互模拟），并研究了它的性质。我们表明，它是结构的意义上说，它是只在定义方面的余代数结构和一步模态语义，而且，可以通过一种形式的关系提升的特点。此外，我们比较$ρ$ -互模拟几个著名的等价概念，我们证明了两个模型之间的互模拟的集合往往形成一个完整的晶格。主要的技术结果是一个Hennessy-Milner型定理，它指出，在某些条件下，逻辑等价意味着$ρ$ -双相似性。特别地，后者不依赖于函子\emph{not}（余代数的类型）和$\mathsf{L}$（给出逻辑）之间的对偶性，也不依赖于逻辑连接$ρ$的属性。
2020-08-21 cs.LO math.LO
On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics
在过去的几十年里，大量的努力投入到确定一阶逻辑的可判定片段。这种努力产生了，除其他外，两个变量的片段和守卫片段，这取决于对语言公式施加的限制类型。尽管上述逻辑在形式化验证和知识表示等领域取得了成功，但这种一阶片段太弱，无法表达影响网络建模或统计推理所需的最简单的统计约束。在这项工作中，我们研究了这些经典的可判定逻辑与百分比量词的扩展，指定如何频繁的一个公式是满足缩进模型。令人惊讶的是，我们发现，所有提到的可判定的片段成为不可判定下这样的扩展，锐化文献中现有的结果。我们的负面结果补充的决定性的两个变量的守卫片段，甚至更有表现力的计数，即Presburger约束。我们的研究结果可以应用于推断各种模态和描述逻辑，如Presburger模态逻辑与逆向或ALCI，表达基数约束的可判定性。
2021-10-03 cs.LO
Transfinite Modal Logic: a Semi-quantitative Explanation for Bayesian Reasoning
Japan Advanced Institute of Science and Technology（日本北陆先端科学技术大学院大学）
贝叶斯推理在人类理性和机器学习中起着重要的作用。本文介绍了超限模态逻辑，它将模态逻辑与序数运算相结合，半定量地形式化贝叶斯推理。在技术上，我们首先研究了序数算术的一些非平凡性质，然后使我们能够自然和优雅地扩展正常模态逻辑的语义到新的超限模态逻辑上，同时仍然保持Kripke模型的普通定义完全不变。尽管所有的超限数学定义，我们认为，在实践中，这种逻辑实际上可以适应一个完全有限的解释。我们认为，超限模态逻辑以一种相当简单明了的形式抓住了贝叶斯推理的本质，特别是它为福尔摩斯的名言“当你排除了不可能，剩下的无论多么不可能，都一定是真理”提供了一个完美的解释。“我们还证明了我们的逻辑的有限模型性质定理的对应。
2022-04-02 cs.AI cs.LO math.LO
Lecture Notes on Verifying Graph Neural Networks
ENS de Lyon（里昂高等师范学院）
本文回顾了图神经网络与多种逻辑的联系，提出了一种包含线性不等式中计数模态的模态逻辑以解决图神经网络验证任务，并给出了基于tableau方法扩展的可满足性算法。
2025-10-13 cs.LG cs.LO
Differential Equations as Fixpoints and Games
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
研究通过证明一阶博弈逻辑GL与一阶模态μ-演算L_mu等表达且等价，统一博弈与不动点。还证明了微分方程扩展dGL和微分模态μ-演算的等表达性与等价性，可对常微分方程完全公理化，通过证明搜索判定其性质，有理博弈得出dGL的强算术完备性定理。
2026-09-21 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
Discrete Linear Ensemble Logic
Institute of Computer Science, Leipzig University（莱比锡大学计算机研究所）；The University of Texas Health Science Center at Houston（德克萨斯大学健康科学中心休斯顿分校）
针对生物医学知识统一符号层需求，研究自然数上离散集成逻辑$\text{EL}(\text{Nat})$，给出语法语义、嵌入结果、复杂度与表达力结论，并提出相对完备的$\text{HEL}$证明系统。
2026-08-13 cs.LO
Lewis and Brouwer meet Strong Löb
本研究在构造性Löb逻辑中考察“强度”原理，给出可证性逻辑核心定理的简化形式，证明两个系统的一致插值性，概述其算术解释并梳理与计算机科学的关联。
2024-04-18 cs.LO math.LO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.LO
