To access the full text documents, please follow this link: http://hdl.handle.net/10256/8404

An Efficient Nominal Unification Algorithm
Levy, Jordi; Villaret i Ausellé, Mateu
Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo α equivalence. Here we prove that the existence of nominal unifiers can be decided in quadratic time. First, we linearly-reduce nominal unification problems to a sequence of freshness and equalities between atoms, modulo a permutation, using ideas as Paterson and Wegman for first-order unification. Second, we prove that solvability of these reduced problems may be checked in quadràtic time. Finally, we point out how using ideas of Brown and Tarjan for unbalanced merging, we could solve these reduced problems more efficiently
Algorismes computacionals
Computer algorithms
Lògica matemàtica
Logic, Symbolic and mathematical
Complexitat computacional
Computational complexity
Attribution-NonCommercial-NoDerivs 3.0 Spain
http://creativecommons.org/licenses/by-nc-nd/3.0/es/
Article
info:eu-repo/semantics/publishedVersion
Dagstuhl Publishing
         

Show full item record

Related documents

Other documents of the same author

Kutsia, Temur; Levy, Jordi; Villaret i Ausellé, Mateu
Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret i Ausellé, Mateu
López Ibáñez, Beatriz; Muñoz Solà, Víctor; Murillo Espinar, Javier; Barber, Federico; Salido, Miguel A.; Abril, Montserrat; Cervantes, Mariamar; Caro Pérez, Luis Fernando; Villaret i Ausellé, Mateu
Bofill Arasa, Miquel; Palahí i Sitges, Miquel; Suy Franch, Josep; Villaret i Ausellé, Mateu
 

Coordination

 

Supporters