The finiteness of logic programming derivations

International audienceThe question of the termination of logic programming computations is studied from a semantical point of view. To every program are associated two first-order formulas. Their valid consequences are respectively the finiteness and the infiniteness SLDNF sets of the logic programs considered. The non-existence of a recursive safe computation rule leading into an infinite SLDNF computation is proved