Argumentation theory for mathematical argument

Computational tools to support this through proof checking, automatic theorem proving, and computer algebra are well-established, though they require formal, computationally explicit, content as input. However, the existing mathematical literature, particularly informal mathematical dialogues, and expository texts, is opaque to such systems, which cannot currently handle the variety of activities typically involved in producing such knowledge and proofs, such as, for example, exposition and argument that concerns making conjectures, forming concepts, and discussing examples and counterexamples. Our goal is to bridge this gap through devising an expressive modelling language that is closely related to the way mathematics is actually done. Our approach to modelling such content is inspired by the general-purpose argument modelling formalism Inference Anchoring Theory (IAT), introduced by Reed and Budzynska (2010). As its name suggests, IAT anchors logical inferences in discourse. IAT has been applied to mediation (Janier and Reed, 2017), debates (Budzynska et al, 2014b), and to paradoxes in ethotic argumentation (Budzynska, 2013), along with other real-world dialogues (Budzynska et al, 2013).