Author name cluster

Stefaan Decorte

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

LOPSTR Conference 1998 Conference Paper

Termination Analysis for Tabled Logic Programming

Stefaan Decorte
Danny De Schreye
Michael Leuschel
Bern Martens
Konstantinos Sagonas

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.

Details

LOPSTR Conference 1993 Conference Paper

Automatic Termination Analysis

Kristof Verschaetse
Stefaan Decorte
Danny De Schreye

Abstract Proving termination of programs is important in any approach to program development. In logic programming, where the logic and the control component of a program can very easily be dealt with in two separate phases of the development, the termination issue is solely addressed in the second phase. Both formal, theoretical frameworks for reasoning about termination, and automatic techniques for termination analysis have recently obtained considerable attention in the logic programming community. Unfortunately, in current work, these two types of approaches to termination have been rather orthogonal. It would be desirable if automatic techniques could rely directly on general frameworks for their correctness proofs. We recently presented a new, practical framework for termination analysis of definite logic programs with respect to call patterns. In the current paper, we describe an automated technique, which is directly based on the framework. The main advantages are: the generality of the approach (analysis can be performed for any given set of top-level goals), the clear theoretical underpinning provided by the framework and full automation. .

Details