Termination Proofs of Rewriting Systems - Heuristics for Generating
Polynomial Orderings

Joachim Steinbach
Fachbereich Informatik, Universit"at Kaiserslautern, Postfach 3049,
D-6750 Kaiserslautern, GERMANY
E-mail: steinba@informatik.uni-kl.de

Abstract
Orderings on polynomial interpretations of operators represent a
powerful technique for proving the termination of rewriting systems.
One of the main problems of polynomial orderings concerns the choice
of the right interpretation for a given rewriting system. It is very
difficult to develop techniques for solving this problem. Here, we
present three new heuristic approaches: (i) guidelines for dealing
with special classes of rewriting systems, (ii) an algorithm for
choosing appropriate special polynomials as well as (iii) an extension
of the original polynomial ordering which supports the generation of
suitable interpretations. All these heuristics will be applied to
examples in order to illustrate their practical relevance.

Keywords
term rewriting systems, termination, simplification orderings,
polynomial orderings

anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1991/papers
file: Steinbach.SR-91-14.english.ps.Z