Generalizing allowedness while retaining completeness of SLDNF-resolution

Abstract

We propose various generalizations of the usual definition of allowedness used to prove the completeness of SLDNF-resolution. In particular, we define the property of recursively covered programs and goals. We show that, for programs and goals that are call-consistent, even and recursively covered, SLDNF-resolution computes a complete set of ground answers. We then propose further generalized conditions that ensure that SLDNF-resolution is flounder-free. Moreover, this allows us to define a class of programs that subsumes all three major syntactic classes of programs and goals for which SLDNF-resolution is known to be complete; i.e., programs and goals that are either definite, or hierarchical and weakly allowed, or call-consistent, strict and allowed. We conjecture that our generalizations preserve the completeness of SLDNF-resolution. We also investigate the possibility of weakening the other syntactic conditions, i.e., even and call-consistent, while retaining completeness.