Item
Levy, Jordi
Villaret i AusellÃ©, Mateu 

Nominal Unification is an extension of firstorder 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 linearlyreduce nominal unification problems to a sequence of freshness and equalities between atoms, modulo a permutation, using ideas as Paterson and Wegman for firstorder 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  
http://hdl.handle.net/2072/294833  
eng  
Dagstuhl Publishing  
AttributionNonCommercialNoDerivs 3.0 Spain  
http://creativecommons.org/licenses/byncnd/3.0/es/  
Algorismes computacionals
Computer algorithms LÃ²gica matemÃ tica Logic, Symbolic and mathematical Complexitat computacional Computational complexity 

An Efficient Nominal Unification Algorithm  
info:eurepo/semantics/article  
Recercat 