Anti-Unification Completeness Analysis in PVS
arXiv:2607.12655 · doi:10.4204/EPTCS.448.3
The paper formally proves the completeness of a rule‑based syntactic anti‑unification algorithm within the Prototype Verification System (PVS), detailing the differences between anti‑unification and unification formalizations.
Abstract
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.
In Proceedings LFMTP 2026, arXiv:2607.10318