关联可交换同余闭包算法的模块化和组合性，附带语义属性
摘要：计算基于未解释符号和满足关联性和交换性（AC）属性的地面方程的同余闭包的算法被提出。这些算法基于通过使用常数作为抽象非平面术语的方法来计算同余闭包的框架，该方法首次在Kapur的同余闭包算法（RTA97）中提出。该框架是通用、灵活的，并且还被扩展为开发同余闭包算法，即当关联性-交换性函数符号可以具有附加属性，包括幂等性、零化性、单位元、可取消性和群特性以及其各种组合时。算法是模块化的；它们的正确性和终止证明是简单的，利用了模块化。与早期算法不同，所提出的算法既不依赖于非变量术语上复杂的AC兼容的有限序，也不需要使用关联性-交换性统一和扩展规则以生成同余闭包的规范重写系统。它们特别适合集成到满足性模理论（SMT）求解器中。还概述了一种将整数系数的多项式理想的Groebner基算法视为关联性-交换性符号*与单位元1的同余闭包与Abel群的同余闭包相结合的新方法。
作者：Deepak Kapur
论文ID：2111.04793
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22