Redundancy Elimination and Loop Checks for Logic Programs

AbstractA simple analysis of the arguments developed by Bol et al. (Theoret. Comput. Sci.86, 35-79 (1991)) shows that an actual reason for the nonexistence of a complete sound simple check for all function-free programs is the presence in the resolvents of potentially unlimited sequences of atoms chained by common variables. This hints that a limitation of the number of variables generating this kind of chain could guarantee the applicability of complete simple loop checks. This line is followed in the paper, and quite general classes of logic programs are characterized, without any direct imposition on the structures of the rules. This objective is accomplished by exploiting a variant of SLD-resolution, which is able to perform a systematic elimination of redundant atoms from resolvents. As a notable result, it turns out that the equality loop check is complete for our class of logic programs. This seems to suggest that the necessity of using subsumption loop checks instead of equality checks is essentially due to the presence of redundant atoms in resolvents