Rewriting
This is an up-to-date survey of term rewriting theory and its applications written by two leading experts of the field. It is divided into ten sections: 1. Introduction, 2. Terminology, 3. Normal Forms and Validity, 4. Termination Properties, 5. Church-Rosser Properties, 6. Completion, 7. Relativized Rewriting, 8. Equational Theorem Proving, 9. Conditional Rewriting, and 10. Programming. Moreover, the paper contains an extensive Bibliography and an Index. In addition to the general basic material, several more specialized or advanced topics are discussed, and many more are mentioned together with helpful references. Of course, there are not very many proofs, but the underlying ideas are carefully explained, and many examples illustrate all the main notions and methods considered. Although a few excellent overviews of the area already exist, this well-written paper will certainly become one of the standard references.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
- Theory decision by decomposition
- Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
- Rewriting techniques and applications. 3rd international conference, RTA-89, Chapel Hill, NC, USA, April 3--5, 1989. Proceedings
- Dealing with explicit preferences and uncertainty in answer set programming
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Equational theorem proving modulo
- Set of support, demodulation, paramodulation: a historical perspective
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- SCL(EQ): SCL for first-order logic with equality
- Making theory reasoning simpler
- On interpolation in automated theorem proving
- Rewriting-based repairing strategies for XML repositories
- Automated verification of selected equivalences for security protocols
- Abstract canonical presentations
- Selecting the selection
- Timed term rewrite systems
- Strategic rewriting
- Rewrite-based decision procedures
- Interpolation systems for ground proofs in automated deduction: a survey
- Deciding knowledge in security protocols under some e-voting theories
- Modular termination and combinability for superposition modulo counter arithmetic
- scientific article; zbMATH DE number 4155899 (Why is no real title available?)
- scientific article; zbMATH DE number 4090779 (Why is no real title available?)
- scientific article; zbMATH DE number 177826 (Why is no real title available?)
- Tableaux and hypersequents for justification logics
- scientific article; zbMATH DE number 2043526 (Why is no real title available?)
- Efficient general AGH-unification
- Term Rewriting and All That
- Canonical ground Horn theories
- Narrowing based inductive proof search
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
- More problems in rewriting
- Problems in rewriting III
- New Undecidability Results for Properties of Term Rewrite Systems
- Efficient general unification for XOR with homomorphism
- Proving weak properties of rewriting
- SCL(EQ): SCL for first-order logic with equality
- Equational Theorem Proving for Clauses over Strings
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Strict coherence of conditional rewriting modulo axioms
- An Iabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility
- Computing ground congruence classes
- Congruence closure modulo groups
- Equational theorem proving for clauses over strings
- An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems
- Things to know when implementing KBO
- The disconnection tableau calculus
- Deciding expressive description logics in the framework of resolution
This page was built for publication: Rewriting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751361)
