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. Constraint logic program semantics is redefined in terms of proof trees using a cover relation. 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 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 declarative error notion. Indeed, it is incoherent to use only low level debugging tools based on an understanding of the operational behaviour of the system and to give up a high level knowledge of the declarative meaning of the programs. But, the success of a declarative debugging tool is directly relat..