## Advanced Topics in Term RewritingTerm 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 volume 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 *comprehensive coverage of conditional term-rewriting systems *state-of-the-art survey of modularity in term rewriting *presentation of unified framework for term and graph rewriting *up-to-date discussion of transformational methods for proving termination of logic programs, including the TALP system This unique book offers a comprehensive and unified view of the subject that is suitable for all computer scientists, program designers, and software engineers who study and use term rewriting techniques. Practitioners, researchers and professionals will find the book an essential and authoritative resource and guide for the latest developments and results in the field. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

II | 1 |

III | 7 |

IV | 9 |

V | 11 |

VI | 16 |

VII | 21 |

VIII | 23 |

IX | 31 |

XLIX | 215 |

L | 225 |

LI | 229 |

LII | 230 |

LIII | 232 |

LIV | 233 |

LV | 235 |

LVI | 237 |

X | 37 |

XI | 40 |

XII | 45 |

XIII | 47 |

XIV | 51 |

XV | 57 |

XVI | 59 |

XVII | 60 |

XVIII | 64 |

XIX | 71 |

XX | 75 |

XXI | 77 |

XXII | 88 |

XXIII | 93 |

XXIV | 98 |

XXVI | 104 |

XXVII | 109 |

XXVIII | 115 |

XXIX | 116 |

XXX | 120 |

XXXI | 124 |

XXXII | 127 |

XXXIII | 129 |

XXXIV | 135 |

XXXV | 152 |

XXXVI | 155 |

XXXVII | 166 |

XXXVIII | 178 |

XXXIX | 179 |

XL | 180 |

XLI | 186 |

XLII | 187 |

XLIII | 190 |

XLIV | 195 |

XLV | 204 |

XLVII | 206 |

XLVIII | 211 |

LVIII | 243 |

LIX | 248 |

LXI | 252 |

LXII | 257 |

LXIII | 259 |

LXIV | 263 |

LXV | 265 |

LXVI | 275 |

LXVII | 281 |

LXVIII | 282 |

LXIX | 285 |

LXX | 291 |

LXXI | 294 |

LXXIII | 309 |

LXXIV | 313 |

LXXV | 317 |

LXXVI | 325 |

LXXVII | 327 |

LXXVIII | 333 |

LXXIX | 337 |

LXXX | 338 |

LXXXI | 340 |

LXXXII | 343 |

LXXXIII | 351 |

LXXXIV | 354 |

LXXXV | 355 |

LXXXVI | 362 |

LXXXVII | 364 |

LXXXVIII | 369 |

LXXXIX | 371 |

XC | 376 |

XCI | 379 |

XCII | 381 |

385 | |

407 | |

### Other editions - View all

### Common terms and phrases

According to Lemma C T(T Cf-terminating Computer conditional rewrite confluence constructor-sharing contains contradiction conversion Corollary CTRS CTRSs cycle defined Definition denotes dependency graph dependency pair derivation starting deterministic 3-CTRS disjoint TRSs disjoint unions example extra variables F-algebra follows function symbols graph rewriting ground term Hence hierarchical combination implies inductive hypothesis infinite innermost innermost terminating irreflexive joinable left-linear locally confluent logic program marked modular for disjoint modulo multiset Newman's lemma nonduplicating nonoverlapping normal form obtain orthogonal partial ordering path ordering PCP instance Proof Let proper extension Proposition proving termination quasi-ordering quasi-reduction ordering quicksort rank(t redex reduction ordering reduction sequence reduction step rewrite relation rewrite rule rewrite sequence rewrite step root(t satisfies Section signature simplification ordering simply terminating substitution Suppose term rewriting systems Theorem transformation TRSs u(Rv U(TZ Un(TZ unique normal Var(l w-terminating well-founded well-moded logic program