Contributions to a Theory of Existential Termination for Definite Logic Programs.
Giorgio Levi, Francesca Scozzari · 1995
We suggest a new formalization of the existential termination problem of logic programs under the PROLOG leftmost selection rule and depth-first computation rule. First of all, we give a characterization of the problem in terms of occurrence sets, by proving that a hprogram; goali existentially terminates if and only if there exists a finite correct occurrence set. Then we show that in order to study existential termination, we do not need to specify the occurrences of the atoms, since existential termination turns out to be decidable, when instances of atoms are used more than once (up to renaming). We then reduce the verification of existential termination to the search of a suitable semi occurrence set for the pair hprogram; goali, by providing an algorithm for proving that the proposed semi occurrence set is a correct occurrence set. Finally we propose a simple method (based on abstract interpretation techniques) for generating such semi occurrence sets. Keywords: existe...