Towards declarative diagnosis of constraint programs over nite domains

The paper proposes a theoretical approach of the debugging of con-straint programs based on a notion of explanation tree. The proposed approach is an attempt to adapt algorithmic debugging to constraint pro-gramming. In this theoretical framework for domain reduction, expla-nations are proof trees explaining value removals. These proof trees are de ned by inductive denitions which express the removals of values as consequence of other value removals. Explanations may be considered as the essence of constraint programming. They are a declarative view of the computation trace. The diagnosis consists in locating an error in an explanation rooted by a symptom