Termination Test for Logic Programs

This page illustrates a termination analysis for logic programs based on the semantic foundation described in the paper "A Semantic Basis for Termination Analysis of Logic Programs and its Realization using Symbolic Norm Constraints", by Michael Codish and Cohavit Taboch. ( abstract, postscript )

The contribution of this paper is a simple semantics for logic programs based on binary unfoldings which makes termination observable.

The semantics associates a program with its binary unfoldings - a possibly infinite set of binary clauses. Termination of a program P and goal G is indicated by the absence of an infinite chain in the binary unfoldings of P starting with G.

An abstract interpretation using the above described semantic foundation over a domain of relations on pairs of argument positions results in a termination analysis very similar to that described in N.Lindenstrauss and Y. Sagiv, Checking Termination of Queries to Logic Programs also implemented in TermiLog .

An abstract domain using polyhedra can also be used with our semantics. We thank Andy King and Florence Benoy for helping us with the implementation of this domain.

To experiment with our system you may have up to 1 minute of our CPU time. To get a feeling for how much analysis that will give you, have a look at the Examples.

For more information : taboch@cs.bgu.ac.il