2002/04/12 by Yi-Dong Shen, Jia-Huai You, Li-Yan Yuan +2
Computer Science · #cs.LO #cs.PL
published as ACM Transactions on Computational Logic 4(4):417-430, 2003 · To appear in ACM TOCL
arxiv created 2002/04/12 · arxiv updated 2009/11/30
We present a new characterization of termination of general logic programs. Most existing termination analysis approaches rely on some static information about the structure of the source code of a logic program, such as modes/types, norms/level mappings, models/interargument relations, and the like. We propose a dynamic approach which employs some key dynamic features of an infinite (generalized) SLDNF-derivation, such as repetition of selected subgoals and recursive increase in term size. We also introduce a new formulation of SLDNF-trees, called generalized SLDNF-trees. Generalized SLDNF-trees deal with negative subgoals in the same way as Prolog and exist for any general logic programs.