Ground Term Algebra 上有限生成同余关系的并
符号计算
2025-10-17 v2 计算机科学中的逻辑
摘要
我们证明了对于任意 ground term 方程系统 E 和 F，(1) E 和 F 生成的同余关系的并是 ground term 代数上的同余关系当且仅当存在一个 ground term 方程系统 H 使得 H 生成的同余关系等于 E 和 F 生成的同余关系的并当且仅当 E 和 F 的并生成的同余关系等于 E 和 F 生成的同余关系的并，且(2) Whether the congruence generated by the union of E and F is equal to the union of the congruences generated by E and F is decidable in quadratic time, where the size of the input is the number of occurrences of symbols in E plus the number of occurrences of symbols in F。
关键词
引用
@article{arxiv.2411.14559,
title = {Union of Finitely Generated Congruences on Ground Term Algebra},
author = {Sándor Vágvölgyi},
journal= {arXiv preprint arXiv:2411.14559},
year = {2025}
}
备注
57 pages