Heterogeneous SLD resolution

AbstractDue to a significant oversight in the definition of computation rules, the current theory of SLD resolution is not general enough to model the behavior of some PROLOG implementations with advanced control facilities. In this paper, Heterogeneous SLD resolution is defined. It is an extension of SLD resolution which increases the “don't care” nondeterminism of computation rules and can decrease the size of the search space. Soundness and completeness, for success and finite failure, are proved using similar results from SLD resolution. Though Heterogeneous SLD resolution was originally devised to model current systems, it can be exploited more fully than it is now. As an example, an interesting new computation rule is described. It can be seen as a simple form of intelligent backtracking with few overheads