Ben-Gurion University

April 1997

N. Dershowitz

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.)
**