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

Maxim Makatchev, Pamela W. Jordan, Kurt VanLehn

Research output: Contribution to journalArticle

3 Citations (Scopus)

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 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)
Volume3220
StatePublished - 2004
Externally publishedYes

Fingerprint

Proof Search
Physics
Proposition
Abduction
Reasoning
Heuristics
Students
Specificity
Knowledge representation
Modeling
Knowledge Representation
Graph in graph theory
Feedback
Theorem
Atoms
Correctness
Maximise
Costs
Costs and Cost Analysis
Metric

ASJC Scopus subject areas

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

Cite this

@article{38644a05f3b84105a146d0201d89601f,
title = "Modeling students' Reasoning about qualitative physics: Heuristics for abductive proof search",
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.",
author = "Maxim Makatchev and Jordan, {Pamela W.} and Kurt VanLehn",
year = "2004",
language = "English (US)",
volume = "3220",
pages = "699--709",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

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 -