Rewriting techniques and applications

The book covers a range of advanced topics in rewriting systems and formal logic, structured into multiple sessions. It begins with discussions on path ordering constraints and strategic pattern matching, followed by explorations into natural deduction normalization and weakly orthogonal rewriting. The sessions include invited talks on hierarchical graph decompositions and the undecidability of ground term algebra theory. Key results are presented on the satisfiability of quantifier-free formulae and the decidability of existential one-step rewriting theory. Further sessions delve into syntactic AC-RPO, theory path orderings, and characterizations of recursive functions using Higman’s lemma. The content also addresses the word problem in equational theories, normalization via rewrite closures, and test sets for regular tree languages. An invited tutorial on higher-order rewriting is included, along with system descriptions of various declarative systems like Maude, TOY, and UniMoK. The latter part of the book examines decidability in left-linear growing term rewriting systems, context-sensitive rewrite systems, and the calculus of algebraic constructions. An invited talk connects rewriting with formal language theory, while additional topics cover rewrite systems associated with quadratic Pisot units and the implementation of tree synchronized languages.