LIPIcs.FSCD.2016.11.pdf
- Filesize: 0.69 MB
- 17 pages
Document
Nominal Narrowing
Authors
-
Part of:
Volume:
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-06-17
Cite As Get 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)
https://doi.org/10.4230/LIPIcs.FSCD.2016.11
Abstract
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.
Subject Classification
Keywords
- Nominal Rewriting
- Nominal Unification
- Matching
- Narrowing
- Equational Theories
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads