Title: Termination of simply-moded well-typed logic programs under a tabled execution mechanism
Authors: Verbaeten, Sofie ×
De Schreye, Danny #
Issue Date: Jun-2001
Publisher: Springer-verlag
Series Title: Applicable algebra in engineering communication and computing vol:12 issue:1-2 pages:157-196
Abstract: Tabled logic programming is receiving increasing attention in the Logic Programming community. It avoids many of the shortcomings of SLD(NF) execution and provides a more flexible and often extremely efficient execution mechanism for logic programs. In particular, tabled execution of logic programs terminates more often than execution based on SLD-resolution. So, if a program can be proven to terminate under SLD-resolution, then the program will trivially also terminate under SLG-resolution, the resolution principle of tabling. But, since there are SLG-terminating programs which are not SLD-terminating, more effective proof techniques can be found. One of the few approaches studying termination of tabled logic programs was developed by Decorte et al. They present necessary and sufficient conditions for two notions of termination under LG-resolution, i.e. SLG-resolution with left-to-right selection rule: quasi-termination and (the stronger notion of) LG-termination. Starting from these necessary and sufficient conditions, we introduce sufficient conditions for quasi-termination and LG-termination which are stated fully at the clause level and are easy to automatize. To this end, we use mode and type information: we consider simply-moded, well-typed programs and queries. We point out how our termination conditions can be automatized, by extending the recently developed, constraint-based, automatic termination analysis for SLD-resolution of Decorte and De Schreye. Finally, we present a result on substitution-closedness of quasi-termination and LG-termination for the class of simply-moded, well-typed programs and queries.
ISSN: 0938-1279
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
32916.pdf Published 322KbAdobe PDFView/Open
32916_app.pdf Published 211KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science