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