{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:26Z","timestamp":1753894406878,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,2,28]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.46298\/lmcs-21(1:20)2025","type":"journal-article","created":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T10:30:11Z","timestamp":1740738611000},"source":"Crossref","is-referenced-by-count":0,"title":["Congruence Closure Modulo Groups"],"prefix":"10.46298","volume":"Volume 21, Issue 1","author":[{"given":"Dohan","family":"Kim","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2025,2,28]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/15301\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/15301\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T10:30:12Z","timestamp":1740738612000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/12387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,28]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-21(1:20)2025","relation":{"has-preprint":[{"id-type":"arxiv","id":"2310.05014v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2310.05014v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2310.05014","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2310.05014","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2025,2,28]]},"article-number":"12387"}}