This paper presents a new framework for constructing congruence closure of a finite set of ground equations over uninterpreted symbols and interpreted symbols for the group axioms. In this framework, ground equations are flattened into certain forms by introducing new constants, and a completion procedure is performed on ground flat equations. The proposed completion procedure uses equational inference rules and constructs a ground convergent rewrite system for congruence closure with such interpreted symbols. If the completion procedure terminates, then it yields a decision procedure for the word problem for a finite set of ground equations with respect to the group axioms. This paper also provides a sufficient terminating condition of the completion procedure for constructing a ground convergent rewrite system from ground flat equations containing interpreted symbols for the group axioms. In addition, this paper presents a new method for constructing congruence closure of a finite set of ground equations containing interpreted symbols for the semigroup, monoid, and the multiple disjoint sets of group axioms, respectively, using the proposed framework.

翻译：本文提出了一种新框架，用于在未解释符号和群公理解释符号上构建有限集基等式的同余闭包。在该框架中，通过引入新常量将基等式扁平化为特定形式，并对基扁平等式执行完备化过程。所提出的完备化过程使用等式推理规则，构建包含此类解释符号的基收敛重写系统以实现同余闭包。若该完备化过程终止，则可为群公理下有限基等式的字问题提供判定过程。本文同时给出了该完备化过程从包含群公理解释符号的基扁平等式构建基收敛重写系统的充分终止条件。此外，本文还基于该框架分别提出了针对半群、幺半群及多组不相交群公理解释符号的有限基等式集构建同余闭包的新方法。