A Weak Allowedness Condition that Ensures Completeness of SLDNF-Resolution.
Lawrence Cavedon, Hendrik Decker · UPCommons institutional repository (Universitat Politècnica de Catalunya) · 1990
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.