Tabled evaluation with delaying for general logic programs

摘要: SLD resolution with negation as finite failure (SLDNF) reflects the procedural interpretation of predicate calculus a programming language and forms computational basis for Prolog systems. Despite its advantages stack-based memory management, SLDNF is often not appropriate query evaluation three reasons: (a) it may terminate due to infinite positive recursion; (b) be recursion through negation; (c) repeatedly evaluate same literal in rule body, leading unacceptable performance.We address all problems goal-oriented general logic programs by presenting tabled delaying, called SLG resolution. It has distinctive features:(i) partial deduction procedure, consisting seven fundamental transformations. A transformed step into set answers. The use transformations separates logical issues from ones. allows an arbitrary computation selecting body control strategy apply.(ii) sound search space complete respect well-founded model non-floundering queries, preserves three-valued stable models. To under differenc models, can enhanced further processing answers subgoals relevant query.(iii) avoids both negative loops always terminates bounded-term-size property. polynomial time data complexity function-free programs. Through delaying mechanism handling ground literals involved loops, repetition any derivation steps.Restricted are identified definite, locally stratified, modularly stratified programs, shedding light on role each transformation plays.