Catalogo Articoli (Spogli Riviste)

OPAC HELP

Titolo:
Termination of simply-moded well-typed logic programs under a tabled execution mechanism
Autore:
Verbaeten, S; De Schreye, D;
Indirizzi:
Katholieke Univ Leuven, Dept Comp Sci, B-3001 Heverlee, Belgium KatholiekeUniv Leuven Heverlee Belgium B-3001 B-3001 Heverlee, Belgium
Titolo Testata:
APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING
fascicolo: 1-2, volume: 12, anno: 2001,
pagine: 157 - 196
SICI:
0938-1279(200106)12:1-2<157:TOSWLP>2.0.ZU;2-B
Fonte:
ISI
Lingua:
ENG
Soggetto:
PROVING TERMINATION; PROLOG PROGRAMS; TABULATION; RESOLUTION;
Keywords:
logic programming; tabling; termination;
Tipo documento:
Article
Natura:
Periodico
Settore Disciplinare:
Engineering, Computing & Technology
Citazioni:
32
Recensione:
Indirizzi per estratti:
Indirizzo: Verbaeten, S Katholieke Univ Leuven, Dept Comp Sci, Celestijnenlaan 200A, B-3001 Heverlee, Belgium Katholieke Univ Leuven Celestijnenlaan 200A Heverlee Belgium B-3001
Citazione:
S. Verbaeten e D. De Schreye, "Termination of simply-moded well-typed logic programs under a tabled execution mechanism", APPL ALG EN, 12(1-2), 2001, pp. 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 programsterminates more often than execution based on SLD-resolution. So, if a program can be proven to terminate under SLD-resolution, then the program willtrivially also terminate under SLG-resolution, the resolution principle oftabling. 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 introducesufficient conditions for quasi-termination and LG-termination which are stated fully at the clause level and are easy to automatize. To this end, weuse 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.

ASDD Area Sistemi Dipartimentali e Documentali, Università di Bologna, Catalogo delle riviste ed altri periodici
Documento generato il 01/04/20 alle ore 23:51:17