Catalogo Articoli (Spogli Riviste)

OPAC HELP

Titolo:
A general framework for automatic termination analysis of logic programs
Autore:
Dershowitz, N; Lindenstrauss, N; Sagiv, Y; Serebrenik, A;
Indirizzi:
Tel Aviv Univ, Sch Comp Sci, IL-69978 Tel Aviv, Israel Tel Aviv Univ Tel Aviv Israel IL-69978 mp Sci, IL-69978 Tel Aviv, Israel Hebrew Univ Jerusalem, Inst Comp Sci, IL-91904 Jerusalem, Israel Hebrew Univ Jerusalem Jerusalem Israel IL-91904 -91904 Jerusalem, Israel 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: 117 - 156
SICI:
0938-1279(200106)12:1-2<117:AGFFAT>2.0.ZU;2-I
Fonte:
ISI
Lingua:
ENG
Soggetto:
ABSTRACT INTERPRETATION;
Keywords:
termination of logic programs; abstract interpretation; constraints;
Tipo documento:
Article
Natura:
Periodico
Settore Disciplinare:
Engineering, Computing & Technology
Citazioni:
38
Recensione:
Indirizzi per estratti:
Indirizzo: Dershowitz, N Tel Aviv Univ, Sch Comp Sci, IL-69978 Tel Aviv, Israel Tel Aviv Univ Tel Aviv Israel IL-69978 78 Tel Aviv, Israel
Citazione:
N. Dershowitz et al., "A general framework for automatic termination analysis of logic programs", APPL ALG EN, 12(1-2), 2001, pp. 117-156

Abstract

This paper describes a general framework for automatic termination analysis of logic programs, where we understand by "termination" the finiteness ofthe LD-tree constructed for the program and a given query. A general property of mappings from a certain subset of the branches of an infinite LD-tree into a finite set is proved. From this result several termination theorems are derived, by using different finite sets. The first two are formulatedfor the predicate dependency and atom dependency graphs. Then a general result for the case of the query-mapping pairs relevant to a program is proved (cf. C29, 21]). The correctness of the Termilog system described in [22] follows from it. In this system it is not possible to prove termination forprograms involving arithmetic predicates, since the usual order for the integers is not well-founded. A new method, which can be easily incorporated in Termilog or similar systems, is presented, which makes it possible to prove termination for programs involving arithmetic predicates. It is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing. a termination proof into several cases, such that a simple termination function suffices for each case. Finally several possible extensions are outlined. This research has been partially supported by grants from the Israel Science Foundation.

ASDD Area Sistemi Dipartimentali e Documentali, Università di Bologna, Catalogo delle riviste ed altri periodici
Documento generato il 29/03/20 alle ore 08:41:42