Argumentation manuscript No.
(will be inserted by the editor)

Argumentation theory for mathematical argument
Joseph Corneli · Ursula Martin ·
Dave Murray-Rust · Gabriela Rino Nesin ·
Alison Pease

arXiv:1803.06500v1 [cs.CL] 17 Mar 2018

Received: date / Accepted: date

Abstract To adequately model mathematical arguments the analyst must be able to
represent the mathematical objects under discussion and the relationships between
them, as well as inferences drawn about these objects and relationships as the discourse
unfolds. We introduce a framework with these properties, which has been applied
to both mathematical dialogues and expository texts. The framework can recover
salient elements of discourse at, and within, the sentence level, as well as the way
mathematical content connects to form larger argumentative structures. We show how
the framework might be used to support computational reasoning, and argue that it
provides a more natural way to examine the process of proving theorems than do
Lamport’s structured proofs.
Keywords inference anchoring theory · mathematical practice · mathematical
argument · structured proof
Support from the UK Engineering and Physical Sciences Research Council is acknowledged under grants
EPSRC EP/K040251/2 (Corneli, Martin and Nesin), EP/J017728/2 (Murray-Rust) and EP/P017320/1
(Pease).
J. Corneli
School of Informatics
University of Edinburgh
E-mail: joseph.corneli@ed.ac.uk
U. Martin
Department of Computer Science
University of Oxford
D. Murray-Rust
Edinburgh College of Art
University of Edinburgh
G. Rino Nesin
Computing, Engineering and Mathematics
University of Brighton
A. Pease
Computing, School of Science and Engineering
University of Dundee

2

Joseph Corneli et al.

1 Introduction
Argumentation theory can help us understand the way mathematical knowledge develops. In order to better understand the processes of mathematical proof and communication, we turn to informal mathematical dialogues and expository texts as our
primary sources of data. Improved understanding of mathematical practice can, in
turn, inform the design of support tools for mathematicians.
Computational tools for proof checking, automatic theorem proving, and computer
algebra are well-established, however, they can only be used with formal, computationally explicit, content. Translating proofs into formal languages constitutes an
unrealistic demand for most mathematicians and students, and does little to address
their day-to-day communication needs (Thurston, 1994; Melis, 2005). Furthermore,
the existing mathematical literature is opaque to current computational systems, which
rely on hand-coded knowledge bases entered in formal or constrained languages
(Furse, 1990, 1994). Both data ingest and end-user interaction could benefit from the
use of an expressive modelling language that is closely related to the way mathematics
is actually done.
Our approach to modelling mathematical arguments is inspired by the generalpurpose argument modelling formalism Inference Anchoring Theory (IAT), introduced
by Reed and Budzynska (2011). 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). The Inference
Anchoring Theory + Content (IATC) framework we introduce is based on IAT, but with
several significant modifications. Most fundamentally, IATC is designed to surface the
structural features inherent in mathematical content.
Indeed, IATC could be used as an overlaid layer on top of mathematics represented in more formal languages, where an informal text can be put in full or partial
correspondence with a formal treatment. Lamport’s “Temporal Logic of Actions+”
(TLA+ ) (Lamport, 1999, 2014) is one candidate formalism that could be used to model
content-level expressions, by analogy with Lamport’s own semi-formal “structured
proofs” (Lamport, 1995, 2012).
Unlike structured proof, IATC does not aim to reshape the way people do mathematics, but to model it more exactly. As such, it constitutes groundwork for a future
generation of computer systems that can collaborate with mathematicians and students
in a way these potential users already understand. Epstein (2015) highlights the “extent
to which a person believes that her work experience or product has been facilitated or
improved by the collaboration” as a key evaluation metric for assessing collaborative
intelligent computer systems. The key metric at this stage is more basic, namely,
we are interested in the degree to which IATC can represent real-world examples
of mathematical practice in a way that can make them accessible to computational
reasoning. After introducing the modelling approach, we use several examples to show
that IATC is indeed satisfactory in this regard.
The plan of the work is as follows. §2 reviews previous research on mathematical
argument, in particular Inference Anchoring Theory. §3 describes the grammar of
IATC markup. §4 uses several examples of mathematical texts that have been thus

Argumentation theory for mathematical argument

3

marked-up in order to illustrate the relevant modelling concerns. §5 summarises and
reviews the contribution, situates our work in relationship to the broader literature,
and outlines potential directions for further work.

2 Background
In this section we give a brief summary of previous argumentation-theoretic research
on mathematical argument (§2.1). In addition, we describe Inference Anchoring
Theory (§2.2) and structured proof (§2.3), two landmarks that guide our effort.

2.1 Argumentation in mathematics
The term “argument” has several distinct meanings in a mathematical context. Gasteren
(1990) considers “mathematical arguments” to be proofs; Pedemonte (2007) disagrees
and sees them as something more general. “Argument” may in some cases stand for
the concept of an informally-presented proof, one hallmark being that such presentations admit multiple semantically distinct formalisations (Tanswell, 2015). On the
other hand, “argument” may stand for a still more abstract proof sketch (Lamport,
1995), which would not admit formalisation without the addition of significant further
details. Yet again, in mathematics as in other disciplines, the concept of “argument”
is sometimes associated with social phenomena of persuasive discussion (Zack and
Graves, 2001).
Carrascal (2015) provides an excellent survey of recent thinking about argument in
mathematics. Carrascal advises: “in order to learn more about the nature of mathematical practice and how its products are evaluated, we should be looking at real examples
of this practice.” She points to Pease and Martin (2012) as a notable example in this
genre. Once we have developed a suitable apparatus in Section 3, Section 4 will tackle
several real-world examples, including a detailed reexamination of the MiniPolymath
dataset studied by Pease and Martin, which is sourced from a public discussion of a
problem that appeared in an advanced high school level mathematical competition. In
this setting we see “argument” in all of the senses above.
Carrascal emphasises that mathematical communication has a rhetorical aspect
which depends on context. Aberdein (2010) contends that for argumentation to succeed, participants must possess many of the “virtues of argument”, broadly typologised
as willingness to engage in argumentation, willingness to listen to others, willingness
to modify one’s own position, and willingness to question the obvious. The relationship between mathematical reasoning and everyday reasoning has been debated
(Kisielewicz, 2016; Aberdein, 2016; Kisielewicz, 2017). With regard to the style of
argumentation suited to the mathematical context, Dutilh Novaes (2016) asserts that
“A good proof is one that convinces a fair but ‘tough’ opponent.”
“Blog maths” (Barany, 2010) like that found in research-level Polymath and advanced student-level MiniPolymath, along with forum-based mathematical discussions
like those found on the professional-level question-and-answer site MathOverflow,
“tell us about mathematicians’ attitudes to working together in public” as well as the

4

Joseph Corneli et al.

“kinds of activities that go on in developing a proof” (Martin, 2015). Alongside direct
mathematical contributions participants in these discussions typically work to maintain
“an environment which is friendly, collaborative, informal, polite and psychologically
safe” (Pease and Martin, 2012). When exchanges are mediated by text, different
interpretations need to be explicitly negotiated. Van Oers (2002) has suggested that
“mathematical problem solving in a group is not just an exchange or struggle of mathematical meanings, but is basically a permanent struggle of mutual interpretations
of meanings.” Mathematical content plays a key role in such exchanges: divergent
understandings are negotiated using shared concepts, definitions, and standards for
proof, even as the concepts evolve.
Along these lines, Pease et al (2017) used the methods of structured and abstract
argumentation to formalise the theory of informal mathematical developed in Lakatos’s
(1976) Proofs and Refutations as a set of rules for turn-taking in a dialogue game. These
rules define operations on a shared information state represented in the Argument
Interchange Format (AIF) (Lawrence et al, 2012), which is then interpreted by The
Online Argument Structures Tool (TOAST) (Snaith and Reed, 2012) and passed on to
DungOMatic (Snaith et al, 2010) to calculate the grounded extension, which in this
case represents the currently accepted, collaboratively constructed, proof or theory
under discussion. Dauphin and Cramer (2018) produced a similar model of naturaldeduction style arguments, explanations, and the “prima facie laws of logic” such as
may be debated in work on mathematical foundations.
The current effort does not attempt formality at that level. Instead, we adapt a more
general-purpose argument modelling approach, Inference Anchoring Theory, which is
described in the following section.

2.2 Inference Anchoring Theory
Inference Anchoring Theory (IAT) is used to model the logical relationships that obtain
between the propositional contents of the utterances made in dialogues (Budzynska
and Reed, 2011). As noted by Reed et al (2017), the inspiration for developing IAT
lies in earlier work on representing dialogue in the Argumentation Interchange Format.
A succinct high-level account of IAT is that:
arguing can be interpreted as an illocutionary act that comes about as the
result of a relation between uttering a premise and uttering a conclusion, thus
mirroring the logical structure of inference[.] (Reed et al, 2017, p. 146)
The theory’s essential features are as follow.
IAT is grounded in a notion of dialogical relations that formalise the informal
“conventions and norms that dictate the flow of dialogue” (Snaith and Reed, 2016).
Per Budzynska and Reed (2011), these dialogical relations are also referred to as
“transitions,” a term that is meant to recall the notion of transitions between operating
states in a finite state machine. Indeed, when the norms have been fully codified in
a dialogue protocol, the transitions are exactly described by a finite state machine.
In such a setting the formal argumentation-theoretic techniques and tools mentioned
briefly in Section 2.1 can be applied, though IAT models are not always fully formal.

