Formalizing Anti-Unification Algorithms in PVS
Start Year: 2025
An anti-unification problem for a family of objects of a certain type in a certain context consists in finding commonalities between those objects in order to construct generalizers that uniformly abstract over their differences subject to a preference relation for comparing them according to what constitutes a good generalization relative to the context. Anti-unification is a vital component in mathematical formalisms regarding different deductive frameworks such as proof assistants, systems for numerical, symbolic and algebraic computations, automatic deduction, and automation (Cerna and Kutsia [2023]), to cite a few.
Considering those applications and the development of the field of equational reasoning, it is pertinent to formalize, in interactive theorem provers, the mathematical properties ensuring the termination, soundness, and completeness of computational solutions for anti-unification problems modulo various algebraic theories. The only formalization of an anti-unification algorithm known to date is due to Ayala-Rincon et al. [2025] for syntactic anti-unification. The specification of the algorithm Antiunify (Ayala-Rincón et al. [2025]), together with its termination and soundness, was formalized and verified in PVS (Prototype Verification System, Owre et al. [1992]).
Although useful, algorithms for syntactic anti-unification alone cannot provide all the preferred solutions for the instances present in equational theories such as the commutative (C), associative (A) (Alpuente et al. [2014]), idempotent (I) (Cerna and Kutsia [2020a]), unital (U) (Cerna and Kutsia [2020b]), absorptive (Abs) (Ayala-Rincón [2024]) theories as well as their combinations. A very favourable aspect of the algorithm's construction and specification in PVS developed by Ayala-Rincón et al. [2025] is that the work done so far provides a very solid ground upon which algorithms for solving the anti-unification problems in first-order equational theories of extensive use can also be specified and formally mechanized.
The main goal of this project is the extension of the algorithm Antiunify to complete and sound algorithms for dealing with anti-unification modulo equational theories of extensive use, in particular anti-unificatiom modulo (Abs C)(Abs)(C). Those extensions and their mathematical properties will be also specified and verified in PVS.
References
M. Alpuente, S. Escobar, J. Espert, and J. Meseguer. A modular order-sorted equational generalization algorithm. Inf. Comput., 235:98–136, 2014. URL https://doi.org/10.1016/j.ic.2014.01.006.
M. Ayala-Rincón, D. M. Cerna, A. F. G. Barragán, and T. Kutsia. Equational anti-unification over absorption theories. In C. Benzmüller, M. J. H. Heule, and R. A. Schmidt, editors, Automated Reasoning, pages 317–337, Cham, 2024. Springer Nature Switzerland. ISBN 978-3-031-63501-4. URL https://doi.org/10.1007/978-3-031-63501-4_17.
M. Ayala-Rincón, T. A. de Lima, M. J. D. Lima, M. M. Moscato, and T. Kutsia. Verification of an anti-unification algorithm in PVS. In A. Dutle, L. Humphrey, and L. Titolo, editors, NASA Formal Methods, pages 54–71, Cham, 2025. Springer Nature Switzerland. ISBN 978-3-031-93706-4. URL https://doi.org/10.1007/978-3-031-93706-4_4.
D. M. Cerna and T. Kutsia. Idempotent Anti-Unification. ACM Trans. Comput. Log., 21(2): 10:1–10:32, 2020a. URL https://doi.org/10.1145/3359060.
D. M. Cerna and T. Kutsia. Unital Anti-Unification: Type and Algorithms. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020b). URL https://doi.org/10.4230/LIPIcs.FSCD.2020.26
D. M. Cerna and T. Kutsia. Anti-unification and generalization: A survey. In Proceedings of the 32nd Int. Joint Conference on Artificial Intelligence, IJCAI, pages 6563–6573. ijcai.org, 2023. URL https://doi.org/10.24963/ijcai.2023/736.
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th Int. Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer. URL https://doi.org/10.1007/3-540-55602-8_217.