变量类别模递归一阶句法统一
摘要：一阶语法统一的推广到一个变量索引是对象语言的一部分的术语代数。与一阶语法统一不同，给定问题中的变量数量不是有限绑定的，因为术语可以具有自对称子项（模索引移位），允许构造包含无限变量的无限深术语，我们称之为算术递进术语。这种构造与归纳推理有关。我们表明，称为简单线性1环的统一性是可判定的，并猜测对于较不受限制的环类是可判定的。
作者：David M. Cerna
论文ID：2306.09152
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-06