REWRITE SYSTEMS
Spring 2002
N. Dershowitz

Instead of 17 June we will meet 24 June

DESCRIPTION

Equational reasoning is important in artificial intelligence, automated deduction, symbolic algebra, program verification, and high-level programming languages. Reasoning with equations includes deriving consequences of given equations and finding values for variables that satisfy a given equation.  Rewrite rules, that is directed equations, are used to replace equals by equals, but only in a direction that results in a simpler expression. The theory of rewriting centers around the notion of "normal forms", expressions that cannot be rewritten any further. When equal terms always have the same normal form, the system is said to be "canonical" or "complete".
 

COURSE OUTLINE

  • Introduction: equational reasoning, rewrite systems, term orderings
  • Rewriting: normal forms, existence, uniqueness, deciding equality
  • Termination: undecidability, interpretations, Kruskal's Tree Theorem, recursive path orderings
  • Confluence: Church-Rosser property, Newman's Lemma, local confluence, critical pairs
  • Orthogonality: strong confluence, Parallel Moves Lemma, outermost computations
  • Completion: proof orderings, Knuth-Bendix procedure, ordered completion
  • Theorem proving: equational reasoning, induction, first-order
  • COURSE NOTES

    OPEN PROBLEMS

    SYSTEMS

    PAPERS

    OTHER LINKS

    Old Course