A Certified Algorithm for AC-Unification
Venue
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp. 8:1–8:21
Publication Year
2022
Identifiers
- DOI: doi:10.4230/LIPIcs.FSCD.2022.8
- ISBN: 978-3-95977-233-4
Authors
- Mauricio Ayala-Rincón
- Maribel Fernández
- Gabriel Ferreira Silva
- Daniele Nantes
Abstract
Implementing unification modulo Associativity and Commutativity (AC) axioms is crucial in rewrite-based programming and theorem provers. We modify Stickel’s seminal AC-unification algorithm to avoid mutual recursion and formalise it in the PVS proof assistant. More precisely, we prove the adjusted algorithm’s termination, soundness, and completeness. To do this, we adapted Fages’ termination proof, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. This development (to the best of our knowledge) provides the first fully formalised AC-unification algorithm.