About The System

The system for automatic termination test for logic programs is implemented with SICStus prolog version 3.5.
The web interface was developed using the PiLLoW web package :

The analysis is performed in two main stages :

In the first stage the system analyses a given logic program and creates a set of binary unfoldings of the program over two abstract domains :

Instantiation dependencies, computed over the domain Prop.
Size dependencies, can be computed over two domains :
- Relations on pairs of argument positions.
- Polyhedra.

In the goal independent stage the analysis is done as follows :

Select a symbolic norm : list size or term size.
Abstract the given logic program by replacing each term with its symbolic norm.
Compute the s-semantics of the program over 2 domains :
- For instantiation dependencies perform groundness analysis on the abstract program.
- For size dependencies use the constraints solver (CLP(R) library of SICStus).
Compute the set of binary unfoldings of the program in a similar way.

In the second stage, given an initial abstract call, the termination test is done as follows :

Computing all the abstract calls that arise in the computation using the binary unfoldings.
For each call and binary clause : test that the size of an argument position which is instantiated enough is strictly decreasing in the computation.