Termination Analysis for Tabled Logic Programming

Abstract We provide a theoretical basis for studying the termination of tabled logic programs executed under SLG-resolution using a left-to-right computation rule. To this end, we study the classes of quasi-terminating and LG-terminating programs (for a set of atomic goals S ). These are tabled logic programs where execution of each call from S leads to only a finite number of different (i. e. , non-variant) calls, and a finite number of different calls and computed answer substitutions for them, respectively. We then relate these two classes through a program transformation, and present a characterisation of quasi-termination by means of the notion of quasi-acceptability of tabled programs. The latter provides us with a practical method of proving termination and the method is illustrated on non-trivial examples of tabled logic programs.

Authors

• Stefaan Decorte
• Danny De Schreye
• Michael Leuschel
• Bern Martens
• Konstantinos Sagonas

Keywords

No keywords are indexed for this paper.