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.


1 Answer 1


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$ Commented Apr 13, 2011 at 15:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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