扩展字方程的可满足性：可判定与不可判定之间的边界
计算机科学中的逻辑
2018-02-05 v1 形式语言与自动机理论
摘要
字方程（或自由幺半群上方程的 existential theory）的研究是数学与理论计算机科学中的核心课题。Makanin 在 1970 年代末证明了给定字方程是否有解这一问题的可判定性，此后该课题得到了大量研究。近年来，在用于安全分析的字符串 SMT 求解器背景下，这一可判定性问题变得至关重要。此外，该理论的许多扩展（例如带长度函数上线性算术的量词免费字方程）与片段（例如对变量数目的限制）无论从理论角度还是程序分析应用角度都十分重要。受这些考量驱动，我们证明了若干新结果，从而阐明了字方程一阶理论的许多片段与扩展在可判定与不可判定之间的边界。
引用
@article{arxiv.1802.00523,
title = {The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability},
author = {Joel Day and Vijay Ganesh and Paul He and Florin Manea and Dirk Nowotka},
journal= {arXiv preprint arXiv:1802.00523},
year = {2018}
}