Congruence Closure Modulo Groups
Dohan Kim
TL;DR
The paper tackles the word problem for finite sets of ground equations modulo the group axioms $G$ by introducing a three‑phase, ground completion framework that flattens terms, augments with ground instantiations entailed by $G$, and then performs a string‑based completion to produce a ground convergent rewrite system. It proves that, when termination occurs, congruence with the original equations reduces to normal forms under the combined system $(S_ ty^ hd(E)rac{gr(R(G))}{A})$, and identifies a sufficient termination condition via a monoid presentation of finite groups. The framework is shown to extend to congruence closure modulo semigroups, monoids, and multiple disjoint sets of group axioms by adjusting Phase II while reusing Phase III, and it remains purely ground, avoiding nonground interactions with $G$. The results yield a practical decision procedure for the ground word problem in these theories and suggest applications to SMT solvers and verification tools, with future work on broader algebraic structures and extensions. Overall, the work provides a simple, generic, and potentially broadly applicable approach to congruence closure in algebraic theories using ground completion on associatively flattened, ground flat equations.
Abstract
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.