@inproceedings{10.1007/978-3-540-27836-8_30,
    Abstract = {Nominal logic is a first-order theory of names and binding based on a primitive operation of swapping rather than substitution. Urban, Pitts, and Gabbay have developed a nominal unification algorithm that unifies terms up to nominal equality. However, because of nominal logic's equivariance principle, atomic formulas can be provably equivalent without being provably equal as terms, so resolution using nominal unification is sound but incomplete. For complete resolution, a more general form of unification called equivariant unification, or ``unification up to a permutation'' is required. Similarly, for rewrite rules expressed in nominal logic, a more general form of matching called equivariant matching is necessary.},
    Address = {Berlin, Heidelberg},
    Author = {Cheney, James},
    BookTitle = {Automata, Languages and Programming},
    Editor = {D{\'\i}az, Josep and Karhum{\"a}ki, Juhani and Lepist{\"o}, Arto and Sannella, Donald},
    File = {The Complexity of Equivariant Unification - complexity (0) - a - a - c.pdf},
    ISBN = {978-3-540-27836-8},
    Pages = {332--344},
    Publisher = {Springer Berlin Heidelberg},
    Title = {The Complexity of Equivariant Unification},
    Year = {2004},
    date-added = {2019-09-12 18:37:09 +0200},
    date-modified = {2019-09-12 18:37:09 +0200},
    doi = {10.1007/978-3-540-27836-8_30}
}

@inproceedings{10.1007/978-3-540-27836-8_30, Abstract = {Nominal logic is a first-order theory of names and binding based on a primitive operation of swapping rather than substitution. Urban, Pitts, and Gabbay have developed a nominal unification algorithm that unifies terms up to nominal equality. However, because of nominal logic's equivariance principle, atomic formulas can be provably equivalent without being provably equal as terms, so resolution using nominal unification is sound but incomplete. For complete resolution, a more general form of unification called equivariant unification, or ``unification up to a permutation'' is required. Similarly, for rewrite rules expressed in nominal logic, a more general form of matching called equivariant matching is necessary.}, Address = {Berlin, Heidelberg}, Author = {Cheney, James}, BookTitle = {Automata, Languages and Programming}, Editor = {D{\'\i}az, Josep and Karhum{\"a}ki, Juhani and Lepist{\"o}, Arto and Sannella, Donald}, File = {The Complexity of Equivariant Unification - complexity (0) - a - a - c.pdf}, ISBN = {978-3-540-27836-8}, Pages = {332--344}, Publisher = {Springer Berlin Heidelberg}, Title = {The Complexity of Equivariant Unification}, Year = {2004}, date-added = {2019-09-12 18:37:09 +0200}, date-modified = {2019-09-12 18:37:09 +0200}, doi = {10.1007/978-3-540-27836-8_30} }