Abductive Proofs as Models of Qualitative Reasoning

In this paper we describe an application of weighted ab-ductive theorem proving that is used to create a model of students ' qualitative reasoning for the Why2-Atlas tutoring system. The system encourages a student to write an essay in natural language so that the essay provides both an explanation as well as an answer to a qualitative mechanics problem. The student's essay is rst mapped into a rst-order predicate logic repre-sentation, which the abductive theorem prover treats as a goal (observation) in order to generate a proof that explains the essay. The resulting proof (1) provides an evaluation of the correctness of the student's essay, and, in the event the essay contains errors, (2) provides a di-agnosis of the observed errors that help identify possible tutoring actions. We describe the knowledge represen-tation, rules and weighted abductive theorem proving framework, outline previous and upcoming evaluations, and discuss possible future directions