Rights accessRestricted access - publisher's policy
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.
CitationFernández, M.; Rubio, A. Nominal completion for rewrite systems with binders. A: International Colloquium on Automata, Languages and Programming. "Automata, Languages, and Programming: 39th International Colloquium, ICALP 2012: Warwick, UK, July 9-13, 2012: proceedings, part II". Warwick: Springer, 2012, p. 201-213.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: firstname.lastname@example.org