Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logic programming or term rewriting systems. Previous work on nominal rewriting and logic programming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic’s equivariance property, these applications require a stronger form of unification, which we call equivariant unification. Unfortunately, equivariant unification and matching are NP-hard decision problems. This paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as NP decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.


Logic Program Logic Programming Nominal Term Ground Term Permutation Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cheney, J., Urban, C.: Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 269–283. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Cheney, J.: The complexity of equivariant unification. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 332–344. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Cheney, J.R.: Nominal Logic Programming. PhD thesis, Cornell University, Ithaca, NY (August 2004)Google Scholar
  4. 4.
    Fernández, M., Gabbay, M., Mackie, I.: Nominal rewriting systems. In: Proceedings of the 6th Conference on Principles and Practice of Declarative Programming (PPDP 2004) (to appear)Google Scholar
  5. 5.
    Frühwirth, T.: Theory and practice of constraint handling rules. Journal of Logic Programming 37(1-3), 95–138 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)zbMATHCrossRefGoogle Scholar
  7. 7.
    Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 183, 165–193 (2003)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programmming with binders made simple. In: Proc. 8th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2003), Uppsala, Sweden, pp. 263–274. ACM Press, New York (2003)CrossRefGoogle Scholar
  9. 9.
    Snyder, W.: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic, vol. 11. Birkhäuser, Basel (1991)zbMATHGoogle Scholar
  10. 10.
    Urban, C., Cheney, J.: Avoiding equivariance in alpha-Prolog (2004)Google Scholar
  11. 11.
    Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323(1-3), 473–497 (2004)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • James Cheney
    • 1
  1. 1.University of Edinburgh 

Personalised recommendations