Autumn 2004
Nachum Dershowitz

Time: Wed. 16-19
Location: Kaplun 324


  1. 4 Nov:  I have upgraded my Scheme and Lisp interpreters to handle non-linear rules (with multiple occurrences of variables) properly.


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
  • Information