Congruence Closure Modulo Groups

TL;DR

This paper introduces a novel framework for constructing congruence closure over ground equations involving uninterpreted and interpreted symbols for group axioms, enabling decision procedures for the word problem.

Contribution

It proposes a new completion procedure and a sufficient termination condition for congruence closure with interpreted symbols, extending to semigroup, monoid, and multiple group axioms.

Findings

The completion procedure can decide the word problem when it terminates.

A new method for congruence closure with multiple group axioms is developed.

The framework provides a decision procedure for ground equations involving group axioms.

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.