Termination is well-known to be one of the important aspects of program correctness. Logic programming provides a framework with a strong theoretical basis for tackling this problem. However, due to the declarative formulation of programs, the danger of non-termination may increase. As a result, termination analysis received considerable attention in logic programming. Recently, the study of termination of numerical programs led to the emerging of the adorning technique . This technique implements the well-known divide et impera strategy by distinguishing between different subsets of values for variables, and deriving termination proofs based on these subsets. In this paper we generalise this technique and discuss its applicability to the domain of terms (the Herbrand domain).
|Title of host publication||Proceedings of the 13th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2003), 25-27 August 2003, Uppsala, Sweden|
|Place of Publication||Berlin|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science|