Interpreting semi-formal utterances in dialogs about mathematical proofs

Dialogs in formal domains, such as mathematics, are characterized by a mixture of telegraphic natural language text and embedded formal expressions. Analysis methods for this kind of setting are rare and require empirical justification due to a notorious lack of data, as opposed to the richness of presentations found in genre-specific textbooks. In this paper, we focus on interpretation techniques for major phenomena observed in a recently collected corpus of tutorial dialogs on proving mathematical theorems. We combine analysis techniques for mathematical formulas and for natural language expressions, supported by knowledge about domain-relevant lexical semantics and by representations relating informal vocabulary to precise domain terms. Interpreting these expressions in a competent manner is not only important for the use in tutorial systems, but also for supporting domain experts through improving the accessibility and usability of formal systems.