In this paper we describe a part of the Why2-Atlas tutoring system that models students' reasoning in the domain of qualitative physics. The main goals of the model are (1) to evaluate correctness of the student's essay, and, in case the essay contains errors, (2) to direct remedial tutoring actions according to plausible errors in the student's reasoning. To meet these goals, a backchaining theorem prover generates a set of assumptions and a chain of reasoning (a proof) that plausibly led the student to write the observed essay. A proof can include correct as well as buggy reasoning steps and assumptions. After a proof is generated, it is analyzed for correctness and the analysis is used to generate appropriate feedback to the student. We describe the weighted abductive theorem proving framework, outline previous and upcoming evaluations and discuss possible future directions.
For a PDF full article version, click here (147KB).