Dohan Kim - Congruence Closure Modulo Groups

lmcs:12387 - Logical Methods in Computer Science, February 28, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:20)2025
Congruence Closure Modulo GroupsArticle

Authors: Dohan Kim

    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.


    Volume: Volume 21, Issue 1
    Published on: February 28, 2025
    Accepted on: January 22, 2025
    Submitted on: October 10, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 435 times.
    This article's PDF has been downloaded 156 times.