Tabulated resolution for the well-founded semantics
1998 (English)In: The journal of logic programming, ISSN 0743-1066, E-ISSN 1873-5789, Vol. 34, no 2, 67-109 p.Article in journal (Refereed) Published
Based on the search forest for positive programs as defined by Bol and Degerstedt, we define a tabulation-based framework that is sound and complete (when floundering does not occur) w.r.t. the well-founded semantics. In contrast to SLS-resolution as proposed by Przymusinski and by Ross, a positivistic computation rule is not required. Moreover, unlike SLG-resolution due to Chen and Warren, our proposal relies on tabulation for both positive and negative recursion without losing the clear separation of the search space from search strategies. In particular, the newly proposed search forest is finite for nonfloundering functor-free programs.
Place, publisher, year, edition, pages
1998. Vol. 34, no 2, 67-109 p.
IdentifiersURN: urn:nbn:se:sh:diva-12703DOI: 10.1016/S0743-1066(97)00073-3ISI: 000071535900001OAI: oai:DiVA.org:sh-12703DiVA: diva2:452122