A weak allowedness condition that ensures completeness of SLDNF-resolution

Abstract

The lillowedness condition usually imposed on classes of programs for which general completeness results for SLDNF-resolution have been proved is a very restrictive one and prohibits many important programming constructs. We weaken allowedness by defining a condition that accounts for bindings that will occur when unification takes place. We prove that Kunen's completeness theorems for SLDNF-resolution still hold when allowedness is replaced by this significantly weaker condition. The condition that accounts for the variable bindings may also prove useful to the formal understanding of data.-flow analysis techniques.