Enno Ohlebusch
Advanced Topics in Term Rewriting
Springer-Verlag, 414 pages, April 2002.
ISBN: 0-387-95250-0
table of contents


Term rewriting techniques are applicable to various fields of computer science, including software engineering, programming languages, computer algebra, program verification, automated theorem proving and Boolean algebra. These powerful techniques can be successfully applied in all areas that demand efficient methods for reasoning with equations. One of the major problems encountered is the characterization of classes of rewrite systems that have a desirable property, like confluence or termination. In a system that is both terminating and confluent, every computation leads to a result that is unique, regardless of the order in which the rewrite rules are applied. This new text/reference provides a comprehensive and unified presentation of termination and confluence, as well as related properties.

Topics and features:
• Unified presentation and notation for important advanced topics in term rewriting
• Coverage of the newest techniques for proving termination of rewrite systems
• Comprehensive coverage of conditional term rewriting systems
• State-of-the-art survey of modularity in term rewriting
• Presentation of a unified framework for term and graph rewriting
• Up-to-date discussion of transformational methods for proving termination of logic programs