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, IL69978 Tel Aviv, Israel Tel Aviv Univ Tel Aviv Israel IL69978 mp Sci, IL69978 Tel Aviv, Israel Hebrew Univ Jerusalem, Inst Comp Sci, IL91904 Jerusalem, Israel Hebrew Univ Jerusalem Jerusalem Israel IL91904 91904 Jerusalem, Israel Katholieke Univ Leuven, Dept Comp Sci, B3001 Heverlee, Belgium KatholiekeUniv Leuven Heverlee Belgium B3001 B3001 Heverlee, Belgium
 Titolo Testata:
 APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING
fascicolo: 12,
volume: 12,
anno: 2001,
pagine: 117  156
 SICI:
 09381279(200106)12:12<117:AGFFAT>2.0.ZU;2I
 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, IL69978 Tel Aviv, Israel Tel Aviv Univ Tel Aviv Israel IL69978 78 Tel Aviv, Israel



 Citazione:
 N. Dershowitz et al., "A general framework for automatic termination analysis of logic programs", APPL ALG EN, 12(12), 2001, pp. 117156
Abstract
This paper describes a general framework for automatic termination analysis of logic programs, where we understand by "termination" the finiteness ofthe LDtree constructed for the program and a given query. A general property of mappings from a certain subset of the branches of an infinite LDtree 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 querymapping 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 wellfounded. 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 querymapping 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