Kleene Algebras, Regular Languages and Substructural Logics
我们介绍了两个子结构命题逻辑KL，KL+，其中使用析取，融合和一元，（准）指数连接。对于这两个我们证明强完备性的解释在Kleene代数及其变体。我们还证明了强完备性的语言模型，其中每个逻辑都有不同的解释。我们表明，这两个逻辑的切割规则是可接受的，都有一个可判定的后果关系。
2014-08-26 cs.FL cs.LO
Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness
带测试的守护克莱因代数（GKAT）是KAT的一个有效片段，因为它允许等价的几乎线性可判定性。本文研究了GKAT的（余）代数性质。我们最初的重点是片段，可以区分不成功的程序执行不同的动作，通过省略所谓的提前终止公理。我们开发了一个操作（coalgebraic）和指称（代数）语义，并表明它们是一致的。然后，我们在这个语义的GKAT表达式的行为特征，导致一个coequation，捕捉对应于GKAT表达式的行为的自动机的共变。最后，我们证明了减少片段的公理是健全的和完整的w.r.t.的语义，然后建立在这个结果，以恢复一个语义，是健全的和完整的w.r.t.完整的公理集
2021-05-20 cs.LO cs.PL
Weak Kleene Algebra is Sound and (Possibly) Complete for Simulation
我们证明了弱Kleene代数（WKA）的公理对于正则表达式模模拟等价性理论是合理的和完备的，假设它们对于单调树是完备的（如Takai和Furusawa所述）。
2009-10-06 cs.LO cs.PL
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
本文为无跳过指令的带测试守护克林代数（GKAT）片段建立了代数公理化，并证明了两个完备性定理，弥补了GKAT缺乏代数公理化的不足。
2024-10-01 cs.LO cs.PL
A note on commutative Kleene algebra
本文详细证明了代数逻辑中的一个重要结果：自由交换Kleene代数是半线性集空间。这个结果的第一个证明是由Redko在1964年提出的，并由Pilling在1970年的论文中进行了简化和修正。然而，我们认为现在需要对这个证明进行新的说明。这一结果已获得了特别重要的是，在最近几年，因为它是一个关键组成部分的完整性证明的几个代数模型的并发计算（双Kleene代数，并发Kleene代数.）。为此，我们提出了一个新的证明。
2019-10-31 cs.FL cs.LO
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
带测试的Kleene代数（GKAT）是带测试的Kleene代数（KAT）的变体，它通过将KAT的并（$+$）和迭代（$*$）操作限制为谓词保护版本而产生。我们开发的（共）代数理论的GKAT和展示它如何可以有效地用于理由的命令式程序。在对比KAT，其方程理论是PSPACE-完全的，我们表明，GKAT的方程理论是（几乎）线性时间。我们还提供了一个完整的Kleene定理和证明完整性的类似Salomaa的公理化Kleene代数。
2019-12-13 cs.LO cs.PL
Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements
本文研究了带变量补和常量补的 Kleene 代数项关于语言的等式理论，引入词到字母赋值证明了部分片段的可判定性，并展示了带变量补和非空常量的等式理论完备性定理。
2024-11-25 cs.LO
*-Continuous Kleene $ω$-Algebras for Energy Problems
能量问题在嵌入式或自治系统的形式化分析中非常重要。利用最近的结果，星连续Kleene ω-代数，我们在这里表明，能源问题可以解决的代数操作的过渡矩阵的能源自动机。为此，我们证明了一般的结果，某些类的可加性函数的完整格，这应该是一个更普遍的兴趣。
2015-09-10 cs.FL cs.LO
A Unifying Categorical View of Nondeterministic Iteration and Tests
本文从范畴论视角分离并分析Kleene迭代，提出含余积与测试的Kleene迭代范畴，证明其兼容异常、存储、并发等特性，并将自由模型刻画为非确定性有理树。
2024-07-17 cs.LO
Kleene Algebra with Tests and Coq Tools for While Programs
我们提出了一个Coq库Kleene代数与测试，包括证明他们的完整性在适当的概念的语言，他们的方程理论的决策程序，并利用在这样的理论的一个特定形状的假设的工具。带有测试的Kleene代数使得在大多数命令式程序设计语言中表示if-then-else语句和while循环成为可能。它们实际上是由Kozen引入的，作为命题霍尔逻辑的替代。我们展示了如何利用相应的Coq工具的程序验证的上下文中证明等价的，而程序，正确的一些标准的编译器优化，霍尔规则的部分正确性，以及一个特别具有挑战性的等价流程图计划。
2013-02-07 cs.LO cs.MS cs.PL
The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
Chiba University（千叶大学）
本文研究了关系 Kleene 代数带图环的等式理论，证明其为 PSPACE-完全，并探讨了扩展术语对 PSPACE-完全性的影响。
2026-07-21 cs.LO
Weighted GKAT: Completeness and Complexity
本文提出了配备分支、条件和循环的非解释型加权编程语言 wGKAT，利用加权自动机变体给出其操作语义，引入了可靠且完备的公理化体系，并提供了互模拟等价的多项式时间判定过程。
2025-04-29 cs.FL cs.LO cs.PL
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity
该研究提出可对含概率分支的未解释命令式程序推理的ProbGKAT框架，给出其操作语义、互模拟的完备Salomaa式公理化，并证明可通过通用划分求精算法在O(n³ log n)时间内判定其互模拟性。
2023-05-02 cs.FL cs.LO
Higher Catoids, Higher Quantales and their Correspondences
本文引入了$ω$-catoids和$ω$-quantales作为高维重写中结构的推广，建立了它们之间的对应关系，并扩展到$(ω,p)$-catoids和卷积$(ω,p)$-quantales，为$ω$-Kleene代数和$ω$-quantale公理的系统性发展提供了支持。
2025-06-28 cs.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
Finitely-valued propositional dynamic logic
我们研究了命题动态逻辑的一个多值推广，其中Kripke模型的状态公式和状态之间的可达性关系在有限FL-代数中求值。对这个框架的一个自然的解释是关于执行结构化行动的成本的推理。证明了有限FL-代数上的PDL是可判定的。我们还建立了一类基于具有典型常数的交换积分FL-代数的PDL的一般完备性结果。
2020-12-22 cs.LO
Continuous Algebras with Hypotheses
Radboud University（拉德堡德大学）；CNRS, LIP, ENS de Lyon（法国国家科学研究中心，计算机科学与实验室，里昂高等师范学院）
本文提出一个统一的框架，涵盖Kleene代数的各种变体以及正则树语言，通过考虑由完全格有序的代数，其中可以计算最小固定点，并提供一个由封闭语言组成的标准模型，证明其在所有连续模型上都是正确且完整的。此外，本文研究了准等式公理化，并展示了如何通过模块化的方式获得完整公理化，从而在每个情况下证明了交换Kleene代数、bi-KA和正则树语言在不同假设下的完备性。
2026-07-14 cs.LO
Admissibility in Finitely Generated Quasivarieties
检查拟方程在一个随机生成（即，由有限代数的有限集合生成的）拟簇Q相当于在拟簇的适当的有限自由代数中检查有效性，因此是可判定的。然而，由于自由代数可能是大的，即使是小集合的小代数和非常少的生成元，这种天真的方法来检查在$\Q$的容许计算是不可行的。在本文中，算法的介绍，产生一个最小的（相对于一个多集良好的顺序在他们的基数）有限集的代数，使有效性的准方程在这个集合中对应的准方程在Q的容许性。特别是，结构完备性（有效性和容许性一致）和几乎结构完备性（有效性和容许性一致的准方程与统一的前提）可以检查。该算法说明了一个选择著名的生成的拟变种，并适应于处理有限值逻辑中的规则的可接受性。
2013-06-23 cs.LO math.LO
Almost structural completeness; an algebraic approach
一个演绎系统是结构完备的，如果它的容许推理规则是可导出的。对于几个重要的系统，如模态逻辑S5，结构完备性的失败仅仅是由被动规则的不可导性引起的，即规则不能应用于系统的定理。忽略被动规则会导致几乎结构完备性的概念，这意味着，可接受的非被动规则的可导性。本文用纯代数方法研究了一般代数的拟簇和簇的几乎结构完备性。结果适用于所有可代数化的演绎系统。首先，给出了几乎结构完备拟簇的各种刻画。其中两个是一般的：表示为可表示代数，和表示为亚直不可约代数。一个是有限模型的性质和方程可定义的主相对同余，其中的条件是有限次直不可约代数上可验证的拟簇。其次，几乎结构完整的品种的例子提供特别强调的是把各种各样的闭包代数，这是已知的构成足够的语义正规扩张的S4模态逻辑。一个这样的几乎结构完整，但结构不完整，品种的无限家庭被构造。这个族中的每个簇都有一个不嵌入到这个簇的任何自由代数中的可表示的可统一代数。因此，它的统一不是单一的。这表明几乎结构完备性严格弱于闭包代数簇的投射统一。
2014-08-22 cs.LO math.LO math.RA
Forcing, Transition Algebras, and Calculi
提出转移代数逻辑系统，通过引入动态逻辑特性增强多类一阶逻辑，并推广力迫方法至标记范畴，证明了具有可数无限前提证明规则的完备性。
2024-04-24 cs.LO
