Portal de Periódicos da CAPES

Capítulo de livro Produção Nacional Revisado por pares

BIBTEX RIS

Nominal C-Unification

2018; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-94460-9_14

1611-3349

Maurício Ayala-Rincón, Washington Luís Ribeiro de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho,

Formal Methods in Verification

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 fixed point constraints, whose solutions can be generated by algebraic techniques on combinatorics of permutations.