The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
Chiba University（千叶大学）
本文研究了关系 Kleene 代数带图环的等式理论，证明其为 PSPACE-完全，并探讨了扩展术语对 PSPACE-完全性的影响。
2026-07-21 cs.LO
Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements
本文研究了带变量补和常量补的 Kleene 代数项关于语言的等式理论，引入词到字母赋值证明了部分片段的可判定性，并展示了带变量补和非空常量的等式理论完备性定理。
2024-11-25 cs.LO
Axiomatization of if-then-else over monoids of possibly non-halting programs and tests
为了研究if-then-else结构在可能非停机程序和测试上的公理化，通过考虑来自抽象$C$ -代数的测试，在文献中引入了$C$ -集的概念.本文将$C$ -集的概念推广到$C$ -幺半群，它不仅包括程序的合成，也包括程序与测试的合成。对于其中$C$ -代数为adas的$C$ -幺半群类，得到了用泛函$C$ -幺半群表示的正则表示.
2017-02-19 cs.LO
Compact Quantitative Theories of Convex Algebras
CNRS & ENS de Lyon（法国国家科学研究中心与里昂高等师范学院）
本文提出紧凑量化等式理论的概念，并证明Mardare等人提出的凸代数理论是紧凑的，用于公理化有限支持概率分布上的距离。
2026-02-27 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
Monads and Quantitative Equational Theories for Nondeterminism and Probability
概率分布的凸集单子是一个众所周知的工具，用于模拟不确定性和概率计算效果的组合。在这项工作中，我们解除这单子从范畴的集合到范畴的度量空间，通过Hausdorff和Kantorovich度量提升。我们的主要结果是介绍了这解除单子的凸半格的定量方程理论，使用的框架，最近推出的Mardare，Panangelo和Plotkin的定量代数。
2020-05-15 cs.LO
Compact Quantitative Equational Theories as Monad Restrictions
CNRS and ENS de Lyon（法国国家科学研究中心与里昂高等师范学院）；ENS de Lyon（里昂高等师范学院）
本研究针对量化代数中证明因无穷规则多为无限对象的问题，基于单子限制概念，给出了紧致量化等式理论的等价范畴学刻画。
2026-10-12 cs.LO
The Algebra of Parity Games
本文基于奇偶博弈的字符串图表示，为其提供可靠且完备的公理化，使博弈可通过等式推理直接求解，并转换为具同等表达能力的符号演算。
2025-01-30 cs.LO
Coalgebraic Path Constraints
Bucknell University（巴克斯内尔大学）
本文提出等式路径约束，作为余等式的替代方法，定义了余变种并构建了最终余代数，连接到单调结构，并计算了表达余等式的颜色数上限。
2026-03-13 cs.LO
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda
这个文件提供了一个正式的证明伯克霍夫的完备性定理的多排序代数，其中指出，任何方程蕴涵有效的所有模型也是可证明的方程理论。更准确地说，如果某个方程在所有验证一组固定方程的模型中都是有效的，那么这个方程可以使用同余的证明规则从该组导出。该证明已在Agda版本2.6.2中正式化，并包含Agda标准库版本1.7，本文档复制了已注释的Agda代码。
2021-11-15 cs.LO
Hypothesis Elimination in Kleene Semirings
Kleene半环是满足Kleene代数公理减去零化公理（x.0 = 0 = 0.x）的代数结构。我们表明，Kleene半环（像Kleene代数）承认有效消除各种方程的假设，特别是Hoare公式（t=0，其中t是一个任意项）。我们的方法是纯粹的证明理论，并可用于消除霍恩假设在任何合适的霍恩方程理论。此外，它给出了一个简单的条件下，假设消除可以组合。
2014-03-12 cs.LO
Exact Unification and Admissibility
一个新的层次结构的“确切”统一类型的介绍，动机是研究的容许规则的方程类和非经典逻辑。在这种情况下，等式类中的恒等式的统一符不是通过实例化，而是通过包含在相应的统一恒等式集合上来进行预排序。在这种新的预序下，统一子的最小完备集总是具有比标准实例化预序所提供的基数更小或相等的基数，并且在显著的情况下可以观察到显著的减少。特别地，分配格、幂等半群和MV-代数类都具有零统一型，它们具有酉或有限正合型。这些结果是通过精确统一的代数解释，灵感来自Ghilardi的代数方法方程统一。
2015-09-25 cs.LO
Axiomatization of Finite Algebras
证明了有限代数的有限类A中所有有效的n元公式的集合总是正则树语言，并计算了A的有限公理集。本文对Barzdin的液流算法（Barzdin+Barzdin，1991）进行了合理的改进。对于给定的理论T，我们给出了一类原型代数A存在的充分条件。这样的集合允许我们证明T| = p简单地通过测试p是否在A中成立。
2014-03-28 cs.FL cs.LO
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
本文为无跳过指令的带测试守护克林代数（GKAT）片段建立了代数公理化，并证明了两个完备性定理，弥补了GKAT缺乏代数公理化的不足。
2024-10-01 cs.LO cs.PL
Second-Order Algebraic Theories
Fiore和Hur最近介绍了从一阶到二阶的泛代数和方程逻辑的保守扩展。二阶泛代数和二阶方程逻辑分别为变量绑定语言和参数化元变量语言提供了模型理论和形式演绎系统。这项工作完成的基础上的主题从观点的范畴代数。具体地说，本文引入了二阶代数理论的概念，发展了二阶代数理论的基本理论。建立了两个范畴等价：在句法层面上，二阶方程表示和二阶代数理论;在语义层面上，二阶代数和二阶函子模型。我们的发展包括一个数学定义的句法之间的翻译二阶方程介绍。这给出了第一个形式化的概念，如编码和转换的上下文中的语言与变量绑定。
2013-08-25 cs.LO math.CT
Free algebras of topologically enriched multi-sorted equational theories
本文将多类等式理论推广到在 Set 上拓扑的对称幺半范畴 V 中强化的情形，证明自由 T-代数可由底层经典理论的自由代数提升得到，并给出显式归纳描述。
2023-08-18 cs.LO math.CT math.GN
Closed nominal rewriting and efficiently computable nominal algebra equality
本文分析了名义代数与名义重写的关系，给出了名义理论中方程演绎的一种新的简明表述。我们利用一些新的结果，证明了一个方程理论的子类，其中名义重写提供了一个检查名义代数等式的完整过程。这个子类包含了微积分和一阶逻辑的规范。
2010-09-14 cs.LO cs.PL
Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
定量方程逻辑的框架已成功地应用于推理的载体是度量空间和操作是非扩张的代数。我们在两个正交的方向扩展这个框架：代数赋予广义度量空间结构，和操作是非扩张的提升。我们将我们的结果的代数公理化的Eukaszyk-Karmowski距离的概率分布，最近发现的应用领域的表示学习马尔可夫过程。
2022-01-22 cs.LO
The Agda Universal Algebra Library, Part 2: Structure
Agda Universal Algebra Library（UALib）是我们开发的类型和程序（定理和证明）库，用于使用Agda程序设计语言和证明助手形式化依赖类型论中的通用代数基础。UALib包含了来自泛代数、方程逻辑和模型理论的大量定义、定理和证明，并提供了许多例子，展示了归纳和依赖类型在表示和推理数学结构和方程理论方面的能力。在本文中，我们描述的类型和证明的UALib涉及同态，项，和子代数。
2021-03-16 cs.LO math.LO
A Decision Procedure for Probabilistic Kleene Algebra with Angelic Nondeterminism
Grinnell College（格林内尔学院）；Cornell University（康奈尔大学）
本文针对Ong、Ma和Kozen（2025）提出的带天使非确定性的概率Kleene代数，给出了其等式理论的判定过程及正确性证明。
2026-10-26 cs.FL cs.LO
Computer-supported Exploration of a Categorical Axiomatization of Modeloids
一个拟模型，一个特定的部分双射集，从一个结构抽象到它的部分自同构集的思想中出现。它带有一个称为导数的操作，该操作的灵感来自Escherichfeucht-Fraïssé游戏。在本文中，我们开发了一个推广的拟模型，首先到逆半群，然后到逆范畴使用公理化方法的范畴论。然后，我们表明，这种提法使一个纯粹的代数观点Escherifeucht-Fraïssé游戏。
2020-01-13 cs.LO math.AT math.CT
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
本文利用同调方法为项重写系统等价公理集的数量提供更优下界，并实现程序在64个完整TRS上验证。
2022-09-20 cs.LO math.AC math.LO
Deciding KAT and Hoare Logic with Derivatives
带测试的Kleene代数（KAT）是布尔代数（BA）和正则表达式代数Kleene代数（KA）的结合，是一个用于程序验证的方程系统。特别地，KAT包含了霍尔逻辑（PHL）的命题片段，该逻辑是用于程序的规范和验证的形式化系统，并且是当前大多数用于检查程序正确性的工具的基础。KAT的方程理论和PHL在KAT中的编码都是可判定的。在本文中，我们提出了一个新的决策过程的基础上的概念偏导数的两个KAT表达式的等价性。我们还介绍的概念，衍生模特定的方程组。有了这个，我们扩展了以前的程序来决定PHL。最后给出了一些实验结果。
2012-10-09 cs.FL cs.LO
Generalization of terms via universal algebra
IIIA – Artificial Intelligence Research Institute, CSIC – Spanish National Research Council（III A人工智能研究所，西班牙国家研究委员会）
本文通过普遍代数方法研究术语泛化问题，利用投影和正合代数分析泛化偏序和类型，并应用于代数与逻辑领域，提出若干单位型实例。
2026-10-30 cs.LO math.LO
Theorem Proving and Algebra
这本书可以被看作是一个文本的定理证明，使用技术，从一般代数，否则作为一个文本的一般代数说明和具体的实际练习，在定理证明。这本书考虑了几个不同的逻辑系统，包括一阶逻辑，霍恩子句逻辑，等式逻辑和一阶逻辑与平等。同样，几种不同的证明范式被认为是。然而，我们确实强调等式逻辑，为了简单起见，我们只使用OBJ 3软件系统，尽管它以一种相当灵活的方式使用。我们不追求机械化证明的崇高目标，就像数学家们引以为傲的那样;相反，我们寻求采取措施为计算机科学家开发软件和硬件提供有用的证明。这一较为适度的目标具有既可实现又有实际好处的优点。内容包括：多类签名、代数和同态;项代数和代换;方程和满足;条件方程;方程推导及其完备性;条件方程的推导;常数定理;理论的解释和等价;项重写、终止、汇合和范式;抽象重写系统;标准模型、抽象数据类型、初始化和归纳;重写和演绎模方程;一阶逻辑、模型和证明规划;二阶代数;排序代数和重写;模块;统一和完成;以及隐藏代数。与此同时，还将逐步介绍OBJ 3、群论应用、各种抽象数据类型（如数制、列表和堆栈）、命题演算、硬件验证、λ演算、函数程序的正确性以及其他主题。
2021-01-16 cs.LO cs.PL cs.SC
