一句话：提出模块化 AC 同余闭包算法，可组合幂等、可消去、群等语义性质，便于集成到 SMT 求解器。
该论文研究含未解释符号以及满足结合交换（AC）性质及其他代数性质的解释符号的地面方程组的同余闭包计算问题。已有方法通常依赖复杂的 AC 兼容良基序、AC 合一或 completion 中的扩展规则来生成规范重写系统。作者延续 Kapur（RTA97）用常量抽象非平坦项的框架，提出模块化、可组合的 AC 同余闭包算法，并扩展到幂等性、幂零性、单位元、可消去性、群性质及其组合。方法避免复杂排序与 AC 合一/扩展，正确性与终止性证明因模块化而简洁，适合集成到 SMT 求解器。论文还给出将整数系数多项式理想的 Gröbner 基算法视为 AC 同余闭包与交换群同余闭包组合的新视角。
Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing a congruence closure by abstracting nonflat terms by constants as proposed first in Kapur's congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency, identities, cancellativity and group properties as well as their various combinations. Algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into the Satisfiability modulo Theories (SMT) solvers. A new way to view Groebner basis algorithm for polynomial ideals with integer coefficients as a combination of the congruence closures over the AC symbol * with the identity 1 and the congruence closure over an Abelian group with + is outlined.
@article{paperbot2230,
title = {Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties},
author = {Deepak Kapur},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:19)2023}
}