Argumentation theory for mathematical argument

5

Content relationships are typically identified by matching locutions against known
argument schemes, e.g., an ‘Argument from Positive Consequences’ is associated
with two transitions, ‘challenging’ and ‘substantiating’ (Walton et al, 2008). In sum,
Inference Anchoring Theory is based on these three components:
(i) relations between locutions in a dialogue, called transitions;
(ii) relations between sentences (propositional contents of locutions); and
(iii) illocutionary connections that link locutions with their contents.
(Budzynska et al, 2014a), emphasis added
Although it is not mentioned explicitly in the
list above, IAT also makes use of ‘implicit’ speechacts, which anchor propositional content to transitions rather than to locutions. For example, if a
speaker asserts ‘A’ and their interlocutor says ‘No’,
in an IAT analysis the logical content ‘¬A’ would
be attached to the transition, rather than to the
negating word, as pictured in Figure 1. (Here “TA”
stands for a default transition, and “CA” stands
Fig. 1: IAT diagram for the
for default conflict, in other words, there is no exconversation ‘A’/‘No’.
plicit formal protocol attached to this dialogue.)
The locution ‘No’ cannot be made sense of without the preceding context, hence the
illocution attaches to the transition. The broader philosophical point
. . . follows directly from pragma-dialectical analysis which views the speech
act of assertion [ . . . ] as occurring at the ‘sentence’ level, and the speech act
of argumentation as occurring at a ‘higher textual level.’ (Budzynska and Reed,
2011)
Reed (2011) argues that implicit speech acts are ubiquitous; Botting (2015), by
contrast, says that the choice to anchor arguments on transitions is a conceptual
mistake. All opinions about how to cope with such situations aside, the ‘A’/‘No’
example illustrates how semantics may depend on context. Implicit speech acts are
intended to express “the way in which the rules of dialogue influence the construction
of argument” (Budzynska et al, 2016). However, for reasons that will be explained
below, in the current work we do not emphasise transitions—of either the explicit or
implicit variety—since we have a different approach to managing the relationships
between content and context.
To provide an adequate description of argumentation in mathematical settings, we
supplement IAT with an explicit register for content. Alongside (i)–(iii), above, we
introduce:
(iv) a model of non-propositional content, namely of the mathematical objects
under discussion, and the relations between them.
We will describe this addition in detail in Section 3, along with some other adaptations
to IAT that we have found useful in mathematical settings.

6

Joseph Corneli et al.

2.3 Lamport’s structured proofs
Structured proofs, as described by Lamport (1995, 2012), occupy the middle ground
between formal and informal mathematics, and provide a useful point of reference for
our work on IATC. Structured proofs offer a notational strategy that is a “refinement
of [ . . . ] natural deduction” (Lamport, 1995). While the proofs represented using
this system are not required to be strictly formal, the language of structured proofs
has evolved together with Lamport’s work on a formal language and corresponding
proof checking system, the “Temporal Logic of Actions+” (TLA+ ), which is used to
model concurrent systems (Lamport, 1999, 2014). 1 Structured proofs are, specifically,
structured as a strict hierarchy of lemmas.
While this is not representative of the way proofs are usually constructed in
day-to-day practice, Lamport has proposed that structured proofs can assist in proof
development, e.g., by helping to surface errors. Nevertheless, they do not necessarily
make the job of the reader easier: Lamport (2012, p. 20) quotes a referee who had read
one of his structured proofs:
The proofs [ . . . ] are lengthy, and are presented in a style which I find very
tedious. [ . . . ] My feeling is that informal proof sketches [ . . . ] to explain the
crucial ideas in each result would be more appropriate.
Unlike structured proofs, IATC is intended to help express the process by which proofs
are generated in standard practice, rather than to serve as a tool to make the process of
proving or reading proofs easier. It would nevertheless be philosophically compatible
with our aims to include formal statements in TLA+ (or some other language) in
IATC’s content layer. In the following section we introduce IATC, and in Section 4,
we will present an example that more fully illustrates the similarities and differences
between IATC and Lamport-style structured proof.
3 Inference Anchoring Theory + Content
IATC has many things in common with IAT, but should not be seen as a strict addition
to the earlier theory. In this section we describe the adaptations we have made, and
introduce the IATC modelling language.
Several important requirements arise from the features of the mathematics domain.
As we saw above, IAT is concerned with anchoring propositions to utterances and with
mapping the logical relationships that obtain between them. However, various mathematical objects—Larvor (2012) mentions “diagrams, notational expressions, physical
models, mental models and computer models”—are more comfortably thought of as
non-propositional in nature. Furthermore, a large part of mathematical discussion is in
essence meta-discussion about meta-level objects, dealing with proof strategies that
1 Only a few of the keywords available in the latest version of TLA+ appear in the structured proof
notation. Per Lamport (2015), the full list of TLA+ keywords is as follows. Those which are also used
in structured proofs are decorated with underlining: assume . . . prove . . . , boolean, by, case, choose,
constant (synonymously, constants), corollary, def, define, domain, else, except, extends,
have, hide, if, instance, lambda, lemma, let . . . in . . . , new, omitted, pick, proposition,
recursive, subset, suffices, take, theorem, unchanged, union, use, variable, witness.

Argumentation theory for mathematical argument

7

are suggested on the fly, and debates about whether these strategies are likely to work
as intended. Such discussions have been theorised formally using the notion of proof
plans, which are constructed and transformed using explicit heuristics and tactics
(Bundy, 1988). However, Fiedler and Horacek (2007, pp. 63-64) have suggested that
existing work with proof plans cannot be straightforwardly adapted from machineoriented to human-oriented contexts, because proof plans are, from a potential human
reader’s perspective, overly detailed, with insufficient structural abstraction. By contrast, a language like IATC is charged with expressing “strategic arguments that are
meaningful to humans” (Fiedler and Horacek, 2007, p. 68). However, as important as
strategic reasoning is, low-level mathematical content is even more fundamental.
We see the first-class role that content plays in mathematical discourse when new
terms are introduced and referred to, for example. Thus, the editor’s introduction to
Karttunen (1976) notes the following:
. . . informal notational practise of mathematicians, who will write an existentially quantified formula (say, (∃e)(∀x)(xe = ex = x), as one of a set of
postulates for group theory) and thenceforth use the variable bound by the
existential quantifier as if it were a constant as when they will write the next
postulate (∀x)(∃x−1 )(xx−1 = x−1 x = e). [punctuation modified]
Karttunen’s concept of “discourse referents,” illustrated in the quote above, underlies Discourse Representation Theory (Kamp and Reyle, 1993) and its extensions.
While the developers of IAT acknowledge the generality of Structured Discourse
Representation Theory (SDRT), in particular, they criticise it for making “assumptions
of context-independent semantics” (Budzynska et al, 2016). The ‘A’/‘No’ dialogue,
above, illustrated how context is handled in IAT: ‘No’ cannot be meaningfully understood outside of the conversation in which it is embedded. While we agree that context
is crucial, IATC differs from IAT in its approach. Specifically, IATC ignores the notion
of dialogical relations, and instead connects locutions to each other directly in the
content and intermediate (meta-discussion) layers. Before we describe the language in
detail, a simple example analogous to the ‘A’/‘No’ dialogue discussed shows how this
works (Figure 2).
Here, rather than connecting ‘No’ to
a transition, we connect it to previously
modelled content via a ‘Challenge’ illocution. This approach allows us to more
explicitly model the ways in which statements connect. For example, ‘B’ does
not simply conflict with A, but rather
presents a warrant for “not A”. Bob’s
Fig. 2: IATC diagram exhibiting a theory,
follow-up statement “maybe A0 ” might
a counterexample, and a reformulation.
in principle follow a default transition
from Wilma’s refutation, but the relationship between these statements is not explicit.
Referring to the emerging model of content, A0 is understood to relate most explicitly
to the content of Bob’s original statement “A”, and is modelled as a reformation of
that earlier statement.

8

Joseph Corneli et al.

In line with these design decisions, and inspired by the specific features of mathematical dialogue and exposition, IATC adds a range of extra machinery to the IAT
framework to model the relationships between mathematical objects and propositions,
along with an array of dialogue moves related to the strategic aspects of proof. Unlike
IAT, we make no attempt to cover argumentation in law, natural science, or interpersonal mediation, fields in which the norms that govern inference can be vastly different.
(Precedent, for example, may be acceptable in a legal argument but not in one about
ethics.) In mathematical argumentation, we find a much more homogeneous set of
conventions and norms, many of which are embodied in the objects under discussion
and the things that can sensibly be said about them. Details of our notational apparatus
are given in Tables 1 and 2.

Assert (s [, a ])
Agree (s [, a ])
Challenge (s [, a ])
Retract (s [, a ])
Define (o, p)
Suggest (s)
Judge (s, v)
Query (s)
QueryE ({pi (X)})

