Nominal Logic is an extension of first-order logic with equality, name-binding, name-swapping, and freshness of names. Contrarily to higher-order logic, bound variables are treated as atoms, and only free variables are proper unknowns in nominal unification. This allows "variable capture", breaking a fundamental principle of lambda-calculus. Despite this difference, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be reduced to a particular fragment of higher-order unification problems: higher-order patterns unification. This reduction proves that nominal unification can be decided in quadratic deterministic time. © 2008 Springer-Verlag.
CITATION STYLE
Levy, J., & Villaret, M. (2008). Nominal unification from a higher-order perspective. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 246–260). https://doi.org/10.1007/978-3-540-70590-1_17
Mendeley helps you to discover research relevant for your work.