Using The System

In the main system page you should enter a prolog file name to be analyzed. You can optionally change the following parameters :

Symbolic norm :
- Term size - which counts the number of edges in the term-tree.
- List size - which measures the length of a list.
- Define other symbolic norm.
Computing bottom up size dependencies :
- Relations on pairs of argument positions : size dependencies are of the form :
```
X=Y,X<Y,X=<Y
```
  for pairs of argument positions.
- Polyhedra : size dependencies are given in a form of polyhedra : general linear dependencies between 2 or more argument positions.
Selecting either method you can get different results from the analysis.
Number of steps before widening : The polyhedra domain requires using widening. The widening is performed after computing N facts (2,3, or 4) according to the selected value. Using a larger value is more accurate, but also slower.
Computing binary unfoldings :
- Goal dependent : the closure of binary unfoldings is computed after the initial goal is given and only for the relevant calls.
- Goal independent : the closure of binary unfoldings is computed in the first stage. The result is that the goal independent stage is longer and the goal dependent stage is very fast. It is better to use this option if you want to check several initial goals for one program.

Pattern is the pattern of the term the norm should be defined for. It should be of the form f(X1,X2,...,Xn) where f is a function symbol and X1,X2,...,Xn are distinct variables.
Size is the way the norm should be computed. This expression should be of the form : "T1 + T2 + ..." where each Ti is either a natural number, or a term of the form size(X) and X is one of the variables in the given pattern.

For example the list-length norm can be defined as follows :

[defsize([X|Xs],1+size(Xs)),
 defsize([],0),
 defsize(X,0)].

The results of analyzing the query are :

An answer if the query terminates or possibly no.
A description (in the abstract domains of instantiation and size dependencies) of all possible calls and the matching binary clauses.
A graphic representation of the recursive binary clauses with the matching calls. (If requested by the user).
Some of the clauses show the decrease in an instantiated argument position in a red arrow.
If all the binary clauses contain an argument position which is instantiated and its size strictly decreases, then the query terminates. Otherwise the clauses that do not contain this red arrow are the cause for a possible non-termination, or for the inability of the system to prove termination.