有界 ACh 合一
计算机科学中的逻辑
2020-10-14 v2
摘要
我们考虑模一个等式理论 ACh 的合一问题，该理论由一个在函数符号 上同态于结合-交换算子 的函数符号组成。由于模 ACh 理论的合一是不可判定的，我们定义该问题的一个变体，称为有界 ACh 合一。在这一有界版本的 ACh 合一中，我们本质上限制了 递归作用于一项的次数，并且只允许满足该界限的解。对一项中 的出现次数没有限制，且 符号可被无限次使用。我们给出了求解该有界问题的推理规则，并证明这些规则是可靠、完备且终止的。我们已在 Maude 中实现了该算法并给出了实验结果。我们认为该算法在密码协议分析中是有用的。
引用
@article{arxiv.1811.05602,
title = {Bounded ACh Unification},
author = {Ajay Kumar Eeralla and Christopher Lynch},
journal= {arXiv preprint arXiv:1811.05602},
year = {2020}
}