Anti-Unification Completeness Analysis in PVS
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.
Cite
@article{arxiv.2607.12655,
title = {Anti-Unification Completeness Analysis in PVS},
author = {Mauricio Ayala-Rincón and Thaynara Arielly de Lima and Maria Júlia Dias Lima and Temur Kutsia and Marcos Mercandeli-Rodrigues},
journal= {arXiv preprint arXiv:2607.12655},
year = {2026}
}
Comments
In Proceedings LFMTP 2026, arXiv:2607.10318