We suggest a new formalization of the existential termination problem of logic p rograms 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 program and a goal existentially terminate 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 a program and a goal, 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: existential termination, program analysis.