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.
Rewriting is a very powerful method for dealing with equations. It is a topic of much recent theoretical and applied research in Europe, Japan, and the U.S. 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".
The course will be self-contained. There are no prerequisites.
There will be two one-week homework assignments and no exam.
N. Dershowitz. Functional Programming, Concurrency, Simulation and Automated Reasoning, Lecture Notes in Computer Science 693, 199-228 (1993)
A gentle introduction to the theory and applications of rewriting with equations. It discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as rewriting-based (functional and logic) programming and (equational, first-order, and inductive) theorem proving. An extensive bibliography is included. (The on-line version is better than the published one.)
N. Dershowitz and J.-P. Jouannaud. Chap. 6 of Handbook of Theoretical Computer Science B: Formal Methods and Semantics, J. van Leeuwen, ed., North-Holland, Amsterdam (1990) 243-320
This is a survey of the theory of rewriting. (The on-line version is imprecise.)
J. W. Klop. Chap. 1 in Handbook of Logic in Computer Science, vol. 2, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, eds., Oxford University Press, Oxford (1992) 1-117.
This excellent survey stresses confluence properties, orthogonal systems, and completion. It includes exercises. (The on-line version does not have the valuable diagrams.)
Equational Inference, Canonical Proofs, and Proof Orderings
L. Bachmair and N. Dershowitz. J. of the ACM 41 (2) 236-276 (Feb. 1994)
This paper describes the application of proof orderings--a technique for reasoning about inference systems--to various rewrite-based theorem-proving methods, including ordered completion and a proof by consistency procedure for proving inductive theorems. (The on-line version is a pre-publication technical report.)