Nominal C-Unification
Mauricio Ayala-Rinc\'on, Washington de Carvalho-Segundo, Maribel, Fern\'andez, Daniele Nantes-Sobrinho

TL;DR
This paper introduces a sound and complete procedure for nominal C-unification, extending unification to include commutative operators within the nominal framework, formalized in Coq.
Contribution
It presents the first formalized, sound, and complete algorithm for nominal C-unification that handles commutative operators and transforms problems into fixpoint problems.
Findings
Formalized in Coq for correctness
Transforms problems into fixpoint problems
Provides algebraic solution techniques
Abstract
Nominal unification is an extension of first-order unification that takes into account the \alpha-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixpoint problems, whose solutions can be generated by algebraic techniques on combinatorics of permutations.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
