Nominal Narrowing

Authors Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho

Thumbnail PDF


  • Filesize: 0.69 MB
  • 17 pages

Document Identifiers

Author Details

Mauricio Ayala-Rincón
Maribel Fernández
Daniele Nantes-Sobrinho

Cite AsGet BibTex

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Nominal unification is a generalisation of first-order unification that takes alpha-equivalence into account. In this paper, we study nominal unification in the context of equational theories. We introduce nominal narrowing and design a general nominal E-unification procedure, which is sound and complete for a wide class of equational theories. We give examples of application.
  • Nominal Rewriting
  • Nominal Unification
  • Matching
  • Narrowing
  • Equational Theories


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads