Congruence closure on ground equations is a well-established, efficient algorithm for deciding ground equalities. It computes an explicit representation of the ground equivalence classes on the basis of a set of ground input equations. Then equalities are decided by membership. We generalize the ground congruence closure algorithm to non-ground equations. The algorithm also computes an explicit representation of all non-ground equivalence classes. It is terminating due to an a priori bound on the term size. By experiments we compare our new algorithm with ground congruence closure.

翻译：地面方程上的同余闭包是一种成熟高效的算法，用于判定地面等式。该算法基于一组地面输入方程，显式计算地面等价类的表示形式，进而通过成员关系判定等式。本文将地面同余闭包算法推广至非地面方程的情形。新算法同样能显式计算所有非地面等价类的表示形式，并因项尺寸存在先验上界而保证终止性。通过实验，我们将新算法与地面同余闭包算法进行了对比分析。