Performatives (perf[...])
Assert belief that statement s is true, optionally because of a.
Agree with a previous statement s, optionally because of a.
Assert belief that statement s is false, optionally because of a.
Retract a previous statement s, optionally because of
a.
Define object o via property p.
Suggest a strategy s.
Apply a heuristic value judgement v to some statement s.
Ask for the truth value of statement s.
Ask for the class of objects X for which all of the
properties {pi } hold.

Table 1: Inference Anchoring Theory + Content, part 1: Performatives

Argumentation theory for mathematical argument

9

Inferential Structure (rel[...])
implies (s, t)
Statement s implies statement t.
not (s)
Negation of s.
conjunction (s, t, . . . ) Conjunction of statements s, t, . . .
has_property (o, p)
Object o has property p.
instance_of (o, m)
Object o is an instance of the broader class m.
indep_of (o, d)
Object o does not depend on the choice of object d.
case_split (s, {si } . i) Statement s is equivalent to the conjunction of the
si ’s.
wlog (s, t)
Statement t is equivalent to statement s but easier to
prove.
Heuristics and Value Judgments (value[...])
Statement s is easy to prove; optionally, easier than
statement t.
plausible (s)
Statement s is plausible.
beautiful (s)
Statement s is beautiful (or mathematically elegant).
useful (s)
Statement s can be used in an eventual proof.
Statement x describes an heuristic (with less rigour
heuristic (x)
than a strategy).
easy (s [, t])

goal (s)
strategy (m, s)
auxiliary (s, a)
analogy (s, t)
implements (s, m)
generalise (m, n)

Reasoning Tactics (meta[...])
Used with Suggest to guide other agents to work
on s.
Method m may be used to prove s.
Statement s requires an auxiliary lemma a.
Statement s and statement t should be seen as analogous in some way.
Statement s implements the method m from a previously suggested strategy.
Method m generalises method n.

Content-Focused Structural Relations (struct[...])
used_in (o, s)
Object o is used in statement (or object) s.
sub_prop (s, t)
Statement s contains proposition t.
reform (s, t)
Statement s can be reformed into statement t.
extensional_set (p) The set of objects with property p.
instantiates (s, t)
Statement s schematically instantiates statement t.
expands (x, y)
Expression x expands to expression y.
sums (x, y)
Expression x sums to expression y.
cont_summand (x, y)
Expression x contains y as a summand.
Table 2: Inference Anchoring Theory + Content, part 2: Inferential Structure, Heuristics
and Value Judgments, Reasoning Tactics, and content-focused relations

10

Joseph Corneli et al.

At the core of IATC are a set of performatives, corresponding to the illocutionary
connections from IAT. These have slots which are in most cases are filled by statements.
The statements may be represented in unparsed natural language, as symbolic tokens
that serve as shorthand for such statements, or they may be parsed into expressions
in some representation language. The specification of IATC includes 9 performatives
(Table 1) together with 15 intermediate relations (Table 2).
These intermediate relations are clustered into segments treating Inferential Structure, Heuristics and Value Judgments, Reasoning Tactics, and Content-Focused Structural Relations. The latter category is used to surface relationships that apply directly
at the content level. For example, ‘used_in (o, s)’ states that object o appears in
statement s. Statements may be made directly about objects and propositions, or about
relationships between the same.
We have found two distinct linear notations useful: one of them explicitly retains
the grammatical categories ‘perf’, ‘rel’, ‘value’, ‘meta’, and struct’, while the
other discards them. For example, ‘perf[Assert](rel[has_property](o, p))’ denotes the assertion of the statement “object o has property p.” This notation is inspired
by McCarthy’s m-expressions (1960), whereas the other more compressed notation
is s-expression based and is used when grammatical categories do not need to be
explicitly presented, e.g., ‘(Suggest (goal perm_view_mod))’ is equivalent to
‘perf[Suggest](meta[goal](perm_view_mod))’.
Like IAT, IATC can also be used as a graphical representation language; a simple
fictive example was presented in Figure 2, above. Figure 3 gives an excerpt of a
real-world example showing both diagrammatic and textual IATC representations.
The example is treated more fully in Section 4.3; even in this short excerpt, we see
how mathematical objects (symbols ai ) and pieces of tagged content (‘problem’
and ‘perm_view’) provide a contextual setting for subsequent performatives to link
to. Note that bold lines at left in the figure are a shorthand for the ‘used_in’ relation. Colour coding highlights the correspondence between the graphical and textual
grammar elements.

perf[Assert](rel[equivalent](problem, perm_view))
perf[Judge](value[useful](perm_view))
perf[Suggest](meta[goal](perm_view))
struct[used_in](ai, problem)
struct[used_in](ai, perm_view)
Fig. 3: IATC markup of the statement “The following reformulation of the problem
may be useful: Show that for any permutation s in Sn , the sum as (1) + as (2) . . . + as ( j)
is not in M for any j ≤ n.”

Argumentation theory for mathematical argument

11

Fig. 4: Nested structures for implements and √
implies
√ in part of a solution to the
challenge problem “What is the 500th digit of ( 2 + 3)2012 ?”

The relations given in Tables 1 and 2 have been sufficient to describe the reasoning
in a range of examples, however we do not claim that this list of relationships would
treat all mathematical texts. Nor do these relationships describe mathematical texts at
the level of formality found in proof checking systems, or the level of detail found in
some other theorisations of discourse. Thus, in the future IATC should not be limited to
the set of tags presented here. For example, we have found uses for the value-judgments
‘easy’, ‘beautiful’, and ‘useful’, but it is quite plausible that future work would
find use for values such as ‘efficient’, ‘generative’, or something else; and
similarly, useful additions may be found in the other grammatical categories. The
evidence from our examples in Section 4 is that these major grammatical categories—
performatives, inferential relations, meta-level reasoning, value judgments, and content
relations—are themselves stable.
We have described, above, the use of content and strategic relationships as a
way to mediate contextual relationships, but context is also representable in IATC in
another more explicit way. Although IATC does not require proofs to be structured in

12

Joseph Corneli et al.

a tree-like hierarchy, nested structure is introduced as follows. In general, language
elements in Table 2 that have a statement slot can also have that slot filled by a
(possibly disconnected) subgraph. In this way structure corresponding to a “lemma”
can be indicated. A lemma, in this sense, is understood to be the reasoning that
‘implements’ a ‘strategy’, or, alternatively, a specific section of reasoning that
‘implies’ some conclusion. In Figure 4, part of a diagram adapted from Corneli et al
(2017b) shows both usages. This representation strategy is similar to the “partitioned
networks” introduced by Hendrix (1975, 1979).
To summarise, IATC resembles IAT in many ways, but some changes were necessary to express details of mathematical reasoning. For example, part of the propositional content of the statement in Figure 3 takes the form “The reformulation P
may be useful.” IAT has no way to extract P itself as a node, but IATC can do so:
it is represented as ‘perm_view’ in the figure. Later moves can then connect to this
piece of content, indeed, we already see such a link in the short example. In the
expanded example presented in Section 4.3, further negotiations about the content will
be unpacked.

4 Examples
In this section, we use three examples to showcase what IATC has to offer as a tool
for analysis. We illustrate
– how IATC might be used to support computational reasoning,
– how it expresses the reasoning structures that appear in real-world proofs,
– and how it helps to uncover the salient elements of mathematical discourse.
The presentation here is a novel and self-contained synthesis of examples that have
been treated in previous papers (Corneli et al, 2017a,b; Pease and Martin, 2012).
Section 4.1 shows how a question posed on the online Q&A forum, MathOverflow
might be modelled computationally. By extension, the ensuing dialogue could be
modelled similarly. MathOverflow is part of the Stack Exchange network of community question-and-answer websites. It is used to discuss research-level questions in
mathematics. Nevertheless, as Martin and Pease note:
The presentation is often speculative and informal, a style which would have
no place in a research paper, reinforced by conversational devices that are
accepting of error and invite challenge. (Martin and Pease, 2013)
In Section 4.1, we show how IATC makes the contents of such dialogues amenable to
further computational analysis.
Section 4.2 considers a challenge problem that was presented in a public lecture by
the mathematician Timothy Gowers (Gowers and Ganesalingam, 2012). The lecture
aimed to motivate and contextualise a project, then beginning, to develop mathematical
software that can “operate in a way that closely mirrors the way human mathematicians
operate” (Ganesalingam and Gowers, 2016). However, the specific problem presented
in the lecture was beyond the scope of Ganesalingam and Gowers’s (2016) method.
Studying this sort of problem in detail is nevertheless compatible with their general

Argumentation theory for mathematical argument

13

vision of “focusing on how humans find proofs.” This in turn is understood to help
design automatic systems that can create proofs which are both correct and explanatory.
Whereas Robinson (1965, p. 23) sought to
reduce complex inferences, which are beyond the capacity of the human mind
to grasp as single steps, to chains of simpler inferences, each of which is within
the capacity of the human mind to grasp as a single transaction,
an alternative route seeks to describe the heuristic process of proving in more cognitively plausible terms, in particular, by asking how (human) mathematicians avoid large
searches (Gowers, 2017). That project is far from complete. IATC might contribute
to the further development of such an effort: we will show that IATC can represent naturalistic details of reasoning that are not captured by more formally-oriented
Lamport-style structured proofs. Researchers working on mathematics software meant
to exhibit human-style reasoning may find this extra expressiveness useful.
Section 4.3 considers a larger-scale example, MiniPolymath 3, and shows how a
detailed IATC analysis expands on the typology of comments developed by Pease and
Martin (2012). The data that underlie this section were generated in a series of online
experiments in collaborative problem solving convened by mathematician Terence
Tao. 2, 3 The earlier analysis by Pease and Martin proposed a typology of comment
types, based on the comments’ contents: examples, conjectures, concepts, proofs,
and other, this last category including cross-referencing, explanation, justification,
appreciation, confirmation, discussion of a strategy’s difficulty, and courtesy comments.
An IATC analysis of the same data gives more a more detailed picture of the anatomy
of the comments in these intuitive categories.

