S-SLD-resolution — An operational semantics for logic programs with external procedures

Abstract

This paper presents a new operational semantics for logic programs with external procedures, introduced in [BM88]. A new resolution procedure S-SLD-resolution is defined, in which each step of computation is characterized by a goal and a set of equational constraints, whose satisfiability cannot be decided with the information at hand. This approach improves the completeness of the resulting system, since further computation may result in the information needed to solve some earlier unsolved constraints. We also state a sufficient condition to distinguish a class of programs where no unsolved constraints will remain at the end of computation.