Term Rewriting and All That

Baader, F., & Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.

Type

Book

Intellectual base

Review or monograph

Year

1998

DOI

10.1017/cbo9781139172752

ISBN

9780521455206

DOI registrant

Cambridge University Press

Link

https://doi.org/10.1017/CBO9781139172752

Cited from

computer_science

Cited by

7 citations across 7 artifacts.

Each citation links to the sentence it supports in the citing article.

Primes

• Equivalence-Preserving Rewriting
  • Theorem proving: normal-form rewriting in term-rewriting systems, rewriting a proof for shorter or more standard form, tactic-based proof restructuring under preserved logical content.

    This sourceStandard reference on term-rewriting systems, normal forms, confluence, and termination — the formal apparatus for rewriting under a preserved equivalence.

    Supported in partVerified against the publisher's abstract

    The book's own abstract establishes it as a general introduction to term rewriting (termination, confluence, completion); it says nothing about theorem proving, proof shortening, or tactic-based restructuring.

    “This textbook offers a unified and self-contained introduction to the field of term rewriting. It covers all the basic material (abstract reduction systems, termination, confluence, completion, and combination problems)”

    Read by an automated reader; not a human review. How support was checked

Domain-specific

• Overlap (term rewriting)
  • The entry records a descriptive analytical identity; practical use requires the governing domain's evidence, standards, and safety obligations.
• Reflexive closure
  • Taking its reflexive closure permits a state to reach itself in zero steps while still excluding all two-step consequences; those require transitive closure.
• Term algebra
  • The entry records a descriptive analytical identity; practical use requires the governing domain's evidence, standards, and safety obligations.

Mechanisms

• Normal-Form Reduction
  • If the system is non-terminating, reduction can loop and never yield a form; if it is non-confluent, two genuinely equivalent inputs can reduce to different normal forms, reporting false inequivalence.

    This sourceExplains that termination prevents endless reduction and confluence secures unique normal forms, enabling valid normal-form comparison for equivalent terms.

• Rewrite or Transition Rule Engine
  • A rule set that is not terminating sends the engine into an infinite loop — the "nice" new rewrite rule that quietly creates a cycle is the classic culprit — and a rule set that is not confluent yields order-dependent answers

    This sourceExplains that termination prevents endless rewriting and confluence ensures a unique normal form independent of rule-application order.

• Rewrite System with Confluence Tests
  • Termination is undecidable in general, so a termination proof rests on finding a suitable ordering and may not exist for a system that nonetheless (subtly) halts; completion can itself fail to terminate, spawning rules without end.

    This sourceShows that termination is undecidable in general, is commonly proved with a suitable reduction ordering, and that completion may fail to terminate while generating new rules.

Verification

Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.

Does it back the claim? Read against the text for 1 of 7 citations: 1 supported in part. Each verdict is shown under its citation below, with what in the work backs the sentence.

Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.

See how references were verified.

Registry ID ref:d5744337b5eb · see in the full table