4.1 Building computable models of mathematics with IATC: A Q&A example
As indicated in the Introduction, a metric for IATC’s success is the degree to which it
can represent real-world examples of mathematical practice in a way that makes them
accessible to computational reasoning. This section gives evidence for the plausibility
of such an enterprise.
Corneli et al (2017a) show how IATC can be used to model the discussion that
develops around the question from MathOverflow depicted in Figure 5. 4 The question
itself can be most straightforwardly parsed as proposing an analogy between two
propositions:
(1) “If G is a finite group, H is a subgroup of G and the index [G : H] is finite, then G
is not equal to the union of gHg−1 ”; and,
(2) “If G is an infinite group, H is a subgroup of G and the index [G : H] is finite, then
G is not equal to the union of gHg−1 .”
The querent knows that (1) is true, and, apparently, wants to know if (2) is true as
well. The comparison between these two statements is clear enough. However, as it
2
3
4

https://terrytao.wordpress.com/2011/06/09/mini-polymath-3-2011-imo-question/
https://polymathprojects.org/2011/07/19/minipolymath3-project-2011-imo/
http://mathoverflow.net/q/34044

14

Joseph Corneli et al.

Fig. 5: Screenshot of a question about group theory posted to MathOverflow: “I have
seen this problem, thatSif G is a finite group and H is a proper subgroup of G with
finite index then G 6=
gHg−1 . Does this remain true for the infinite case also?”
g∈G

turned out, discussants on MathOverflow observed that neither (1) nor (2) has quite the
right phrasing given the essence of the question under consideration. Robin Chapman
comments, “What theSstatement [(1)] should say is that if H is a proper finite index
subset of G then G 6= g∈G gHg−1 [ . . . ] As Keith shows, this is not always true for
subgroups of infinite index [‘(2)0 ’].”
As an illustration of our representation strategy, Listing 1 shows how several
Assertions and one Question written in IATC’s s-expression notation can express
the proposed analogy between (1) and (2), above, in such a way that the statements
become available to subsequent computational reasoning. Further details of the ensuing
dialogue could be represented similarly, but this excerpt is sufficient to show the
style. The listing is structured to illustrate the interaction between an analyst and
an interactive computer system. In the user interface, new information is added as
a sequence of parse trees rooted on IATC performatives. In the backend, these trees
are accumulated into one graph. The parse trees in Listing 1 give more detail than
IATC itself expresses; e.g., the predicates ‘finite-group’, and ‘subgroup’, as
well as the symbolic union of conjugate subgroups, and so on, are not part of the
IATC modelling language. Instead, they are understood as pure “content.” In the
s-expressions returned by ‘read-tree’, terms that belong to the IATC language
are decorated with unique numbers. Each one of these uniquely numbered items
(like ‘conjunction125’) corresponds to a separate “node” in the graph that is being
constructed in the system’s internal representation. These nodes are, accordingly,
uniquely addressable. The s-expressions input in steps “2” and “3” make use of these
numeric decorations to build additional structure on top of the structure created in
previous steps. The graph that is constructed by this process will eventually contain
two similar subgraphs, one containing the expression ‘(finite-group G)’ and
the other containing ‘(infinite-group G)’. Definitions for these predicates in an
underlying knowledge base may also be assumed to be similar (i.e., the two predicates
would be defined via identical group axioms, but each is associated with a different
cardinality). In a further round of computational processing, the proposed analogy
might be confirmed, at a symbolic level, by methods from Sowa and Majumdar (2003).

Argumentation theory for mathematical argument

15

However, more mathematical knowledge would have to be encoded to show that the
superficial analogy does not express a mathematical truth.
As a limited proof of concept showing the plausibility of adding a computational
deduction and verification layer on top of IATC representations, Corneli et al (2017b)
give a detailed expansion of one step of a mathematical proof using simple rules for
transforming the underlying graph structures. It is worth emphasising that the representations of reasoning afforded by language elements in Tables 1 and 2 do not themselves
encode the meta-level reasoning associated with such graph transformations.
Our basic claim is that IATC allows the argumentation aspects of mathematical
dialogues to be represented as explicit graphical structures. This gives a plausible basis
from which to develop an explicit computational model of the reasoning steps that are
implied in mathematical argumentation, including those which may not be explicitly
expressed in discourse.

16

Joseph Corneli et al.

1> (read-tree

’(Assert
(implies
(conjunction (finite-group G)
(subgroup H G)
(has_property (index H G)
finite))
(not (equal G
(union (times g
H
(inverse g))
:over g :in G))))))

→ (Assert123
(implies124
(conjunction125 (finite-group G)
(subgroup H G)
(has_property126 (index H G)
finite))
(not127 (equal G (union (times g
H
(inverse g))
:over g :in G)))))
2> (read-tree
’(Assert
(analogy (implies124
(conjunction125 (finite-group G)
(subgroup H G)
(has_property126 (index H G)
finite))
(not127 (equal G (union (times g
H
(inverse g))
:over g :in G))))
(implies
(conjunction (infinite-group G)
(subgroup H G)
(has_property (index H G)
finite))
(not (equal G
(union (times g
H
(inverse g))
:over g :in G)))))))
→ (Assert128 (analogy129 (implies124 ...)
(implies130 ...)))
3> (read-tree ’(Question implies130))
→ (Question134 implies130)

Listing 1: Importing a question that posits and probes an analogy between statements
about finite and infinite mathematical groups

Argumentation theory for mathematical argument

17

4.2 Making the reasoning explicit in the solution to a challenge problem
In Section 2.3, we described Lamport’s structured proofs: we now present a sideby-side comparison of a specific structured proof and an IATC analysis of the same
material. We will show that IATC is a more natural modelling tool in several regards.
Our chosen example is a “magic leap” problem presented in a public lecture by
Timothy Gowers (2012). This example has been modelled in IATC by Corneli et al
(2017b). The problem initially appears difficult but is mathematically straightforward
once the correct strategy is found. As such, an important part of the reasoning involved
in solving the problem is to find the correct strategy. The steps involved in this part of
the reasoning process are heuristic rather than deductive.
Figure 6 reproduces the proof in Lamport’s style; Figures 7, 8, and 9 present
portions of the IATC tagging of the solution that was presented in Gowers’s lecture.
Figure 7 illustrates an initial exploration of the question, and Figure 8 establishes a
‘strategy’ based on that exploration (“The trick might be: it is close to something
we can compute”). Figure 9 opens the door to actually applying the strategy. The
central part of the proof that ‘implements’ the strategy is highlighted in red in Figure
4, where the conclusion of the proof also appears.
The introduction to the proof, expanded in Figure 7—and condensed into a “P ROOF
SKETCH” in Figure 6—contains interesting examples of heuristic reasoning. This part
of the solution centres on the probing question “Can we do this for X?”, where X
ranges over several examples: x + y, e, and small rationals, and where ‘this’ denotes
“find the 500th digit of X2012 .” In the IATC representation, each tentative proposal to
“do this. . . ” stands in analogy with the original problem statement. Although Figure
7 contains only Assert performatives, a more complete representation would also
include Query performatives, since the analogies are not only proposed: their validity
is also queried, much as we saw in the example treated in the previous section.
Step 1 in the structured proof works out one of the ideas from the proof sketch at a
level of detail that was not present in the lecture, which instead progressed directly on
to the material treated in Step 2. As Fiedler and Horacek (2007, p. 69) noted, “The
analysis of human proof explanations shows that certain logical inferences are only
conveyed implicitly, drawing on the discourse context and default expectations.” There
is no hard and fast rule that can tell us how much of the implicit material we need to
explicate, but one rule of thumb that naturally arises from our representation strategy
is that coherently related discussions should correspond to connected graphs in the
expansion. Thus, for example, Figure 7 illustrates an implicit “unspoken” Assertion;
the proof is made fully explicit in Step 1 of the Lamport-style proof, but never appeared
in the original lecture. Again, in a standard IAT representation, unspoken assertions
would typically be represented as ‘implicit’ speech acts rooted on transitions, whereas
in IATC, we see how these unspoken assertions play a role in the argument via their
expansion and subsequent interconnections in the content layer.
Indeed, nowhere in the explicitly communicated reasoning is the key strategy
fully and explicitly stated. The basic strategy of the proof is that the quantity of interest
may be sufficiently close to something we can compute. In the IATC representation
(Figure 8), this is understood to be Suggested by the following statements from the
proof sketch, “And how about small perturbations of these? Maybe it is close to a

18

Joseph Corneli et al.

