Congruence Closure Modulo Groups
Dohan KimLogical Methods in Computer Science 2025.
Abstract
his 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.
BibTeX
@article{DBLP:journals/lmcs/Kim25,
author = {Dohan Kim},
title = {Congruence Closure Modulo Groups},
journal = {Log. Methods Comput. Sci.},
volume = {21},
number = {1},
year = {2025},
url = {https://doi.org/10.46298/lmcs-21(1:20)2025},
doi = {10.46298/LMCS-21(1:20)2025},
timestamp = {Fri, 04 Apr 2025 16:39:05 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/Kim25.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}