Time: Wed. 16-19
Location: Kaplun 324
Messages
- 4 Nov: I have upgraded my Scheme and
Lisp interpreters to handle non-linear
rules (with multiple occurrences of variables) properly.
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
Information