How to Build Explanations of Automated Proofs A Methodology and Requirements on Domain Representations
Helmut Horacek · 2007
There is ample evidence that results produced by problem-solving methods and ingredients suitable for human-adequate explanations may differ fundamen-tally, which makes documenting the behavior of intelli-gent systems and explaining the solutions they produce quite challenging. Focusing on the explanation of solu-tions found by the most general problem-solvers, auto-mated theorem provers, we sketch what has emerged as a methodology over the past decade in our work-ing group for building content specifications for these kind of explanations. This methodology is conceived as a stratified model with dedicated transformation pro-cesses bridging between adjacent strata. Our investiga-tions have shown that explanation capabilities based on problem-solving knowledge only are limited in a num-ber of ways, which motivates one to represent extra knowledge relevant for communication purposes.