Declarative Debugging in Constraint Logic Programming: the Cover Relation

This work is motivated by the declarative insufficiency diagnosis of constraint logic programs, but focuses only, in this paper, on theoretical viewpoints. Many techniques have been developed for logic programming but cannot be merely adapted to constraint logic programming. An answer is not covered by a more general computed answer any more. Practical implementations use incomplete solvers with regard to theoretical framework of CLP (Jaffar and Lassez 1986) based on a theory or a domain. New theoretical foundations are necessary. 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 p..