Multi-SLD resolution

Multi-SLD resolution is a variant of SLD resolution based on a simple idea.: Let the allowed constraints be closed under disjunction, and provide a mechanism for collecting solutions to a goal and turning the solutions into a disjunctive constraint. This idea leads to an operational model of logic programming, called data, or- parallelism, in which multiple constraint environments partially replace backtracking as the operational embodiment of disjunction. The model has a natural implementation on data-parallel computers since each disjunct of a disjunctive constraint can be handled by a single (virtual) processor. In this paper, weformalize the notions of multi-SLD resolution, multi-derivation, multi-SLD tree, and environment tree;prove the soundness and completeness of multi-SLD resolution; anddescribe and justify several useful optimization techniques based on the form of constraints in a multi-derivation: the distinction between engine and multi variables, templates, and sharing of bindings in the environment tree.Together these results provide the foundations for a new operational semantics of disjunction in logic programming.