Certified First-Order AC-Unification and Applications

AC-unification, i.e., unification modulo Associativity and Commutativity axioms is a key component in rewrite-based programming languages and theorem provers. We have used the PVS proof assistant to specify Stickel's pioneering AC-unification algorithm and proved it to be terminating (using an elaborate lexicographic measure based on Fages' termination proof), sound, and complete. We give a detailed account of the formalisation, including descriptions of the main steps in the proofs of termination, soundness, and completeness; the files that were created along with their hierarchy and size; and a discussion about our design choices, including the consequences of our choice for the grammar of terms. We also discuss applications of the certified AC-unification algorithm, showing how the formalisation could be used as a starting point to formalise more efficient AC-unification algorithms or to test implementations of AC-unification algorithms. This formalisation has been used to obtain a certified nominal AC-matching algorithm. Also, it could serve as a basis to specify a nominal AC-unification algorithm once this open theoretical problem is solved.