Buch, Englisch, 414 Seiten, Format (B × H): 160 mm x 241 mm, Gewicht: 1730 g
ISBN: 978-0-387-95250-5
Verlag: Springer
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.
Zielgruppe
Professional/practitioner
Autoren/Hrsg.
Weitere Infos & Material
1 Motivation.- 2 Abstract Reduction Systems.- 3 Term Rewriting Systems.- 4 Confluence.- 5 Termination.- 6 Relative Undecidability.- 7 Conditional Rewrite Systems.- 8 Modularity.- 9 Graph Rewriting.- 10 Proving Termination of Logic Programs.- A Kruskal’s Theorem.- A.l Partial Well-Orderings.- A.2 A Proof of Kruskal’s Theorem.- References.
