结合语义性质的结合交换同余闭包算法的模块化与组合
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
AI总结：
本文提出模块化且结合语义性质的AC同余闭包算法，避免复杂序和AC合一，适用于SMT求解器，并概述了Groebner基算法作为AC与群同余闭包的组合。
摘要：
提出了计算无解释符号以及满足结合性和交换性（AC）性质的解释符号上的基础方程的同余闭包的算法。这些算法基于一个通过将非平坦项抽象为常量来计算同余闭包的框架，该框架最初在Kapur的同余闭包算法（RTA97）中提出。该框架具有通用性、灵活性，并已扩展用于开发当结合交换函数符号可以具有额外性质（包括幂等性、幂零性、单位元、消去性和群性质）及其各种组合时的同余闭包算法。这些算法是模块化的；其正确性和终止性证明简单，利用了模块化性。与早期算法不同，所提出的算法既不依赖于非变量项上的复杂AC相容良基序，也不需要在完备化中使用结合交换合一和扩展规则来生成同余闭包的规范重写系统。它们特别适合集成到可满足性模理论（SMT）求解器中。文中概述了一种将整数系数多项式理想的格罗布纳基算法视为AC符号*（带单位元1）上的同余闭包与阿贝尔群+上的同余闭包组合的新视角。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
