|
Abstract : |
Based on the search forest for positive programs as defined by Bol and Degerstedt, we define a tabulated version of SLS-resolution that is sound and complete w.r.t. well founded semantics. In contrast to SLS-resolution as proposed by Przymusinski and by Ross, a positivistic computation rule is not required. This proposal is closely related to that of Chen and Warren, but it relies on tabulation for both positive and negative recursion. In this way, only one forest needs to be constructed, rather than a forest for each negative context. For function-free programs, the resulting search forest is finite., |
