Tutorial dialogs on mathematical proofs
Christoph Benzmüller, Armin Fiedler, Malte Gabsdil, Helmut Horacek, Ivana Kruijff‐Korbayová, Manfred Pinkal, Jörg Siekmann, Dimitra Tsovaltzi, Vo Nguyen Quoc Bao, Magdalena Anna Wolska · Swinburne figshare (Swinburne University of Technology) · 2003
The representation of knowledge for a mathematical proof assistant is generally used exclusively for the purpose of proving theorems. Aiming at a broader scope, we examine the use of mathematical knowledge in a mathematical tutoring system with flexible natural language dialog. Based on an analysis of a corpus of dialogs we collected with a simulated tutoring system for teaching proofs in naive set theory, we identify several interesting problems which lead to requirements for mathematical knowledge representation. This includes resolving reference between natural language expressions and mathematical formulas, determining the semantic role of mathematical formulas in context, and determining the contribution of inference steps specified by the user. 1