本文研究符号安全协议分析中的入侵者推导问题，即判断攻击者能否利用其掌握的操作从已观测消息中推导出目标消息。尽管收敛重写系统能够提供规范形式，但模收敛理论的推导一般不可判定，现有可判定片段多由实际密码学示例驱动。本文从最小结构视角出发：当所有函数符号均为一元时，项退化为词，推导问题转化为半Thue系统的右可整除性问题——给定词 u 和 v，判断是否存在词 w 使得 wu ≡_S v。作者针对多类半Thue系统展开研究，证明了收敛的前缀擦除系统和后缀擦除系统的新可判定性结果，这是此前未知的。随后，作者将该视角扩展至项重写系统，其中规则在擦除上下文的同时提升选定的子项或变量。虽然这些类别暗示了超越一元设置的可能可判定推广，但作者进一步证明：对于收敛的同步变量提升系统，推导问题已经不可判定。这一结果揭示了将右可整除性结论推广至更丰富等式理论的可能性和局限性。本文的主要贡献在于：一方面提供了新的可判定性边界，深化了对符号协议分析中推导问题本质的理解；另一方面通过反例明确了推广的极限，有助于为自动协议验证工具的设计提供理论指导。适合对符号形式化方法、重写理论和安全协议验证感兴趣的研究人员阅读。