Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
我们研究了在存在副作用的情况下的共代数模态逻辑来验证行为等价性，即，当余代数存在于（余）Kleisli范畴或Eilenberg-Moore范畴中时。我们的目标是开发一个基于索引类别/纤维化的一般框架，这是常见的上述类别。特别是，我们展示了如何从关系提升（一种特殊的索引态射）的行为等价的coalgebraic概念，我们给出了一个一般的配方来构建这样的提升在上述三种情况下。最后，我们应用这个框架来获得（加权）语言等价和条件双相似性的逻辑特征。
2022-02-04 cs.LO
Coalgebraic trace semantics via forgetful logics
我们使用模态逻辑作为一个框架，共代数迹语义，并显示了具体的例子，如加权，交替和树自动机的语言语义的方法的灵活性，和生成概率系统的迹语义。我们提供了一个充分条件下，通过一个给定的确定性建设获得的逻辑语义符合跟踪语义。最后，我们考虑一个条件，保证存在一个规范的确定过程，是正确的，相对于一个给定的逻辑语义。这个过程与Brzozowski的最小化算法密切相关。
2016-12-27 cs.LO
Completeness of Flat Coalgebraic Fixpoint Logics
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性中。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的定点逻辑倾向于用表达性来换取简单性和可读性，事实上，它经常存在于μ演算的单个变量片段中。这种平坦定点逻辑的家族包括，例如，LTL、CTL和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算（如交替时间时序逻辑ATL）的平坦片段，以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
2016-06-09 cs.LO
Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics
我们建立了一个通用的上限ExpTime的推理与全球的假设（也称为TBoxes）在共代数模态逻辑。与以前的结果不同，这种情况下，我们的界限不需要一个易于处理的一组Tableau规则的实例逻辑，使结果适用于更广泛的类的逻辑。例子是Presburger模态逻辑，它扩展了等级模态逻辑与后继数的线性不等式，以及概率模态逻辑与概率的多项式不等式。我们使用类型消除算法建立理论上界。我们还提供了一个全局缓存算法，潜在地避免了建立整个指数大小的候选状态空间，从而为实际推理提供了基础。该算法仍然涉及频繁的不动点计算，我们展示了如何有效地处理这些问题，在一个具体的算法建模刘和Smolka的线性时间不动点算法。最后，我们证明了上复杂度界是保持下添加名的逻辑，即在共代数混合逻辑。
2021-11-27 cs.LO
Coalgebraic Semantics for Probabilistic Logic Programming
本文提出概率逻辑编程的余代数语义，通过函子F的余代数建模程序，并利用余自由余代数给出推导树与可能世界两种语义，可恢复分布语义，并扩展至加权逻辑编程。
2021-04-09 cs.LO
Uniform Interpolation in Coalgebraic Modal Logic
一个逻辑有统一的插值，如果它的公式可以向下投影到给定的子签名，保留所有的逻辑后果，不提及删除的符号;较弱的属性（克雷格）插值允许投影公式-插值-是不同的每个逻辑后果的原始公式。这些性质是重要的，例如，逻辑理论的模块化。我们研究插值的上下文中的共代数模态逻辑，即模态逻辑公理化秩1，限制为清晰的情况下，许多模态。这种逻辑的例子包括模态逻辑K和KD，邻域逻辑及其单调变体，有限幺半群加权逻辑和联合逻辑。我们引入了一步（均匀）插值的概念，它只指一个限制逻辑没有嵌套的模态，并证明了一个共代数模态逻辑有均匀插值，如果它有一步插值。此外，我们确定保存有限的满射弱回调作为一个充分的，在单调的情况下，必要的一步插值的条件。因此，我们证明或reprove均匀插值的大多数例子上面列出的。
2022-05-01 cs.LO
Generic Trace Logics
我们结合以前的工作，共代数逻辑与共代数轨迹语义的哈苏，雅各布斯和Sokolova。
2011-03-16 cs.LO
Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations
模态逻辑的拓扑解释为拓扑空间的点的推理提供了描述语言和证明系统。最近的工作一直致力于模型检验的空间逻辑离散空间结构，如有限的图形和数字图像，在各种案例研究，包括医学图像分析的应用。这些最近的发展需要一个推广的步骤，从拓扑空间封闭空间。在这项工作中，我们开始研究的双相似性和最小化算法是一致的封闭空间的语义。为此，我们采用共代数模型。我们提出了一个coalgebraic定义的双相似性准离散模型，这是足够的空间逻辑与可达性运营商，补充有限模型的免费和开源的最小化工具。我们还讨论了非准离散的情况下，通过提供一个概括的著名的拓扑双相似性集理论的概念，和一个范畴的定义，在相同的精神作为coalgebraic渲染的邻域框架，但采用协变功率集函子，而不是逆变的。我们证明了它的充分性无穷模态逻辑。
2020-05-12 cs.LO
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
2009-02-12 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
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
On a coalgebraic view on Logic
在本文中，我们提出了从一个角度对逻辑过渡到其他方法，并特别适用于获得一个coalgebraic表示的逻辑。这个过程的核心要素是将结果关系视为范畴中的态射。
2012-02-04 cs.LO math.LO
An Expressive Coalgebraic Modal Logic for Cellular Automata
本文提出了一种用于细胞自动机的余代数模态逻辑，通过行为等价性推断其行为，并证明了Hennessy-Milner定理。
2025-12-16 cs.LO
An Inductive Construction for Many-Valued Coalgebraic Modal Logic
在本文中，我们提出了一个抽象的框架，多值模态逻辑的原子命题和模态算子的解释为谓词提升余代数上的一个endofunctor的集合范畴。它将Pattinson的共形模态逻辑分层方法推广到多值情形。与规范模型构造和过滤的标准技术相比，该方法采用归纳原理来证明逻辑的可靠性、完备性和有限模型性质。因此，我们可以解除对先前方法的限制~ \cite{Lin2022}，该方法要求底层语言必须具有内在化元级真值赋值操作的表达能力。
2022-10-24 cs.LO
Completeness-via-canonicity for coalgebraic logics
本论文旨在提供一套技术来产生具有任意秩公理的共代数逻辑的完备性结果。我们已经选择了调查的可能性，以推广什么可以说是最成功的方法之一，证明完整性的结果在“经典”模态逻辑，即完整性通过规范。这种技术特别适合于一个coalgebraic的推广，因为它的清洁和抽象的代数形式主义。
2015-10-30 cs.LO math.LO
Linear-time logics -- a coalgebraic perspective
本文从余代数视角提出一种通用框架，通过结合分支行为与线性行为类型来定义线性时间逻辑，并证明其逐步语义与基于路径的语义等价，从而支持对定量系统中线性时间性质的可能性、似然性或最小代价进行推理。
2024-06-12 cs.LO
Non-Expansive Fuzzy Coalgebraic Logic
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）
本文提出非扩展共代数模糊模态逻辑，提供PSpace中可判定的标准，并为多种定量模态逻辑提供新的PSpace上界。
2026-02-12 cs.LO
Towards a Coalgebraic Interpretation of Propositional Dynamic Logic
用Kripke模型解释命题动态逻辑要求解释Kripke模型的关系密切地观察模态算子的句法。这对通过随机Kripke模型解释PDL提出了重大挑战，因为程序的操作并不总是在随机关系集中有自然的对应物。我们使用重写规则来建立PDL的解释。它表明，每个程序对应于一个基本上是唯一的不可约树，这反过来又被分配一个谓词提升，作为程序的解释。本文建立并研究了这一解释。它讨论了概率模型的表达PDL和相关的属性，如逻辑和行为的等价性或双相似性的Kripke模型的一个密切相关的Hennessy-Milner类型的非动态逻辑的相应属性。
2011-09-16 cs.LO
Coalgebraic Fuzzy geometric logic
Jadavpur University（贾达布尔大学）；Indian Statistical Institute（印度统计研究所）
本文旨在通过在模糊几何逻辑语言中加入模态来建立一个共代数模糊几何逻辑的框架。利用余代数的方法，用模糊几何逻辑的语言引入模态算子。为了定义模态算子，我们引入了模糊开谓词提升的概念。基于模糊拓扑空间和模糊连续映射范畴$\textbf{Fuzzy-Top}$上的闭函子$T$的余代数，建立了模糊几何逻辑的余代数模型。在这项工作中讨论了定义的模型的互模拟。
2022-09-07 cs.AI cs.LO
An expressive completeness theorem for coalgebraic modal mu-calculi
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。然后，我们考虑下的行为等价的MSO公式的不变性。更具体地说，我们调查是否coalgebraic μ演算是一元二阶语言的一个给定的函子的bisimulation不变的片段。使用automatatattheoretic技术和建设最近的结果由第三作者，我们表明，为了提供这样的表征结果，它足以找到我们所谓的一个足够的一致建设的coalgebraic型函子。作为这个结果的直接应用，我们获得了部分新的证明的Janin-Walukiewicz定理的模态μ演算，避免使用语法范式，和互模拟不变的结果袋函子（分级模态逻辑）和所有指数多项式函子（包括"游戏函子"）。作为一个更复杂的应用程序，涉及额外的非平凡的想法，我们还得到了一个单调模态μ演算的特征定理，相对于自然的一元二阶语言单调邻域模型。
2017-06-30 cs.LO
Model Theory and Proof Theory of Coalgebraic Predicate Logic
本文提出一种基于Set-余代数的通用对应语言，推广一阶逻辑，研究其公理化、完备性、表达能力及模型论性质，并建立相继式系统的消割结果。
2018-03-19 cs.LO
Named Models in Coalgebraic Hybrid Logic
DFKI（德国人工智能研究中心）；Universität Bremen（不来梅大学）；Imperial College London（伦敦帝国理工学院）
混合逻辑扩展了模态逻辑，支持对由所谓的名词指定的各个状态进行推理。我们在共代数语义的广泛背景下研究混合逻辑，其中Kripke框架被替换为给定函子的共代数，从而涵盖了广泛的推理原则，包括，例如，概率、分级、默认或联合运算符。具体而言，我们建立通用标准，一个给定的共代数混合逻辑承认命名的规范模型，随后的完整性证明纯扩展一方面，和扩展的混合语言与本地绑定的其他。我们用一些例子来实例化我们的框架。值得注意的是，我们证明了具有局部约束的分次混合逻辑的完备性。
2010-02-03 cs.AI cs.LO
Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics
Kyoto University（京都大学）；University of Southampton（南安普顿大学）
本文提出延续语义用于固定点模态逻辑和计算树逻辑，证明其与合取语义等价，并重新定义了 CTL* 的模型结构。
2026-02-27 cs.LO
Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas
行为等价可以通过互模拟、模态逻辑和破坏者-复制者游戏来表征。在本文中，我们工作的一般设置的余代数，并专注于通用算法计算双方球员在互模拟游戏的获胜策略。然后将扰流器的获胜策略（如果存在）转化为区分给定非双相似状态的模态公式。公式所需的模态也是动态合成的，我们提出了一个配方，用于用不同的模态重新编码公式，由一组单独的谓词提升给出。游戏和判别公式的生成都已经在一个名为T-BEG的工具中实现。
2020-10-14 cs.LO
Fibred Coalgebraic Logic and Quantum Protocols
受应用于量子系统建模的启发，我们引入了一种新的余代数逻辑。我们的方法扩展了传统的谓词提升语义与额外的模态相关的条件不同的纤维。由于该构造的设置通常会涉及多个签名函子，因此该逻辑包含模态的演算，从而能够使用各种组合操作来构造新的模态。我们扩展的语义的共代数逻辑的设置，并证明这种扩展尊重行为等价。我们展示了如何在组合操作下保留模态的语义属性，然后应用我们的逻辑的计算方面来产生一组表达模态，用于推理量子系统，从更简单的组件构建这些模态。然后，我们展示了这些模态如何描述一些标准的量子协议。我们的逻辑的新功能，以允许统一的描述幺正演化，并支持本地推理，如“爱丽丝的量子位满足条件”是常见的讨论量子协议时。
2014-12-30 cs.LO quant-ph
Coalgebraic Modal Logic for Dynamic Systems with Uncertainty
本文提出一类包含多种不确定性测度的多项式函子，用于构造表示不确定进程的余代数，并给出相应模态逻辑的公理、推理规则及基于典范余代数的完备性证明。
2024-04-01 cs.LO math.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
Many-valued coalgebraic logic over semi-primal varieties
本文研究基于半本原真值度代数的多值余代数逻辑，提出将布尔代数簇上的自函子及经典余代数逻辑系统提升为多值逻辑的方法，并证明完备性与表达性保持，最终应用于经典模态逻辑。
2024-07-16 cs.LO math.CT 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
A Coalgebraic Semantics for Intuitionistic Modal Logic
本文利用 Esakia 空间到 Priestley 空间包含的右伴随，为带 $\Box$ 的直觉主义模态逻辑建立余代数语义，并应用于互模拟、自由模态 Heyting 代数对偶及余代数直觉主义逻辑理论。
2024-06-15 cs.LO math.LO
Disjunctive bases: normal forms and model theory for modal logics
本文提出析取基作为余代数模态逻辑的通用范式框架，证明其蕴含模拟定理和Lyndon定理，并探讨其与nabla模态的关系及构造方法。
2022-08-19 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
(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
行为等价可以通过互模拟、模态逻辑和破坏者-防御者博弈来表征。在本文中，我们回顾了这三个角度在一个coalgebraic设置，这使我们能够概括从特定的分支类型的过渡系统。我们感兴趣的定性概念（经典互模拟）以及定量概念（互模拟度量）。我们的第一个贡献是在经典的情况下，介绍了一个破坏者-防御者互模拟游戏的余代数。其次，我们介绍了这种游戏的度量的情况下，并进一步定义了一个实值模态共代数逻辑，从中我们可以得出的策略的扰流板。对于这个逻辑，我们展示了Hennessy-Milner定理的一个定量版本。
2021-04-19 cs.LO
Completeness for the coalgebraic cover modality
本文研究了L.莫斯这种逻辑的语法，这是统一介绍的coalgebraic类型函子，需要保持弱回调，扩展了经典命题逻辑与所谓的coalgebraic覆盖模态依赖于类型函子。它的语义定义在一个范畴定义的关系提升操作。作为本文的主要贡献，我们引入了一个导子系统，并证明了它为余代数有效的不等式集合提供了一个可靠而完整的公理化。我们的健全性和完整性证明是代数的，我们采用帕丁森的分层方法，表明我们的推导系统可以分层在可数层，对应于所涉及的公式的模态深度。在主要结果的证明中，我们提出了一些新的概念，并得到了一些独立的辅助结果。我们调查性质的概念，关系提升，诱导一个任意的，但固定的集函子。引入了布尔代数表示范畴，并建立了它与布尔代数表示范畴之间的一个连接。由于我们的推导系统只涉及深度为1的公式，因此可以将其编码为布尔代数上的内函子。我们证明了这个函子是有限的，并保持嵌入，我们证明了我们的逻辑的Lindenbaum-Tarski代数可以确定与初始代数这个函子。
2012-07-29 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
Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi
本文在更一般的假设下证明了余代数μ-演算可满足性检查的指数时间上界，通过通用全局缓存算法实现，并直接支持无保护公式，应用于带多项式不等式的分级μ-演算和概率μ-演算扩展。
2024-07-22 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
Optimal Satisfiability Checking for Arithmetic $μ$-Calculi
共代数$μ$演算为不动点逻辑提供了一个通用的语义框架，其分支类型超出了标准的关系设置，例如概率，加权或基于博弈。以前的工作的coalgebraic $μ$ -演算包括指数时间上界的可满足性检查，但需要一个良好的表规则的下一步模态。这样的规则并不是在所有感兴趣的情况下都可用，特别是那些涉及整数权重的情况，如分级$μ$ -演算，或者实值权重与非线性算术的组合。在本文中，我们证明了相同的复杂性上限更一般的假设下，特别是关于（更简单）的可满足性问题的复杂性的基本所谓的一步逻辑，大致描述为嵌套的下一个步骤片段的逻辑。我们还提出了一个通用的全局缓存算法，是适合于实际使用，并支持对飞行可满足性检查。示例应用包括在具有Presburger算术的分级$μ$ -演算的扩展中用于可满足性检查的新指数时间上界，以及（二值）概率$μ$ -演算的扩展与多项式不等式。作为一个副结果，我们还得到了一个新的上限$\mathcal{O}(((nk)!)^2)$的最小模型大小的可满足的公式，所有的共代数$μ$ -演算，其中$n$是大小的公式和$k$的交替深度。
2019-01-15 cs.LO
Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC
Research Institute for Mathematical Sciences, Kyoto University（京都大学数学科学研究所）
本文提出一种余积框架，用于非良基证明系统，通过余积图和一般多项式函子在预她af上建模推导树，以解决GTC的全局非组合性质和无限结构问题，展示了该框架在模态mu-算术、高阶固定点逻辑及Santocanale的圆周证明系统中的应用。
2026-11-02 cs.LO
Quantum Field Theory and Coalgebraic Logic in Theoretical Computer Science
在本文中，我们建议，在范畴论的框架下，它是可能的，以证明数学和逻辑之间的\textit{dual equivalence}的$q$ -变形的Hopf余代数的范畴和QFT的$q$ -变形的Hopf代数的范畴，解释为热场论。每一对代数-余代数分别刻画了QFT系统和它的镜像热浴，从而在远离平衡的条件下持续地模拟耗散量子系统，这对生物科学也具有明显的意义。$q$ -变形的Hopf余代数和$q$ -变形的Hopf代数构成了两个对偶范畴，因为它们分别由与Bogoliubov变换有关的同一函子$T$和它的逆变应用$T^{op}$刻画.实际上，\textit{q} -变形参数与Bogoliubov角有关，并且它是有效的热参数。因此，$q$的不同值可以明确地识别并标记出量子真空的叶理过程中出现的真空。这意味着，在泛余代数的框架下，作为动力学和计算系统（“标记状态转移系统”）的一般理论，这样标记的无限多个量子真空可以被解释为“无限状态黑箱机”的最终余代数。所有这些都为基于QFT的这种共代数公式设计一类新的通用量子计算架构开辟了道路，因为它自然生成斐波那契级数的能力证明了这一点。
2016-12-29 cs.LO math-ph math.MP
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
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
本研究开发了面向代数模态不动点逻辑的通用推理器COOL 2，可实例化为多种模态逻辑的推理工具，并在多类基准集上完成了评估。
2023-06-15 cs.FL cs.LO
Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras
本文研究 Eilenberg-Moore 余代数的分级语义与分级逻辑，证明其能平滑实例化并产生表达性模态逻辑，同时通过量词值单子参数化框架涵盖等价与行为距离。
2024-04-26 cs.LO
Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics
引入博弈上的非交换序列算子$\oslash$，通过对博弈的张量积施加因果关系，从代数上捕捉博弈语义中历史敏感策略的状态存在.函子$A \oslash \_$的余代数--即从$S$到$A \oslash S$的态射--可以被看作是状态Transformers：如果$A \oslash \_$有一个最终的余代数$!A$，那么这样一个状态Transformer的变形封装了它的显式状态，这样它只在连续的调用之间共享。研究了$A \oslash \_$的最终余代数$!A$是$A$上的余自由交换余代数的载体的条件.也就是说，它是一个线性逻辑的指数模型，在这个模型中，我们可以在游戏语义设置中以共代数的方式构造命令对象，例如引用单元。证明了如果张量分解为序列，则最终余代数$!A$可被赋予余自由交换余代数的结构，如果存在从$!(A \times B)$到$!A \otimes !B$的自然同构.如果$!A$是$A \oslash \_$的双自由代数，这个条件总是满足的，但在一般情况下，有必要强加它，因为我们建立了一个例子，给出了一个sequoidally可分解的游戏类别，其中播放将被允许有超限长度。在这个范畴中，函子$A \oslash \_$的最终余代数不是A上的余自由交换余代数：我们通过明确地将函子$A \oslash \_$的最终序列与梅利斯、塔巴罗和塔森在构造余自由交换余代数时使用的作为极限…
2017-05-31 cs.LO
(Co)recursion in Logic Programming: Lazy vs Eager
CoALP（英语：CoAlgebraic Logic Programming）是逻辑编程的一种方言，旨在为逻辑编程中的递归和共递归函数带来更精确的编译时和运行时终止和生产力分析。它的第二个目标是将类似于函数定理证明器的保护惰性（共）递归引入逻辑编程。在本文中，我们解释了CoALP的懒惰特性，并将其与CoLP中的循环分析和急切执行进行了比较。最后，我们概述了未来的发展方向，在逻辑编程的守护（共）递归。
2014-05-20 cs.LO cs.PL
Minimal modal logics, constructive modal logics and their relations
提出一族对应经典模态逻辑的极小模态逻辑，通过两种独立但等价的方法定义，并揭示其与构造性模态逻辑CK的紧密关系，进而衍生出一族构造性模态逻辑。
2023-09-05 cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
本文提出了一种“模态线性逻辑”，它将直觉模态逻辑S4（IS 4）用线性逻辑来表示，建立了从IS 4到它的Girard翻译的S4-版本。它对模态逻辑的扩展是非-这是微不足道的，因为S4模态和指数模态的简单组合导致两种模态之间的不期望的相互作用。为了解决这个问题，我们引入了一个扩展的直觉乘法指数线性逻辑与模态相结合的S4模态和指数模态，并表明它承认从IS 4的声音翻译。通过Curry-Howard对应，我们进一步得到了Pfenning和Davies为分阶段计算所提出的模态微积分的交互几何机器语义。
2019-04-24 cs.LO
Steps and Traces
在余代数理论中，迹语义可以用各种不同的方式定义，包括通过代数逻辑，单子的Kleisli范畴或它的Eilenberg-Moore范畴。本文阐述了两个新的统一思想：1）余代数迹语义自然地提出了在余递归代数，2）所有三种方法出现作为相同的抽象设置的实例。我们的观点将不同的方法置于一个共同的屋檐下，并允许推导出其中一些方法重合的条件。
2020-04-11 cs.LO
Propositional modal logic with implicit modal quantification
命题项模态逻辑在具有无限多的可达性关系的Kripke结构上解释，因此语法允许变量索引模态和量化。这种逻辑是不可判定的，我们考虑一个变量自由命题的双模态逻辑与隐量化。因此，$[\forall] α$断言所有可及性关系上的必然性，而$[\exists] α$是某些可及性关系上的经典必然性。该逻辑是与一个自然的互模拟模型的关系，我们表明，该逻辑正是一个两个排序的一阶逻辑的互模拟不变片段。该逻辑很容易被看作是可判定的，并且承认有效公式的完全公理化。此外，决策过程自然地延伸到“捆绑片段”的完整术语模态逻辑。
2018-12-29 cs.LO
From Hybrid Modal Logic to Matching Logic and Back
建立在我们以前的工作混合多元模态逻辑，我们确定模态逻辑等价匹配逻辑，程序规范和验证的逻辑。这提供了一种严格的方法来在两种方法之间传输结果，这对两个系统都有好处。
2019-09-04 cs.LO
Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
Two variable fragment of Term Modal Logic
项模态逻辑（TML）是具有无限多模态的模态逻辑，在模态指数上量化，因此我们可以有$\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$形式的公式。像一阶模态逻辑一样，TML也是“臭名昭著的”不可判定的，在这个意义上，即使是非常简单的片段也是不可判定的。在本文中，我们证明了一个有趣的片段，即两个变量TML的可判定性。这与二变量一阶模态逻辑相反，二变量一阶模态逻辑是不可判定的。
2019-06-27 cs.LO
