🚀 go-pugleaf

Hi,
We had presented a paper titled "A framework of directionality
for proving the termination of logic programs" at the JICSLP '92
in Washington DC last week. Since some of our audience expressed
interest in the paper, we are making available the long version
of the paper, complete with examples and proofs.  The paper can be
obtained by anonymous ftp on the machine a.cs.uiuc.edu in the
directory /pub/reddy/termination.  The files are termination.dvi (for
a dvi version) or termination.ps (for a postscript version).

The essential idea is two-fold:

a. To describe a rich notion of directionality for logic programs
via a combination of MODES and REGULAR TREES. Modes can
be quite useful in reasoning about interesting semantic
properties of logic programs.

b. To use the above notion of modes in proving termination of logic
programs. We present some simple termination theorems and give examples
of powerful (yet simple) well-founded orderings that can be used to
prove termination of non-trivial programs in a simple manner.

We'd appreciate comments.

Francois Bronsard, T.K. Lakshman, and Uday S. Reddy