AProVE Help: Logic Programs

AProVE supports programs which are compatible to the ISO standard of the Prolog language as input language for logic programs. Termination analysis will be performed by a transformational approach. The result of the transformation is (maybe after several transformation steps) a so-called dependency pair problem whose finiteness implies termination of the original logic program. Complexity analysis is performed by a transformation to a number of dependency tuple problems from which an upper bound on the asymptotic runtime (measured as the number of unification attempts) can be inferred. Determinacy analysis is performed on a graphical representation of the control flow of the logic program.

• Fact (i.e. p(X).)
• Rule (i.e. p(X) :- q(X), r(X).)
• Comment (either between /* and */ or as a line comment after %)

At the moment, AProVE considers unification with occurs check.

In addition to the Prolog syntax listed above, AProVE recognizes three kinds of special commentary lines:

• Termination Query Mode Lines of the form

  %query: p(g,g,a).

• Complexity Query Mode Lines of the form

  %complexity: p(g,g,a).

• Determinacy Query Mode Lines of the form

  %determinacy: p(g,g,a).

The first such line supplies the AProVE system with additional information about the class of queries to analyze and the goal of the analysis (termination, runtime complexity, or determinacy). The predicate and the moding information define the set of queries by specifying which of the predicate's arguments are allowed to contain free variables in the initial query and which are not. The former ones are those arguments that are marked with a "g" (standing for "ground"), the latter ones are those marked with an "a" (standing for "any").

More intuitively described, the ground arguments are being used as input arguments to the predicate, while the others are used as output. For those who prefer this notation, the AProVE system accepts "i" and "o" instead of "g" and "a" as well. Another notation which can be used is "b" for "bound" and "f" for "free".

Normal Prolog style queries will be ignored as they do not contain the goal of the analysis.

For example

%query: append(g,g,a).

append([], Xs, Xs).
append([H|T], Xs, [H|Ys]) :- append(T, Xs, Ys).