SLT-Resolution for the Well-Founded Semantics

dc.creatorShen, Yi-Dong
dc.creatorYuan, Li-Yan
dc.creatorYou, Jia-Huai
dc.date2000-02-27
dc.date2001-03-02
dc.date.accessioned2026-07-07T03:15:55Z
dc.date.available2026-07-07T03:15:55Z
dc.descriptionGlobal 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 for query evaluation 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 principal disadvantage of a non-linear approach is that it cannot be implemented using a simple, efficient stack-based memory structure nor can it be easily extended to handle some strictly sequential operators such as cuts in Prolog. In this paper, we present a linear tabling method, called SLT-resolution, for top-down evaluation of the well-founded semantics. SLT-resolution is a substantial extension of SLDNF-resolution with tabling. Its main features include: (1) It resolves infinite loops and redundant computations while preserving the linearity. (2) It is terminating, and sound and complete w.r.t. the well-founded semantics for programs with the bounded-term-size property with non-floundering queries. Its time complexity is comparable with SLG-resolution and polynomial for function-free logic programs. (3) Because of its linearity for query evaluation, SLT-resolution bridges the gap between the well-founded semantics and standard Prolog implementation techniques. It can be implemented by an extension to any existing Prolog abstract machines such as WAM or ATOAM.
dc.descriptionSlight modification
dc.identifierhttps://arxiv.org/abs/cs/0002016
dc.identifierhttp://arxiv.org/abs/cs/0002016
dc.identifierJournal of Automated Reasoning 28(1):53-97, 2002
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/30162
dc.subjectArtificial Intelligence
dc.subjectProgramming Languages
dc.subjectD.3.1; F.4.1; I.2.3
dc.titleSLT-Resolution for the Well-Founded Semantics
dc.typetext

Files

Collections