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.