Summary: POLO --- A System for Termination Proofs using
Polynomial Orderings \Lambda
FB Informatik, Technische Hochschule Darmstadt,
Alexanderstr. 10, 64283 Darmstadt, Germany
POLO is a system for both semiautomatic and fully automated ter
mination proofs of term rewriting systems using polynomial orderings.
In this paper we describe the system's user interface and illustrate its
performance with some examples.
In [Gie95a] and [Gie95b] we presented a method for automated termination
proofs of term rewriting systems using polynomial orderings. This technique
has been implemented in the POLO system. It runs under Common Lisp and
is available by anonymous ftp from kirmes.inferenzsysteme.informatik.
thdarmstadt.de under pub/termination.
To run the system please start your Lisp, compile the file polo.lisp, load
the compiled version and change the package to polo. More precisely, you have
to enter the following commands. User inputs are printed in bold face.