Makatchev, M., Jordan, P., & VanLehn, K. (2004). Abductive Theorem Proving for Analyzing Student Explanations and Guiding Feedback in Intelligent Tutoring Systems. Journal of Automated Reasoning for Special Issue on Automated Reasoning and Theorem Proving in Education. 32(3), 187-226.

In this paper we describe an application of weighted abductive 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 first mapped into a first order predicate logic representation, 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 diagnosis of the observed errors that help identify possible tutoring actions. We describe the knowledge representation, rules and weighted abductive theorem proving framework, outline previous and upcoming evaluations, and discuss possible future directions.

For a PDF full article version, click here (152KB).