Details

Autor(en) / Beteiligte

• Shen, Yi-Dong
• Yuan, Li-Yan
• You, Jia-Huai
• Zhou, Neng-Fa
• Pfeifer, Gerald
• Leone, Nicola
• Gelfond, Michael

Titel

Linear Tabulated Resolution for the Well-Founded Semantics

Ist Teil von

• Lecture notes in computer science, 1999, p.192-205

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

1999

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Global SLS-resolution and SLG-resolution are two representative mechanisms for top-down evaluation of the well-founded semantics of general logic programs. Global SLS-resolution is linear but suffers from infinite loops and redundant computations. In contrast, SLG-resolution resolves infinite loops and redundant computations by means of tabling, but it is not linear. The distinctive advantage of a linear approach is that it can be implemented using a simple, efficient stack-based memory structure like that in Prolog. In this paper we present a linear tabulated resolution for the well-founded semantics, which resolves the problems of infinite loops and redundant computations while preserving the linearity. For non-floundering queries, the proposed method is sound and complete for general logic programs with the bounded-term-size property.