Proving termination of Prolog programs

Abstract

The paper presented two kinds of proof rules to prove B-termination, the kind of termination obtained by the combination of backtracking and recursion as displayed by Prolog. The first kind of rule takes into account the context of the whole program and is based on a tree oriented operational semantics. The second kind is more compositional, dealing with separate procedures in a context independent way. It is based on a stream oriented semantics. We would like to stress that such proof rules may be successfully used for defining other search strategies than the actual one used by prolog. An interesting question is to define in this way a probabilistic backtracking search strategy.