Modeling students' Reasoning about qualitative physics: Heuristics for abductive proof search

Maxim Makatchev, Pamela W. Jordan, Kurt VanLehn

Research output: Contribution to journalArticle

3 Scopus citations


We describe a theorem prover that is used in the Why2Atlas tutoring system for the purposes of evaluating the correctness of a student's essay and for guiding feedback to the student. The weighted abduction framework of the prover is augmented with various heuristics to assist in searching for a proof that maximizes measures of utility and plausibility. We focus on two new heuristics we added to the theorem prover: (a) a specificity-based cost for assuming an atom, and (b) a rule choice preference that is based on the similarity between the graph of cross-references between the propositions in a candidate rule and the graph of cross-references between the set of goals. The two heuristics are relevant to any abduction framework and knowledge representation that allow for a metric of specificity for a proposition and cross-referencing of propositions via shared variables.

Original languageEnglish (US)
Pages (from-to)699-709
Number of pages11
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - Dec 1 2004
Externally publishedYes


ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this