Showing 1–1 of 1 results for author: de Carvalho-Segundo, W

Nominal C-Unification

Authors: Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández, Daniele Nantes-Sobrinho

Abstract: Nominal unification is an extension of first-order unification that takes into account the α-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 in… ▽ More Nominal unification is an extension of first-order unification that takes into account the α-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. △ Less

Submitted 15 September, 2017; originally announced September 2017.

Comments: Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)

Report number: LOPSTR/2017/22