2010/09/14 by Maribel Fernández, Murdoch J. Gabbay
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.34.5
published as EPTCS 34, 2010, pp. 37-51 · In Proceedings LFMTP 2010, arXiv:1009.2189
arxiv created 2010/09/14 · arxiv updated 2010/09/16
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.