On Termination of Binary CLP Programs

Abstract. Termination of binary CLP programs has recently become an important question in the termination analysis community. The reason for this is due to that a number of approaches to termination of logic programs abstract the input program to a binary CLP program and conclude termination of the input from termination of the abstracted program. In this paper we introduce a class of binary CLP programs such that their termination can be proved by using linear level mappings. We show that membership to this class is decidable and present a decision procedure. Further, we extend this class to programs such that their termination proofs require a combination of linear functions. In particular we consider as level mappings tuples of linear functions and piecewise linear functions.

• Type: Conference
• Year: 2004
• Where: LOPSTR
• Authors: Alexander Serebrenik, Frédéric Mesnard
• Keywords: Binary Clp Programs, Linear Functions, LOPSTR 2004, Termination Analysis Community