Abstract
We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. Completion of rewriting systems with binders is a notably difficult problem; the completion procedure presented in this paper is the first to deal with binders in rewrite rules. © 2012 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Fernández, M., & Rubio, A. (2012). Nominal completion for rewrite systems with binders. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7392 LNCS, pp. 201–213). Springer Verlag. https://doi.org/10.1007/978-3-642-31585-5_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
