A Certified Functional Nominal C-Unification Algorithm.

The nominal approach allows us to extend first-order syntax and represent smoothly systems with variable bindings, using nominal atoms instead of variables and dealing with renaming through permutations of atoms. Nominal unification is, therefore, the extension of first-order unification modulo -equivalence by taking into account this nominal setting. In this work, we present a specification of a nominal C-unification algorithm (nominal unification with commutative operators) in PVS and discuss the proofs of soundness and completeness. Additionally, the algorithm has been implemented in Python. In relation to the only known specification of nominal C-unification, there are two novel features in this work: first, the formalization of a functional algorithm that can be directly executed (not just a set of non-deterministic inference rules); second, simpler proofs of termination, soundness and completeness, due to the reduction in the number of parameters of the lexicographic measure, from four parameters to only two.