Advanced Topics in Term Rewriting

  • Enno Ohlebusch

Table of contents

  1. Front Matter
    Pages i-xv
  2. Enno Ohlebusch
    Pages 1-5
  3. Enno Ohlebusch
    Pages 7-35
  4. Enno Ohlebusch
    Pages 37-43
  5. Enno Ohlebusch
    Pages 45-56
  6. Enno Ohlebusch
    Pages 57-126
  7. Enno Ohlebusch
    Pages 127-178
  8. Enno Ohlebusch
    Pages 179-242
  9. Enno Ohlebusch
    Pages 243-323
  10. Enno Ohlebusch
    Pages 325-349
  11. Enno Ohlebusch
    Pages 351-377
  12. Back Matter
    Pages 379-414

About this book


Term rewriting techniques are applicable in various fields of computer sci­ ence: in software engineering (e.g., equationally specified abstract data types), in programming languages (e.g., functional-logic programming), in computer algebra (e.g., symbolic computations, Grabner bases), in pro­ gram verification (e.g., automatically proving termination of programs), in automated theorem proving (e.g., equational unification), and in algebra (e.g., Boolean algebra, group theory). In other words, term rewriting has applications in practical computer science, theoretical computer science, and mathematics. Roughly speaking, term rewriting techniques can suc­ cessfully be applied in areas that demand efficient methods for reasoning with equations. One of the major problems one encounters in the theory of term rewriting is the characterization of classes of rewrite systems that have a desirable property like confluence or termination. If a term rewriting system is conflu­ ent, then the normal form of a given term is unique. A terminating rewrite system does not permit infinite computations, that is, every computation starting from a term must end in a normal form. Therefore, 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 book provides a comprehensive study of termination and confluence as well as related properties.


Automat Boolean algebra TAL automated theorem proving computer formal method logic programming programming language theorem proving verification

Authors and affiliations

  • Enno Ohlebusch
    • 1
  1. 1.Research Group in Practical Computer Science, Faculty of TechnologyUniversity of BielefeldBielefeldGermany

Bibliographic information

Industry Sectors
IT & Software
Energy, Utilities & Environment