Rewriting techniques and applications

More about the book

This work covers a range of topics in symbolic systems biology and rewriting logic, including confluence as a cut elimination property and associative-commutative rewriting on large terms. It explores a rule-based approach for generating kinetic chemical mechanisms and discusses efficient reductions through director strings. The Maude 2.0 system is highlighted alongside diagrams for meaning preservation and expression reduction systems with patterns. The text addresses higher-order rewriting, new decidability results for fragments of first-order logic, and applications to cryptographic protocols. An E-unification algorithm is presented for analyzing protocols using modular exponentiation, and the complexities of higher-order matching in linear lambda calculus are examined. Various topics such as XML schema, tree logic, and sheaves automata are discussed, along with size-change termination for term rewriting and monotonic AC-compatible semantic path orderings. The work also includes insights on liveness in rewriting, validation techniques for the JavaCard platform, and termination of simply typed term rewriting. Additional subjects include environments for term rewriting engines, a logical algorithm for ML type inference, and stable computational semantics of conflict-free rewrite systems. The text concludes with discussions on recognizing Boolean closed A-tree languages and testing extended regular language membership incremen