√
√
P ROOF SKETCH: What is the 500th digit of ( 2 + 3)2012 ? Even this,
eventually, a computer will be able to solve. The fact that this has been set as
a problem is a huge clue. Can we do this for x + y? For e? Small rationals?
And how about small perturbations of these? Maybe it is close to a rational?
h1i1. For n large enough and m small enough in comparison, the mth digit
of a sufficiently small rational r to the nth power is equal to 0.
P ROOF:
C ASE: r < 1/10
h2i1. (1/10)n = .1n has 0 in n − 1 places in its decimal expansion.
h2i2. r < 1/10 implies rn has zeros in at least n − 1 places in its
decimal expansion, so we simply
√ need
√ to select m < n.
h1i2. Can we compute the mth digit of ( 2 + 3)n ?
P ROOF:
C ASE: √
n = 2√
√ √
h2i1. ( 2 + 3)2 = 2 + 2 2 3 + 3 ∗
but if we
h1i3. Step 2.1 fails to give us an answer by direct
√ computation,
√
eliminate cross-terms, we can see that ( 2 + 3)2 is “close to” an
integer.
P ROOF:√
√
√
√
= 10
h2i1. (√2 + √3)2 + ( 2 −√ 3)2 √
h2i2. (√2 + √3)2 = 10 − ( 2 − 3)2
h2i3. ( 2 − 3)2 is small
P ROOF:√
√
h3i1. ( 2 − 3)2 ≈ (1 13 − 1 12 )2 by continued fraction approximation.
h3i2. (1 31 − 1 12 )2 = ( 86 − 96 )2 = 1/36
√
√
√
√
h1i4. Generalising Step 3.1, ( 2 + 3)2012 + ( 2 − 3)2012 is an integer!
P ROOF:
h2i1. √
Terms√with odd exponents cancel by the binomial theorem.
h1i5. And ( 2 − 3)2012 is a very small number. Maybe the final answer
will be “9”? We need to check whether it’s small enough.
P ROOF:√
√
h2i1. ( 2 − 3)2012 < (1/2)2012 by Step 3.3.1
h2i2. (1/2)2012 = ((1/2)4 )503
4 )503 = (1/16)503
h2i3. ((1/2)
√
√
h2i4. ( 2 − 3)2012 < (1/16)503 < .1503 , and so has at least 502
zeros in its decimal expansion by Step 1
h2i5. The answer is indeed 9.

1

1.1
1.2
2

2.1
3

3.1
3.2
3.3
3.3.1
3.3.2
4
4.1
5

5.1
5.2
5.3
5.4
5.5

Fig. 6: The solution to a challenge problem as a Lamport-style structured proof.

Argumentation theory for mathematical argument

Fig. 7: IATC tagging for the first portion of the challenge problem

Fig. 8: IATC tagging for the second portion of the challenge problem

19

20

Joseph Corneli et al.

Fig. 9: IATC tagging for the third portion of the challenge problem
rational?” Step 1 of the structured proof shows that rationals do, in fact, match the
strategy’s preconditions. The IATC representation is less explicit on this point, since it
sticks more closely to the reasoning expressed in the lecture. This example shows that
even relatively explicit statements may need further interpretation to be represented
meaningfully in IATC. Specifically, the way the proof progresses only makes sense
if we recognise the ‘strategy’ implied by what might otherwise appear to be a
throwaway comment early on.
Step 2 in the structured proof concerns another analogy. This time, a special one
which, the IATC analysis notes, symbolically
generalises the initial question
√
√ (Figure
√
√
8). That is, rather than considering ( 2 + 3)2012 we now consider ( 2 + 3)m .
(NB. an edge connecting the ‘generalise’ node to the problem statement has been
omitted.) However, the concept of generalisation remains implicit in the corresponding
portion of the structured proof. Indeed, Step 2 is not a good match for the requirements
of structured proof at all, since it is not a real lemma, and its “proof” fails (indicated by
“∗”). Including failed proof steps is not a problem for IATC. In Figure 9 the process of
solving the problem proceeds apace, without pausing to remark on a failed lemma,
now that something more interesting has been discovered.
Meanwhile, Step 3 in the structured proof implements
√
√ the main strategy for a
special case of our generalised problem, namely ( 2 + 3)2 , establishing a pattern
that leads to the conclusion. Again, Step 3.3 offers considerably more detail than
was present in the original lecture. Step 4 subsequently generalises the method that
was used in Step 3, and applies it to the expression we were originally interested in.
By Step 5, the necessary structure is in place, and all that is needed is a final check.
The content of Steps 5.1–5.4 collectively implies the final result in Step 5.5 (this
corresponds to the region highlighted in blue in Figure 4).
Several objections could be raised about the structured proof presented in Figure
6, most notably to the inclusion of a failed lemma in Step 2. However, as a source of
information about the intuition behind the proof, this failure is valuable. The IATC
treatment helps surface additional intuitions that remain implicit in the structured
proof: analogies, strategies, and relationships between methods are made explicit.

Argumentation theory for mathematical argument

21

While the structured proof augments the lecture with more technical details, IATC
provides a more faithful model of the reasoning expressed in the lecture itself.

4.3 MiniPolymath Revisited
In this section we use IATC to expand on the analysis of MiniPolymath due to Pease
and Martin (2012). We see that IATC can help advance the theory of mathematical
argument through the analysis of real world examples, per Carrascal (2015).
MiniPolymath 1 through 4 were part of a series of experiments in collaborative
online mathematics (Nielsen et al, 2009–2018). The problems were drawn from the
Mathematical Olympiad, a premier competition for pre-college students. Whereas
individuals working on Mathematical Olympiad problems frequently fail to solve
three of the challenge problems in the four-and-a-half hours allotted, each of the
collaborative Minipolymath efforts generated a solution—though it should be noted
that some of these solutions took more than 24 hours to develop. IATC can help us
understand how the proof efforts progressed, and can potentially help us understand
why they were (mathematically) successful.
Figure 10 presents an except from the MiniPolymath 1 dialogue (MPM1) as it
originally appeared on Tao’s blog. Figure 11 and Table 3 give the IATC analysis of this
excerpt in diagrammatic and textual form. The first portion of Figure 11 repeats Figure
3. The longer excerpt shown here exhibits the complex contextual interconnections
that develop in the content layer.
IATC was also used to tag the entirety of MiniPolymath 3 (MPM3). Figure 12
and Figure 13 give two different high-level views of the anatomy MPM3. The first
diagram shows how tags from IATC’s five grammatical categories were distributed
over time. Thus, for example, we see ‘value’ tags used early in the discussion as
strategies are being considered, and again later in the discussion when solutions are
being vetted. The second diagram shows the correspondence of IATC tags with the
earlier typology of comments developed by Pease and Martin (2012). In the initial
categorisation developed for that paper, comments were allowed to be in multiple
categories at once.
Here, to facilitate a clean mapping to IATC, we redid the categorisation with the
requirement that each comment should fit into exactly one main category. We arrived
at a nearly equal division of comments among the five categories: example (20.3%)
conjecture (21.2%), concept (19.5%), proof (19.5%), and other (19.5%). Aligning
this bulkier categorisation with the IATC tagging shows that these five intuitive labels
are mapped in very different ways to the more detailed IATC tag set.

22

Joseph Corneli et al.

Fig. 10: Screenshot of a portion of the MiniPolymath 1 dialogue

Fig. 11: IATC analysis of MPM1 excerpt (graphical form)

Argumentation theory for mathematical argument

23

(Haim) The following reformulation of the problem may be useful: “Show that
for any permutation s in Sn , the sum as(1) + as(2) + . . . + as( j) is not in M for any
j ≤ n.”
(1) perf[Assert](rel[equivalent](problem, perm_view)),
(2) perf[Judge](value[useful](perm_view)),
(3) perf[Suggest](meta[goal](perm_view)),
(4) struct[used_in](ai, problem),
(5) struct[used_in](ai, perm_view)
(—) Now, we may use the fact that Sn is “quite large” and prove the existence of
such permutation
(6) perf[Assert](rel[has_property](Sn, large)),
(7) struct[used_in](Sn, perm_view),
(8) struct[used_in](Sn, problem)
(—) with some kind of a pigeonhole-ish principle.
(9) perf[Suggest](meta[auxiliary](meta[strategy](
perm_view,pigeonhole), rel[has_property](Sn, large)))
(Dave) Addressing Haim(2 5): That’s pretty strong. And it doesn’t work; there are
numbers a1 , a2 , . . . , an and sets M of n − 1 points such that, for instance, a1 ∈ M .
Then any permutation starting with a1 would not satisfy your conjecture for j = 1.
(10) perf[Challenge](perm_view, a1_ex),
(11) perf[Assert](rel[instance_of](a1, a1_in_M)),
(12) struct[used_in](a1_ex, a1_in_M)
(—) But, just looking for one permutation that satisfies as(1) + as(2) + . . . + as( j) 6∈ M
for any j ≤ n (which is basically the statement of the theorem), could lend itself
well to induction.
(13) perf[Suggest](meta[goal](perm_view_mod)),
(14) struct[reform](perm_view, perm_view_mod),
(15) struct[used_in](Sn, perm_view_mod),
(16) struct[used_in](a1, perm_view_mod)
(—) In other words, use the fact that for every subset M 0 ⊂ M of size j not
containing as(1) + as(2) + . . . + as( j) , there is a way to permute those j numbers to
avoid M 0 .
(17) perf[Suggest](meta[strategy](perm_view_mod, strong_ind_n)),
(18) struct[used_in](n, strong_ind_n),
(19) struct[used_in](n, Sn)
(Haim) Addressing Dave: Sorry, indeed I meant: “Show that for one permutation...”
(20) perf[Retract](perm_view),
(21) perf[Agree](meta[goal](perm_view_mod))
Table 3: IATC analysis of MPM1 excerpt (text form)

24

Joseph Corneli et al.

We observe certain regularities: for example, Assert is present in all five types
of comments, but is used most frequently within proof-related comments. Annotations from the ‘struct’ grammatical category are most prevalently associated with
conjecture-related comments. (NB. In this tagging exercise we only considered the
‘used_in’ facet of the ‘struct’ category, so ‘structural’ is here a synonym for
‘used_in’.) It is not surprising that the performative Challenge is used most frequently in examples, since, intuitively, an example is likely to be put forward as a
counter-example. The most prevalent use of Agree is in comments that are categorised
as “other”. Retract is frequently used in this category as well, as is stronger (here,
a synonym for ‘implies’). These usages reflect social values as well as mathematical
semantics. E.g., one can express support for an idea by underscoring one’s belief in an
implication, as in comment 14.2.2 “Yes, it seems to be a correct solution!”

Fig. 12: Timeline of the MiniPolymath 3 dialogue showing the IATC grammar categories used in the tagging. Comments are binned into 5 minute intervals.

One might suspect that Suggest should be used only within conjectures, but in
the current categorisation it is used somewhat more frequently along with concepts.
This is partly explained by the fact that Suggest can be used to introduce either a
goal or a strategy. Sometimes goals represent conceptual tidying, as in “I guess
there is an odd / even number of point distinction to do” in comment 24.1.
In spite of our self-imposed constraint to map each comment to exactly one of the
five categories, in practice a comment may simultaneously introduce a concept along
with a conjecture that applies that concept. For example the straightforward concept of
“restriction[s] on how the next pivot is chosen”, in comment 2.1.1.1 appears along with
the more speculative conjecture “Can we start with a complete graph and all cycles on
that graph and just discard the ones that don’t follow the restrictions to converge on
the ones that do?” The need to introduce concepts together with conjectures applies

Argumentation theory for mathematical argument

25

in the case of more outlandish conjectures as well (“It might be fun to use projective
duality” in comment 12). However, a concept may also suggest a vague method
without raising a conjecture as such, e.g., “I’m thinking spirograph rather than convex
hull” in comment 3.1.1.2.1.1.
In sum, the IATC analysis of MiniPolymath 3 shows in detail how individual
contributions to the dialogue are comprised. In aggregate, this analysis exposes the
structural anatomy of a successful collaborative proof. It should be noted that not all
the contributions to MPM3 were equally relevant to the final solution. By entering the
structures in an explicit graphical model in the manner described in Section 4.1, graph
theoretic analysis could establish, e.g., the centrality of the various concepts used in
the content layer, and who introduced them into the conversation.

26

Joseph Corneli et al.

Conjecture

Concept

Proof

Other
Example
Fig. 13: Pie charts showing the frequency of IATC tags used to code MPM3, across
five categories. The pie charts record counts, not percentages. E.g., a statement such as
perf[Judge](value[useful](one_turn)) in the IATC tags of comment 2.1.1.1.1
counts towards both ‘Judge’ and ‘useful’, in this case, for the Proof pie chart.

Argumentation theory for mathematical argument

27

5 Conclusion
We have sought to advance the study of mathematical practice from an argumentationtheoretic perspective. We introduced Inference Anchoring Theory + Content, offered a
brief comparison with IAT, which it builds upon, and used three examples to showcase
IATC’s capabilities. We showed that:
– IATC has the potential to support computational reasoning about mathematics by
surfacing the structural relationships between pieces of mathematical content as
they appear in discourse.
– IATC offers a more faithful representation of everyday mathematical practice than
does Lamport-style structured proof.
– IATC can recover salient elements of discourse within comments, as well as with
the way these contents connect across comments.
Some limitations to the approach should be considered when applying the framework. We emphasise these are limitations and not necessarily flaws in the overall
design. In general, the limitations could be addressed with extensions to the language.
– IATC does not handle everything that is said in mathematical dialogues. We saw
above that IATC nevertheless helps disambiguate the “other” category bracketed
by earlier work.
– There are places where IATC representations remain bulky, pushing much of the
actual reasoning into whatever representation system handles the content layer.
– One related limitation is that implications and assumptions that mathematicians
consider “obvious” are typically elided from their discourse, often for valid expository reasons, and that, therefore, unpacking the contextual relationships between
statements typically requires a mathematically trained annotator.
– We introduced a graphical way to segment dialogues, but IATC does not currently
have the ability to express context shifts – although it can compare contexts with
‘analogy’.
Corneli et al (2018) survey other relevant frameworks that might form extensions for a
future version of IATC. It is worth mentioning that general-purpose formalisms like
the W3C’s “PROV” (Groth and Moreau, 2013) would allow us to say something about
the provenance and evolution of concepts, but would have nothing to say about the
mathematics-specific features that interest us.
Some other directions could expand IATC’s offerings. A recent special issue of
Argument & Computation (Harris and Marco, 2017) includes papers detailing the
usefulness of rhetorical structures for argument mining. Mitrović et al (2017), in that
volume, indicate the SALT Rhetorical Ontology (Groza et al, 2006; Groza, 2012) as
relevant prior work. SALT contains three categories—coherence relations, argument
scheme relations, and rhetorical blocks—each of which unfolds with considerable
further detail. These three categories can be seen as somewhat analogous to IATC’s
grammatical categories. Mitrović et al (2017) and Lawrence et al (2017) point to foundational work of Fahnestock (1999, 2004) on the argumentative function of rhetorical
figures, particularly in science writing. IATC might be profitably connected to such
analyses. Furthermore, the integration of rhetoric into argument mining highlights the

28

Joseph Corneli et al.

relevance of structures that are rather different from the IAT-style transitions that have
been used previously (Budzynska et al, 2015). White’s (1978, p. 6) pithy assertion that
“logic itself is merely a formalization of tropical strategies” can serve as an additional
provocation to develop structural analyses of this sort.
Nevertheless, whether mathematical content is modelled using ideas from logic,
rhetoric, or other sources, considerable further work will be required to effectively
describe the processes that are employed in forming and responding to mathematical
arguments. A small case study included as an appendix to Pease et al (2017) (and,
incidentally, based on MiniPolymath 3) illustrates the plausibility of Lakatos’s model—
however that model is clearly far from complete as a theory of mathematical production.
Pease et al were concerned with mathematical content only insofar as it fills slots
for some 20 dialogue moves that are based on Lakatos’s strategy for arguing about
lemmas and counterexamples. For example, MonsterBar(m, c, r) gives a reason r,
contradicting the justification m for the counter-conjecture not-c. At no point does
this theory touch the supposed mathematical ground of axioms and rules of inference.
That the reason r, for example, may have been formed inductively, or deductively, or
in some other way, goes undiscussed. IATC would allow us expand the structure that
appears within statements like r. Whereas Pease et al’s formalisation of Lakatosian
reasoning as a dialogue game offers a computational model of certain dynamical
patterns in mathematics, our current work has focused on kinematics. The efforts can
be seen as complementary: Bundy (2013) has argued that the right representation can
considerably simplify reasoning.
One promising approach to modelling process combines argumentation and multiagent systems (Modgil and McGinnis, 2007; Maghraby et al, 2012; Robertson, 2012).
However most approaches to modelling specifically mathematical agents have had
significant limitations. Thus, for example, Fiedler and Horacek (2007) have described
the difficulty of squaring argumentation-theoretic work with the methods of formal
proof. Ganesalingam and Gowers’s (2016) project aimed at simulating a solitary
individual rather than a population. However, Furse (1990) had already called into
question the robustness of approaches to modelling mathematical creativity that only
model a solitary creative individual. Pease et al (2009) describe an implementation
effort that made use of a multi-agent approach, drawing on argumentation theory
concepts and a Lakatosian model of dialogue. However, the mathematical applications
of that system were limited to straightforward computational aspects of number theory
and group theory, which suggests a “knowledge bottleneck” (Saint-Dizier, 2016;
Moens, 2018).
As indicated in a report of the National Research Council (2014, p. 90), “knowledge extraction and structuring in the context of mathematics” is in demand on an
increasingly industrial scale. IATC allows methods of argumentation to interface with
those of knowledge representation; both aspects are relevant to knowledge extraction.
Formalisation of IATC would assist in its applicability: “IKL Conceptual Graphs”
defined by Sowa (2008) would provide a natural foundation. IKL, the IKRIS Knowledge Language (Hayes, 2006; Sowa, 2008), deals elegantly with context and has been
used as a representational formalism in a project with aims comparable to our own:
the Slate project (Bringsjord et al, 2008), which centred on an argumentation tool

Argumentation theory for mathematical argument

29

that could support a mixture of deductive and informal reasoning. 5 Previous work on
mathematical usage can also inform future efforts in knowledge modelling with IATC
(Trzeciak, 2012; Wells, 2003; Wolska, 2015; Ginev, 2011).
Mathematical Knowledge Management, particularly in the “flexiformal” understanding developed by Kohlhase (2012) and Kohlhase et al (2017), presents another
paradigm that could eventually be integrated with IATC. Flexiformality combines
strict formalisations of those parts of mathematics for which that makes sense with
opaque representations of constants, objects, and informal theories. Iancu (2017) built
on Kohlhase’s work, and focused on “co-representing both the narration and content
aspects of mathematical knowledge in a structure preserving way” (pp. 3-4). However,
modelling narrative in Iancu’s sense is more relevant to the “frontstage” presentation
of mathematics in a single authorial voice than to the “backstage” production of
mathematics (cf. Hersh (1991)).
IATC offers a step forward for research into both the communication and production of mathematics, and can play a role in future work on knowledge extraction and
simulation. Potential applications include, among others, the development of a new
generation of mathematics tutoring software that engages the user in dialogues.

6 Acknowledgements
The authors thank Katarzyna Budzynska, Alan Bundy, Pat Hayes, Raymond Puzio, and
Chris Reed for helpful discussions, and acknowledge the support of fellow researchers
in the ARG-Tech group at the University of Dundee, and the DReaM group at the
University of Edinburgh. Figures were drawn using IHMC CmapTools and the Python
libraries matplotlib and plotly.

References
Aberdein A (2010) Virtue in argument. Argumentation 24(2):165–179
Aberdein A (2016) Commentary on Andrzej Kisielewicz’s: A new approach to argumentation and reasoning based on mathematical practice. In: Mohammed D,
Lewinski M (eds) Argumentation and Reasoned Action, Volume I: Proceedings of
the 1st European Conference on Argumentation, Lisbon 2015, College Publications,
Studies in Logic and Argumentation, vol 62
Barany M (2010) ‘[B]ut this is blog maths and we’re free to make up conventions
as we go along’: Polymath1 and the modalities of ‘massively collaborative mathematics’. In: Proceedings of the 6th International Symposium on Wikis and Open
Collaboration, ACM
Botting D (2015) Inferences and illocutions. Argument & Computation 6(3):246–264
Bringsjord S, Taylor J, Shilliday A, Clark M, Arkoudas K, Schoelles M, Destefano
M, Wodicka J (2008) Slate: An Argument-Centered Intelligent Assistant to Human
Reasoners. In: Proceedings of the 8th International Workshop on Computational
Models of Natural Argument (CMNA 8)
5

http://www.jfsowa.com/ikl/IKLslate.pdf

30

Joseph Corneli et al.

Budzynska K (2013) Circularity in ethotic structures. Synthese 190(15):3185–3207
Budzynska K, Reed C (2011) Speech Acts of Argumentation: Inference Anchors and
Peripheral Cues in Dialogue. In: Computational Models of Natural Argument: Papers from the 2011 AAAI workshop, URL http://www.aaai.org/ocs/index.
php/WS/AAAIW11/paper/view/3940
Budzynska K, Janier M, Reed C, Saint-Dizier P (2013) Towards extraction of dialogical arguments. In: Proceedings of 13th International Conference on Computational
Models of Natural Argument (CMNA 2013)
Budzynska K, Janier M, Kang J, Reed C, Saint-Dizier P, Stede M, Yaskorska O
(2014a) Towards argument mining from dialogue. In: COMMA, pp 185–196, URL
http://comma2014.arg.dundee.ac.uk/res/pdfs/19-budzynska.pdf
Budzynska K, Janier M, Reed C, Saint-Dizier P, Stede M, Yaskorska O (2014b)
A Model for Processing Illocutionary Structures and Argumentation in Debates. In: Proceedings of the Ninth International Conference on Language Resources and Evaluation (LREC-2014), Reykjavik, Iceland, May 26-31, 2014,
pp 917–924, URL http://www.lrec-conf.org/proceedings/lrec2014/
summaries/77.html
Budzynska K, Janier M, Kang J, Konat B, Reed C, Saint-Dizier P, Stede M, Yaskorska
O (2015) Automatically identifying transitions between locutions in dialogue. In:
1st European Conference on Argumentation (ECA 2015), pp pp–1
Budzynska K, Janier M, Reed C, Saint-Dizier P (2016) Theoretical foundations for
illocutionary structure parsing. Argument & Computation 7(1):91–108
Bundy A (1988) The use of explicit plans to guide inductive proofs. In: International
conference on automated deduction, Springer, pp 111–120
Bundy A (2013) The interaction of representation and reasoning. Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 469(2157), DOI 10.1098/rspa.2013.0194, URL http:
//rspa.royalsocietypublishing.org/content/469/2157/20130194,
http://rspa.royalsocietypublishing.org/content/469/2157/
20130194.full.pdf
Carrascal B (2015) Proofs, mathematical practice and argumentation. Argumentation
29(3):305–324, DOI 10.1007/s10503-014-9344-0, URL http://dx.doi.org/
10.1007/s10503-014-9344-0
Corneli J, Martin U, Murray-Rust D, Pease A (2017a) Towards mathematical AI via a
model of the content and process of mathematical question and answer dialogues.
In: Geuvers H, England M, Hasan O, Rabe F, Teschke O (eds) Intelligent Computer
Mathematics 10th International Conference, CICM 2017, Edinburgh, UK, 2017,
Proceedings
Corneli J, Martin U, Murray-Rust D, Pease A, Puzio R, Rino Nesin G (2017b) Modelling the way mathematics is actually done. In: Sperber M, Bresson J, Santolucito
M, McLean A (eds) 2017 International Workshop on Functional Art, Music, Modelling and Design (FARM 2017), ACM
Corneli J, Pease A, Stefanou D (2018) Social Aspects of Concept Invention. In: Confalonieri R, Pease A, Schorlemmer M, Besold T, Kutz O, Maclean E, KaliakatsosPapakostas M (eds) Concept Invention: Foundations, Implementation, Social Aspects and Applications, Computational Synthesis and Creative Systems, Springer

Argumentation theory for mathematical argument

31

Dauphin J, Cramer M (2018) ASPIC-END: Structured Argumentation with Explanations and Natural Deduction. Proceedings of the 2017 International Workshop on
Theory and Applications of Formal Argumention (TAFA)
Dutilh Novaes C (2016) Reductio ad absurdum from a dialogical perspective. Philosophical Studies 173(10):2605–2628
Epstein SL (2015) Wanted: Collaborative intelligence. Artificial Intelligence 221:36–
45
Fahnestock J (1999) Rhetorical Figures in Science. Oxford University Press
Fahnestock J (2004) Figures of Argument (OSSA 2005 Keynote Address). Informal
Logic 24(2)
Fiedler A, Horacek H (2007) Argumentation within deductive reasoning. International
Journal of Intelligent Systems 22(1):49–70
Furse E (1990) Why did AM run out of steam? Tech. rep., CS-90-4, Department of
Computer Studies, University of Glamorgan
Furse E (1994) The Mathematics Understander. In: Institute of Mathematics and its
Applications Conference Series, Oxford University Press, vol 51, pp 209–209
Ganesalingam M, Gowers W (2016) A Fully Automatic Theorem Prover with HumanStyle Output. Journal of Automated Reasoning pp 1–39
Gasteren AJ (1990) On the shape of mathematical arguments, Lecture Notes in
Computer Science, vol 445. Springer Science & Business Media
Ginev D (2011) The structure of mathematical expressions. Master’s thesis, Jacobs
University, Bremen, Germany
Gowers W (2017) How do human mathematicians avoid big searches? URL https:
//www.newton.ac.uk/seminar/20170728133014301, Lecture, Fri, July 28,
13:30 – 14:30, Isaac Newton Institute, University of Cambridge
Gowers W, Ganesalingam M (2012) Modelling the mathematical discovery process.
Maxwell Institute Lecture, Fri, November 2, 4pm – 5pm, James Clerk Maxwell
Building, University of Edinburgh
Groth P, Moreau L (2013) PROV-Overview. An Overview of the PROV Family of
Documents. World Wide Web Consortium
Groza T (2012) Advances in semantic authoring and publishing, vol 13. IOS Press
Groza T, Kim HL, Handschuh S (2006) SALT: Enriching LATEX with Semantic Annotations. In: Proceedings of the 5th International Semantic Web Conference (ISWC
2006)
Harris R, Marco CD (2017) Argument & Computation 8(3) [Special Issue on Rhetorical figures, arguments, computation.]
Hayes P (2006) IKL guide. URL http://www.ihmc.us/users/phayes/IKL/
GUIDE/GUIDE.html
Hendrix GG (1975) Partitioned networks for the mathematical modeling of natural
language semantics. PhD thesis, The University of Texas at Austin, also archived as
Tech. Report NL-28, Department of Computer Science
Hendrix GG (1979) Encoding knowledge in partitioned networks. In: Findler NV
(ed) Associative networks: Representation and use of knowledge by computers,
Academic Press, pp 51–92
Hersh R (1991) Mathematics has a front and a back. Synthese 88(2):127–133

32

Joseph Corneli et al.

Iancu M (2017) Towards Flexiformal Mathematics. PhD thesis, Jacobs University,
Bremen, DE
Janier M, Reed C (2017) Towards a theory of close analysis for dispute mediation
discourse. Argumentation 31(1):45–82
Kamp H, Reyle U (1993) From discourse to logic: An introduction to modeltheoretic
semantics of natural language, formal logic and DRT
Karttunen L (1976) Discourse referents. In: McCawley JD (ed) Syntax and Semantics,
Vol. 7: Notes from the Linguistic Underground, Academic Press, pp 363–386
Kisielewicz A (2016) A new approach to argumentation and reasoning based on mathematical practice. In: Mohammed D, Lewinski M (eds) Argumentation and Reasoned
Action, Volume I: Proceedings of the 1st European Conference on Argumentation,
Lisbon 2015, College Publications, Studies in Logic and Argumentation, vol 62
Kisielewicz A (2017) Logika i argumentacja. Ksiȩgarnia Internetowa PWN
Kohlhase M (2012) The flexiformalist manifesto. In: Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2012 14th International Symposium
on, IEEE, pp 30–35
Kohlhase M, Koprucki T, Müller D, Tabelow K (2017) Mathematical models as research data via flexiformal theory graphs. In: International Conference on Intelligent
Computer Mathematics, Springer, pp 224–238
Lakatos I (1976) Proofs and refutations: The logic of mathematical discovery. Cambridge University Press
Lamport L (1995) How to write a proof. The American Mathematical Monthly
102(7):600–608
Lamport L (1999) Specifying Concurrent Systems with TLA+ . NATO Science Series,
III: Computer and Systems Sciences 173(173):183–247
Lamport L (2012) How to write a 21st century proof. Journal of fixed point theory and
applications 11(1):43–63
Lamport L (2014) TLA+2 : A Preliminary Guide. URL http://lamport.
azurewebsites.net/tla/tla2-guide.pdf
Lamport L (2015) The TLA+ hyperbook. URL http://lamport.azurewebsites.
net/tla/hyperbook.html
Larvor B (2012) How to think about informal proofs. Synthese 187(2):715–730
Lawrence J, Bex F, Reed C, Snaith M (2012) AIFdb: Infrastructure for the argument
web. In: Proceedings of the Fourth International Conference on Computational
Models of Argument (COMMA 2012), pp 515–516
Lawrence J, Visser J, Reed C (2017) Harnessing rhetorical figures for argument mining.
Argument & Computation 8(3):289–310
Maghraby A, Robertson D, Grando A, Rovatsos M (2012) Automated deployment of
argumentation protocols. In: COMMA, pp 197–204
Martin U (2015) Stumbling Around in the Dark: Lessons from Everyday Mathematics, Springer International Publishing, Cham, pp 29–51.
DOI 10.1007/978-3-319-21401-6 2, URL https://doi.org/10.1007/
978-3-319-21401-6_2
Martin U, Pease A (2013) What does mathoverflow tell us about the production of
mathematics? In: SOHUMAN, 2nd International Workshop on Social Media for
Crowdsourcing and Human Computation, at ACM Web Science 2013, May 1, 2013,

Argumentation theory for mathematical argument

33

Paris
McCarthy J (1960) Recursive functions of symbolic expressions and their computation
by machine, part i. Communications of the ACM 3(4):184–195
Melis E (2005) Why proof planning for maths education and how? Mechanizing
Mathematical Reasoning pp 364–378
Mitrović J, OReilly C, Mladenović M, Handschuh S (2017) Ontological representations of rhetorical figures for argument mining. Argument & Computation 8(3):267–
287
Modgil S, McGinnis J (2007) Towards Characterising Argumentation Based Dialogue
in the Argument Interchange Format. In: International Workshop on Argumentation
in Multi-Agent Systems, Springer, pp 80–93
Moens MF (2018) Argumentation mining: How can a machine acquire common sense
and world knowledge? Argument & Computation 9(1)
National Research Council (2014) Developing a 21st Century Global Library for
Mathematics Research. National Academies Press
Nielsen M, et al (2009–2018) Polymath wiki. URL http://michaelnielsen.org/
polymath1/index.php?title=Main_Page
van Oers B (2002) Fruits of Polyphony: A Commentary on a Multiperspective Analysis
of Mathematical Discourse. Journal of the Learning Sciences 11(2-3):359–363, DOI
10.1080/10508406.2002.9672143, URL https://doi.org/10.1080/10508406.
2002.9672143, https://doi.org/10.1080/10508406.2002.9672143
Pease A, Martin U (2012) Seventy four minutes of mathematics: An analysis of the
third Mini-Polymath project. In: Proceedings of AISB/IACAP 2012, Symposium
on Mathematical Practice and Cognition II, URL http://homepages.inf.ed.
ac.uk/apease/papers/seventy-four.pdf
Pease A, Smaill A, Colton S, Lee J (2009) Bridging the gap between argumentation
theory and the philosophy of mathematics. Foundations of Science 14(1):111–135
Pease A, Lawrence J, Budzynska K, Corneli J, Reed C (2017) Lakatos-style Collaborative Mathematics through Dialectical, Structured and Abstract Argumentation.
Artificial Intelligence 246:181–219, URL http://www.sciencedirect.com/
science/article/pii/S0004370217300267
Pedemonte B (2007) How can the relationship between argumentation
and proof be analysed? Educational Studies in Mathematics 66(1):23–
41, DOI 10.1007/s10649-006-9057-x, URL http://dx.doi.org/10.1007/
s10649-006-9057-x
Reed C (2011) Implicit speech acts are ubiquitous. Why? They join the dots. In:
Proceedings of the conference on argumentation: Cognition and community (OSSA2011)
Reed C, Budzynska K (2011) How dialogues create arguments. In: Proceedings of
the 7th Conference on Argumentation of the International Society for the Study of
Argumentation
Reed C, Budzynska K, Duthie R, Janier M, Konat B, Lawrence J, Pease A,
Snaith M (2017) The argument web: an online ecosystem of tools, systems and services for argumentation. Philosophy & Technology 30(2):137–
160, DOI 10.1007/s13347-017-0260-8, URL http://dx.doi.org/10.1007/
s13347-017-0260-8

34

Joseph Corneli et al.

Robertson D (2012) Lightweight Coordination Calculus for Agent Systems: Retrospective and Prospective, Springer Berlin Heidelberg, Berlin, Heidelberg, pp
84–89. DOI 10.1007/978-3-642-29113-5 7, URL https://doi.org/10.1007/
978-3-642-29113-5_7
Robinson JA (1965) A machine-oriented logic based on the resolution principle.
Journal of the ACM (JACM) 12(1):23–41
Saint-Dizier P (2016) Argument Mining: The bottleneck of knowledge and language
resources. In: 10th International Conference on Language Resources and Evaluation
(LREC 2016), pp pp–983
Snaith M, Reed C (2012) TOAST: online ASPIC+ implementation. In: Proceedings of
the 4th International Conference on Computational Models of Argument (COMMA
2012), IOS Press, Vienna
Snaith M, Reed C (2016) Dialogue grammar induction. In: Mohammed D, Lewinski M (eds) Argumentation and Reasoned Action, Volume I: Proceedings of the
1st European Conference on Argumentation, Lisbon 2015, Studies in Logic and
Argumentation, vol 62, College Publications
Snaith M, Devereux J, Lawrence J, Reed C (2010) Pipelining argumentation technologies. In: Baroni P, Cerutti F, Giacomin M, Simari (eds) Proceedings of the 3rd
International Conference on Computational Models of Argument (COMMA 2010),
IOS Press, pp 447–454
Sowa JF (2008) Conceptual Graphso. In: van Harmelen F, Lifschitz V, Porter B (eds)
Handbook of Knowledge Representation, Elsevier, chap 5, pp 213–237
Sowa JF, Majumdar AK (2003) Analogical reasoning. In: Aldo A, Lex W, Ganter
B (eds) Conceptual Structures for Knowledge Creation and Communication: 11th
International Conference on Conceptual Structures, ICCS 2003, Dresden, Germany,
July 21-25, 2003, Proceedings, Springer, no. 2746 in LNAI, pp 16–36
Tanswell F (2015) A Problem with the Dependence of Informal Proofs on Formal
Proofs. Philosophia Mathematica 23(3):295, DOI 10.1093/philmat/nkv008, URL
http://dx.doi.org/10.1093/philmat/nkv008
Thurston W (1994) On proof and progress in mathematics. Bulletin (New Series) of
the American Mathematical Society 30(2):161–177
Trzeciak J (2012) Mathematical English Usage. A Dictionary. URL http://www.
emis.de/monographs/Trzeciak/biglist.html
Walton D, Reed C, Macagno F (2008) Argumentation Schemes. Cambridge University
Press, New York, USA
Wells C (2003) A handbook of mathematical discourse. Infinity Publishing
White HV (1978) Tropics of discourse: essays in cultural criticism. Johns Hopkins
University Press
Wolska MA (2015) Students’ language in computer-assisted tutoring of mathematical
proofs. No. 40 in Saarbrücken Dissertations in Language Science and Technology,
Universaar
Zack V, Graves B (2001) Making mathematical meaning through dialogue: “once
you think of it, the Z minus three seems pretty weird”. Educational Studies in
Mathematics 46(1):229, DOI 10.1023/A:1014045408753, URL https://doi.
org/10.1023/A:1014045408753

