Declarative Debugging in Constraint Logic Programming

. This paper is motivated by the declarative insufficiency diagnosis of constraint logic programs, but focuses only on theoretical viewpoints. Many techniques have been developed for logic programming but cannot be merely adapted to constraint logic programming. Constraint logic program semantics is redefined in terms of proof trees using a cover relation. Proof trees give an intrinsic definition to the answers provided by a program. The cover relation expresses that a constraint is covered by a (possibly infinite) constraint set. Thus we give a theoretical framework where declarative diagnosis method can be studied thanks to the inductive nature of the semantics. We define the notions of symptoms and errors and we prove that if there exists a symptom then there exists an error. 1 Introduction A great strength of Constraint Logic Programming (CLP) is its declarative nature. For a declarative language (with a semantics independent of its execution model), it is essential to consider a ..