### Abstract

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 language | English (US) |
---|---|

Pages (from-to) | 699-709 |

Number of pages | 11 |

Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Volume | 3220 |

State | Published - 2004 |

Externally published | Yes |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science(all)
- Biochemistry, Genetics and Molecular Biology(all)
- Theoretical Computer Science

### Cite this

**Modeling students' Reasoning about qualitative physics : Heuristics for abductive proof search.** / Makatchev, Maxim; Jordan, Pamela W.; VanLehn, Kurt.

Research output: Contribution to journal › Article

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, vol. 3220, pp. 699-709.

}

TY - JOUR

T1 - Modeling students' Reasoning about qualitative physics

T2 - Heuristics for abductive proof search

AU - Makatchev, Maxim

AU - Jordan, Pamela W.

AU - VanLehn, Kurt

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=35048817006&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35048817006&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:35048817006

VL - 3220

SP - 699

EP - 709

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -