We present a framework for constructing congruence closure modulo permutation equations, which extends the abstract congruence closure framework for handling permutation function symbols. Our framework also handles certain interpreted function symbols satisfying each of the following properties: idempotency (I), nilpotency (N), unit (U), I U U, or N U U. Moreover, it yields convergent rewrite systems corresponding to ground equations containing permutation function symbols. We show that congruence closure modulo a given finite set of permutation equations can be constructed in polynomial time using equational inference rules, allowing us to provide a polynomial time decision procedure for the word problem for a finite set of ground equations with a fixed set of permutation function symbols.

翻译：我们提出了一个构建一致封闭模式的组合方程式框架, 用于扩展处理异位函数符号的抽象一致封闭框架。 我们的框架还处理符合下列特性的某些解释函数符号: 一流( I)、 一流( N)、 一流( U)、 单位( U)、 I U U 或 N U 。 此外, 它产生与包含异位函数符号的地面方程式相对应的聚合重写系统 。 我们显示, 一致封闭模式可以使用等式推断规则在多平衡时间构建一套限定的组合式方程式, 允许我们为一组带有固定的组合组合函数符号的有限地面方程式的单词问题提供一个多元时间决定程序 。