Explanations and Proof Trees

Contents

This paper proposes a model for explanations in a set the- oretical framework using the notions of closure or fixpoint. In this approach, sets of rules associated with monotonic op- erators allow to de ine proof trees (Aczel 1977). The proof trees may be considered as a declarative view of the trace of a computation. We claim they are explanations of the result of a computation. First, the general scheme is given. This general scheme is applied to Constraint Logic Pro- gramming, two notions of explanations are given: positive explanations and negative explanations. A use for declara- tive error diagnosis is proposed. Next, the general scheme is applied to Constraint Pro- gramming. In this framework, two de initions of explana- tions are described as well as an application to constraint retraction.