Can you recommend a good reference for reading about lexicographic/recursive path orderings?

I'm currently reading about lpo's in Chapter 2 of the Handbook of Automated Reasoning, 'Resolution Theorem Proving' by Bachmair and Ganzinger, but the presentation is really terse. I would ideally like a more tutorial-like introduction w/ examples.


Some information at the right level of abstraction can be found in:

If you are near a library or bookshop, this book has even more details:

  • $\begingroup$ Thanks for the references. I've read the section on orders from 'Term Rewriting and All That' and it was very good and quite easy to follow. $\endgroup$ Apr 13 '11 at 15:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.