Closed nominal rewriting and efficiently computable nominal algebra equality

Maribel Fernández
(King's College London)
Murdoch J. Gabbay
(Heriot-Watt University)

We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of the lambda-calculus and first-order logic.

In Karl Crary and Marino Miculan: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010), Edinburgh, UK, 14th July 2010, Electronic Proceedings in Theoretical Computer Science 34, pp. 37–51.
Published: 11th September 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.34.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org