Termination proofs for logic programs (Q1188722)

The volume is broadly conceived (in the good sense) and it can serve as a thorough introduction to the termination problem of logic programs and generally as a summary of the latest important results in the area of logic programming. A technique for the automatic generation of termination proofs for logic programs is presented. Such a technique cannot be complete due to the undecidability of the halting problem for Turing machines. A reasonable goal is achieved - to identify sufficient criteria for termination which are of practical interest. Pure Prolog programs are investigated, the nonlogical features of Prolog still deserve serious analysis. Since the only potential source of infinite computations in pure Prolog (without side effects) is recursion, the problem of automatic termination proofs is tractable. A termination proof gives evidence of the fact that the recursive instance of a problem is easier to solve than the original problem. The technique is based on comparison of tuples of terms and proving that the terms occurring in recursive calls become smaller according to a well founded ordering. The occurrence of local variables poses difficulties which are overcome by semantic approach. An algorithm deriving linear inequalities for predicates is applied. It assumes that the program is normalized and has no mutual recursion (which is eliminated by static program transformation). Compared with the approach taken by Ullman and van Gelder, the author presents a more general approach in the format of inequalities and in the way how sizes of terms are measured. This more powerful method can handle quicksort and permutation where the technique of Ullman and van Gelder does not suffice. However, the mergesort remains beyond the scope.