A transformational methodology for proving termination of logic programs

Abstract

An approach for proving termination of well-moded logic programs is given by transforming a given logic program into a term rewriting system. It is proved that the termination of the derived rewriting system implies the termination of the corresponding logic program for well-moded queries under any selection rule implied by the given modings. The approach is mechanizable using termination orderings proposed in the term rewriting literature. Unlike Ullman and van G elder’s approach and PI timer’s method, no preprocessing is needed, and the approach works well even in the presence of mutual recursion. This approach has been used recently to show termination of the Prolog implementation of compiler for ProCoS level 0 language PL0 developed at Oxford University.