PROOFS OF TERMINATION
PURPOSE
The purpose of the course is to learn various methods of proving termination
of programs. Topics include:
-
Well-founded Orderings, Ordinals, Lexicographic and Bag Orderings
-
Higman's Lemma, Kruskal's Theorem, Simplification Orderings
-
Knuth-Bendix Orderings, Recursive Path Orderings
Message
If you are taking this course and haven't received
email from me, please
send a message to me at nachumd@cs.tau.ac.il.
Course Data
Instructor:
Nachum Dershowitz
Office: 214 Schreiber; Tue. 14-15
Phone: 03/640-9621
E-mail: nachumd@cs.tau.ac.il
Resources
Articles
- Nachum Dershowitz, 1982, Orderings for Term-Rewriting Systems, Theoret.
Comp. Sci. 17 (3) 279-301
- Nachum Dershowitz and Zohar Manna, 1979, Proving Termination With
Multiset Orderings, Comm. ACM 22 (8) 465-476.
- Shmuel M. Katz and Zohar Manna, 1975, A closer look at termination,
Acta Informatica 5 (4) 333-352.
- Laurie Kirby and Jeff Paris, 1982, Accessible independence results
for Peano arithmetic, Bulletin London Mathematical Society 14, 285-293
- Zohar Manna, Stephen Ness and Jean Vuillemin, 1973, Inductive
methods for proving properties of programs, Communications of the ACM 16
(8) 91-502.
- Zohar Manna and Richard Waldinger, 1978, Is sometime sometimes
better than always: Intermittent assertions in proving program correctness,
Communications of the ACM 21 (2) 159-172.
- Hans Zantema, 1994, Termination of term rewriting: interpretation
and type elimination, Journal of Symbolic Computation 17, 23-50