A Certified Algorithm for AC-Unification
Venue
Formal Structures for Computation and Deduction (FSCD) 2022
Publication date
Jun 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.