Union of Finitely Generated Congruences on Ground Term Algebra

TL;DR

This paper characterizes when the union of finitely generated congruences from ground term equations forms a congruence and proves that this union's equality is decidable in quadratic time based on input size.

Contribution

It provides necessary and sufficient conditions for the union of finitely generated congruences to be a congruence and establishes a quadratic time decision procedure.

Findings

Union of congruences is a congruence iff generated by some ground equation system

Decidability of congruence union equality in quadratic time

Characterization of congruence unions on ground term algebra

Abstract

We show that for any ground term equation systems $E$ and $F$, (1) the union of the generated congruences by $E$ and $F$ is a congruence on the ground term algebra if and only if there exists a ground term equation system $H$ such that the congruence generated by $H$ is equal to the union of the congruences generated by $E$ and $F$ if and only if the congruence generated by the union of $E $ and $F$ is equal to the union of the congruences generated by $E $ and $F$, and (2) it is decidable in square time whether the congruence generated by the union of $E$ and $F$ is equal to the union of the congruences generated by $E $ and $F$, where the size of the input is the number of occurrences of symbols in $E$ plus the number of occurrences of symbols in $F$.