Equational Anti-Unification over Absorption Theories
本文提出一种基于规则的算法，解决纯吸收理论下的反合一问题，该问题为无穷的，但算法终止并给出最小完备解集的有限表示，且线性变体是有限的。
2023-10-17 cs.LO cs.SE
E-unification for Second-Order Abstract Syntax
本文提出二阶抽象语法的E-合一，融合高阶合一与等式合一思想，实现任意绑定器下的可靠且完备的合一过程。
2023-06-07 cs.LO
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
TU Dresden（德累斯顿工业大学）；Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI) Dresden/Leipzig（德累斯顿/莱比锡可扩展数据分析与人工智能中心）
本文研究了等式理论统一度在不同实例化偏序下的变化，证明了ACUI等理论在非受限偏序下为无限型，并揭示了理论类的一般性质。
2026-10-01 cs.LO
Exact Unification and Admissibility
一个新的层次结构的“确切”统一类型的介绍，动机是研究的容许规则的方程类和非经典逻辑。在这种情况下，等式类中的恒等式的统一符不是通过实例化，而是通过包含在相应的统一恒等式集合上来进行预排序。在这种新的预序下，统一子的最小完备集总是具有比标准实例化预序所提供的基数更小或相等的基数，并且在显著的情况下可以观察到显著的减少。特别地，分配格、幂等半群和MV-代数类都具有零统一型，它们具有酉或有限正合型。这些结果是通过精确统一的代数解释，灵感来自Ghilardi的代数方法方程统一。
2015-09-25 cs.LO
Unification modulo a 2-sorted Equational theory for Cipher-Decipher Block Chaining
我们调查的统一问题有关的密码块链（CBC）模式的加密。我们首先在一个简单的，收敛的，重写系统的签名与两个不相交的排序：列表和元素的链接模型。通过适当地解释该签名的特定符号，重写系统可以对感兴趣的几种实际情况进行建模。一个推理过程，提出了决定这个重写系统的统一问题模。这个过程在以下意义上是模块化的：任何给定的问题都由一个“列表推理”系统处理，因此在问题的元素项之间导出的方程组然后交给任何（“黑盒”）过程，该过程对于求解这些元素方程是完整的。该统一过程的应用的一个例子，作为攻击检测的Needham-Schroeder类协议，采用CBC加密模式的基础上的关联交换（AC）操作XOR。2排序的收敛重写系统，然后扩展到一个完全捕获块链接的解密模式在一个抽象的水平，不使用AC符号;和统一模这个扩展系统也被证明是可判定的。
2014-02-06 cs.LO
Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)
本文在 nominal 语言中引入基于置换不动点约束的 nominal 代数，将交换性无缝集成到 $α$-等价推理中，提出并证明终止且正确的模交换性 nominal 合一算法，为带绑定符和交换算子的语法结构归纳与递归提供可靠基础。
2025-03-01 cs.LO
The Undecidability of Unification Modulo $σ$ Alone
本文证明了在带显式替换的 $\lambda$-演算中，仅关于重写系统 $\sigma$ 的合一问题是不可判定的。
2023-05-09 cs.LO
A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
我们提出了形式化的证明，验证了一阶统一算法定义的可满足的约束列表生成一个最一般的统一（MGU），这也恰好是幂等的。我们所有的证明都在Coq定理证明器中得到了形式化。我们的证明表明，由统一算法产生的有限映射提供了一个模型的公理表征幂等MGU的约束列表。作为我们验证的基础的公理是从一个标准集通过将它们扩展到约束列表而得出的。对我们来说，约束是简单类型语言中术语之间的等式。使用Coq库Coq.FSets.FMapInterface将替换正式建模为有限映射。Coq的函数归纳法是证明许多公理的主要证明技术。
2010-12-22 cs.LO
On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
模单侧分配性的统一算法是Tidén和Arnborg的早期结果。最近，由于许多密码运算符满足这一性质，这一理论在密码协议分析中引起了人们的兴趣。不幸的是，该算法的文件，虽然正确的，最近已被证明不是多项式时间有界的声称。此外，对于某些情况，存在相对于输入大小呈指数级大的最一般的统一器。在本文中，我们首先提出了一个新的多项式时间算法，解决了决定问题的一个非平凡的子情况下，基于类型化理论，统一模单侧分配。接下来，我们提出了一个新的多项式算法，解决了统一模单侧分配的决策问题。一个结构，采用字符串压缩，是用来实现的多项式界。最后，我们研究了新的非对称统一范式中的单边分配问题。我们给出了单侧分配性的第一个非对称统一算法。
2015-06-18 cs.LO
On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity
我们证明了Tiden和Arnborg算法的方程统一模单侧分配性是不是多项式时间有界的，如以前所认为的。一组反例的开发表明，该算法经历了指数级的许多步骤。
2010-12-22 cs.LO cs.SC
One is all you need: Second-order Unification without First-order Variables
Czech Academy of Sciences（捷克科学院）；Dynatrace Research（Dynatrace 研究部）；RPTU Kaiserslautern（凯泽斯劳滕技术大学）
本文提出一种无需一阶变量的二阶统一度片段，证明了Hilbert第十问题可归约为该问题，从而证明了二阶统一度的不可判定性。
2026-04-08 cs.LO
On the Axiomatisation of Branching Bisimulation Congruence over CCS
在本文中，我们调查的方程理论（限制，重新标记，和递归自由片段）CCS模扎根分支双相似性，这是一个经典的，基于bisimulation的概念等价的抽象过程中的行为从内部计算步骤。首先，我们证明了CCS不是基于模所考虑的同余。作为一个关键步骤的独立利益的证明，否定的结果，我们证明了每个CCS进程有一个独特的并行分解成不可分解的过程模分支双相似性。作为第二个主要贡献，我们表明，当一组行动是有限的，根分支双相似性有一个有限的方程基础上CCS丰富的左合并和通信合并运营商从ACP。
2022-06-28 cs.LO
A Coq Formalization of Unification Modulo Exclusive-Or
针对自动定理证明和安全协议分析中的关键问题等式统一化，本文聚焦异或模统一化，在Coq中实现受Liu和Lynch启发的求解算法并证明其可靠、完备且终止，还通过代码提取得到OCaml实现。
2025-02-13 cs.CR cs.LO
Graded Quantitative Narrowing
本文提出量化窄化，将分级量化重写中的匹配推广为合一，以处理含变量项，并证明其在 Lawverean quantales 等式理论中求解量化合一问题的可靠性及完备性条件。
2025-07-25 cs.LO
Higher-Order Pattern Unification Modulo Similarity Relations
VIAM, Tbilisi State University, Georgia（VIAM，第比利斯州立大学，格鲁吉亚）；Kutaisi International University, Georgia（库塔伊国际大学，格鲁吉亚）；RISC, Johannes Kepler University, Linz, Austria（RISC，约翰尼斯·开普勒大学，林茨，奥地利）
本文提出一种将高阶模式与基于最小T范数的相似关系相结合的高阶模式合一算法，证明其终止性、可靠性和完备性，并能在可合一时计算出具有最高近似度的最一般合一子。
2025-07-17 cs.AI cs.LO math.LO
On Finite Bases for Weak Semantics: Failures versus Impossible Futures
我们提供了一个有限的基础上（在）方程理论的过程代数BCCS模弱故障前序和等价。我们也给出了积极和消极的结果，关于公理化的BCCS模弱不可能期货语义。
2008-10-27 cs.LO
Unification modulo a partial theory of exponentiation
模幂运算是现代密码学中一种常见的数学运算。这一点，以及在基和指数级别上的模乘（到不同的模），在大量的密钥协商协议中起着重要的作用。在我们的早期工作中，我们给出了许多可判定性以及不可判定性的结果，涉及到模幂运算的各种性质。在这里，我们考虑一个部分子理论只集中在指数和乘法运算符。证明了两个主要结果。第一个结果是肯定的，即，上述理论的统一问题（其中没有额外的性质是假设的乘法运算符）是可判定的。第二个结果是否定的：如果我们假设这两个乘法算子属于两个不同的交换群，那么统一问题就变得不可判定。
2010-12-22 cs.LO cs.SC
E-Generalization Using Grammars
我们将反统一的概念扩展到方程理论，并提出了一种基于正则树文法的E-推广集的有限表示的计算方法。我们提出了一个框架，结合归纳逻辑程序设计和E-推广，其中包括一个扩展的Plotkin的lgg定理方程的情况下。我们展示了潜在的权力E-推广的三个例子的应用程序：计算的建议，辅助引理方程归纳证明，计算的建设法律为给定的长期序列，学习屏幕编辑器命令序列。
2017-03-21 cs.AI cs.FL cs.LO
Bounded ACh Unification
我们考虑的统一模的方程理论ACh的问题，其中包括一个功能符号$h$，这是同态的结合交换运营商$+$。由于统一模ACh理论是不可判定的，我们定义了一个变种的问题称为\textit{bounded ACh unification}。在ACh统一的这个有界版本中，我们本质上限制了$h$可以递归地应用于一个项的次数，并且只允许满足这个限制的解决方案。术语中$h$的出现次数没有限制，并且$+$符号可以应用无限次。我们给推理规则解决有界版本的问题，并证明规则是健全的，完整的，和终止。我们已经在Maude中实现了该算法，并给出了实验结果。我们认为，该算法是有用的密码协议分析。
2019-08-25 cs.LO
Algebraic anti-unification
Vienna University of Technology（维也纳技术大学）
本文在泛代数的一般框架下提出代数反统一理论，通过引入代数泛化序和最小泛化概念，建立基本结构性质，并利用自动机理论研究有限一元代数和有限代数中的可计算性。
2026-06-01 cs.AI cs.DM cs.LO
Symbolic Analysis of Maude Theories with Narval
具有符号推理能力的并发函数式语言（如Maude）为编程和分析复杂的、高度不确定的软件系统提供了一种高级、优雅和高效的方法。Maude的符号能力基于重写理论中的等式统一和缩小，并为Maude提供高级逻辑编程能力，例如重写理论中的统一模用户可定义等式理论和符号可达性分析。复杂的计算问题可以有效地和自然地解决Maude感谢这些最近开发的符号能力和经典Maude功能的协同作用，如：（i）丰富的类型结构与排序（类型），子排序，和重载;（ii）方程重写模公理的各种组合，如结合性，交换性，和身份;和（iii）重写理论中的经典可达性分析。然而，所有这些功能的组合可能会阻碍非经验丰富的开发人员对Maude符号计算的理解。本文的目的是描述如何通过提供一个名为Narval的复杂图形工具来简化Maude重写理论的编程和分析，该工具支持Maude符号计算的细粒度检查。本文件正在考虑被TPLP接受。
2019-07-25 cs.LO cs.PL
Termination of rewrite relations on $λ$-terms based on Girard's notion of reducibility
本文将Girard为证明多态$λ$ -演算中的$β$ -约简的终止性而引入的约简概念加以推广，利用可计算闭包的概念证明了$λ$ -项上的各种重写关系的终止性，包括模某些方程理论的重写和匹配模$β$ $η$的重写.这为各种高阶重写框架提供了一个强大的终止准则，包括Klop的简单类型组合约简系统和Nipkow的高阶重写系统。
2015-09-02 cs.LO math.LO
Nominal anti-unification
我们研究名义上的反统一，这是有关计算最不一般的推广给定的条款，在上下文。一般情况下，该问题不存在最小一般解，但如果推广中允许的原子集是有限的，则存在唯一模变量重命名和$α$ -等价的最小一般推广.我们提出了一个计算它的算法，该算法依赖于一个子算法，该子算法建设性地决定上下文中两个术语之间的等方差。我们证明了这两个算法的可靠性和完备性，并分析了它们的复杂性。名义反统一可应用于需要一阶项泛化的问题（归纳学习、克隆检测等），但涉及绑定。
2025-04-29 cs.LO
Left-Linear Completion with AC Axioms
本文重新研究左线性项重写系统的模等式理论完备化，给出有限运行新正确性证明与推理系统模拟结果，证明所得完备系统的规范性，并展示左线性AC完备化可由一般AC完备化模拟以支持随时切换。
2025-04-28 cs.LO
