Characterizing Termination of Logic Programs with Level Mappings.

Abstract

We study a large class of logic programs which terminate with respect to a natural class of goals.Both classes are characterized in terms of level mappings.The class of logic programs is strong enough to compute every total recursive function.The class of goals considerably extends the variable-free ones.Based on the ideas developed in this paper we present a technique which improves the termination behaviour of Prolog programs.