| ||||
| ||||
![]() Title:A Certified Algorithm for AC-Unification Authors:Mauricio Ayala-Rincón, Maribel Fernandez, Gabriel Ferreira Silva and Daniele Nantes-Sobrinho Conference:FSCD2022 Tags:AC-Unification, Certified Algorithms, Formal Methods, Interactive Theorem Proving and PVS 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. A Certified Algorithm for AC-Unification ![]() A Certified Algorithm for AC-Unification | ||||
Copyright © 2002 – 2025 EasyChair |