arXiv · 2411.14559
Union of Finitely Generated Congruences 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$.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Sándor Vágvölgyi. 2024-11-21. Union of Finitely Generated Congruences on Ground Term Algebra. https://arxiv.org/abs/2411.14559
Cite the original work for its findings. Save a collection to share your selection of sources.