Constructing first-order loops of normal logic programs

It is possible that a logic program has no finite complete sets of loops. For instance, the Hamiltonian circuit problem encoded by Nielemä is such a logic program. This means that the complete set of loops of a logic program is possibly infinite. In order to represent a possible infinite complete set of loops by a finite set of loops, we propose a constructive approach: (i) we introduce the notion of base loops which can be obtained from predicate positive dependency graphs of logic programs and show that every logic program has a finite complete set of base loops; (ii) we show that every loop of a logic program can be constructed from its base loops using substitution and union.