Explanations and Proof Trees

Authors

  • Gérard Ferrand
  • Willy Lesaint
  • Alexandre Tessier

Keywords:

Explanation, proof tree, rule, fixpoint, closure, constraint logic programming, constraint satisfaction problem, error diagnosis, constraint retraction

Abstract

This paper proposes a model for explanations in a set theoretical framework using the notions of closure or fixpoint. In this approach, sets of rules associated with monotonic operators allow to define proof trees. The proof trees may be considered as a declarative view of the trace of a computation. We claim they are explanations of the results of a computation. This notion of explanation is applied to constraint logic programming, and it is used for declarative error diagnosis. It is also applied to constraint programming, and used for constraint retraction.

Downloads

Download data is not yet available.

Downloads

Published

2012-01-30

How to Cite

Ferrand, G., Lesaint, W., & Tessier, A. (2012). Explanations and Proof Trees. Computing and Informatics, 25(2-3), 105–122. Retrieved from https://www.cai.sk/ojs/index.php/cai/article/view/335