A Framework of Directionality for Proving Termination of Logic Programs.

Abstract

Abstract In this paper we propose a rich notion of directionality of predicates that combines modes and regular tree types. We provide a semantic soundness result for this notion and give inference systems to decide well-modedness of logic programs and goals. We show how this rich notion of directionality can be used to prove the universal termination of LD-resolution for logic programs with non-ground goals by using simple syntactic orderings of the kind used in rewriting theory.