Document Open Access Logo

Nominal Anti-Unification

Authors Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

Thumbnail PDF


  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Author Details

Alexander Baumgartner
Temur Kutsia
Jordi Levy
Mateu Villaret

Cite AsGet BibTex

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 57-73, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
  • Nominal Anti-Unification
  • Term-in-context
  • Equivariance


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail