AI 中文总结
该研究聚焦于 PVS 中的反合一完备性分析，通过剖析建立基于规则算法完备性的各方面，突出反合一与合一形式化差异，此前工作涉及相关算法终止性和健全性验证，此次完善了对反合一完备性的研究。
AI 中文摘要
在句法反合一中，人们关注寻找项之间的共性，同时（统一地）抽象它们的差异。七十年代反合一发展的最初目标是使归纳推理自动化。反合一技术最近的应用包括将顺序代码高效转换为并行代码、检测代码克隆以及防止软件故障。先前工作涉及在原型验证系统（PVS）中验证基于句法反合一推理规则的函数算法的终止性和健全性所需的要素。本文剖析了正式建立基于规则算法完备性所需的所有方面，突出了反合一和合一形式化中的显著差异。
英文摘要
In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification development in the seventies was to automate inductive reasoning. Recent applications of anti-unification techniques include efficiently transforming sequential code into parallel code, detecting code clones, and preventing software failures. Previous work addressed the elements required to verify, in the Prototype Verification System (PVS), termination and soundness of a functional algorithm based on inference rules for syntactic anti-unification. This paper dissects all aspects required to formally establish the completeness of the rule-based algorithm, highlighting the significant differences in the formalizations of anti-unification and unification.
CommentsIn Proceedings LFMTP 2026, arXiv:2607.10318
Journal refEPTCS 448, 2026, pp. 29-46
