Explanations and Proof Trees

Gérard Ferrand, Willy Lesaint, and Alexandre Tessier

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.