Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation

Alison Pease (Lead / Corresponding author), John Lawrence, Katarzyna Budzynska, Joseph Corneli, Chris Reed

Research output: Contribution to journalArticle

  • 7 Citations

Abstract

The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. We demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. Finally, we offer reflections on our mixed-initiative collaborative approach.
LanguageEnglish
Pages181-219
Number of pages39
JournalArtificial Intelligence
Volume246
Early online date1 Mar 2017
DOIs
Publication statusPublished - May 2017

Fingerprint

argumentation
mathematics
dialogue
Social aspects
Theorem proving
game theory
Game theory
artificial intelligence
historical development
logic
abstraction
Labeling
Artificial intelligence
Lenses
artifact
Semantics
semantics
simulation
Argumentation
Mathematics

Keywords

  • Automated theorem proving
  • automated reasoning
  • abstract argumentation
  • argumentation
  • collaborative intelligence
  • dialogue games
  • Lakatos
  • mathematical argument
  • structured argumentation
  • social creativity
  • philosophy of mathematical practice

Cite this

@article{9546d30155294ceaabc3ccd1da0d031d,
title = "Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation",
abstract = "The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. We demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. Finally, we offer reflections on our mixed-initiative collaborative approach.",
keywords = "Automated theorem proving, automated reasoning, abstract argumentation, argumentation, collaborative intelligence, dialogue games, Lakatos, mathematical argument, structured argumentation, social creativity, philosophy of mathematical practice",
author = "Alison Pease and John Lawrence and Katarzyna Budzynska and Joseph Corneli and Chris Reed",
note = "We further gratefully acknowledge that this work has been supported in part by the Polish National Science Centre under grant 2011/03/B/HS1/04559, in part by the EPSRC under grants EP/G060347/1, EP/N014871/1 and EP/K037293/1, and in part by the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open Grant number 611553 (COINVENT).",
year = "2017",
month = "5",
doi = "10.1016/j.artint.2017.02.006",
language = "English",
volume = "246",
pages = "181--219",
journal = "Artificial Intelligence",
issn = "0004-3702",
publisher = "Elsevier",

}

TY - JOUR

T1 - Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation

AU - Pease, Alison

AU - Lawrence, John

AU - Budzynska, Katarzyna

AU - Corneli, Joseph

AU - Reed, Chris

N1 - We further gratefully acknowledge that this work has been supported in part by the Polish National Science Centre under grant 2011/03/B/HS1/04559, in part by the EPSRC under grants EP/G060347/1, EP/N014871/1 and EP/K037293/1, and in part by the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open Grant number 611553 (COINVENT).

PY - 2017/5

Y1 - 2017/5

N2 - The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. We demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. Finally, we offer reflections on our mixed-initiative collaborative approach.

AB - The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. We demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. Finally, we offer reflections on our mixed-initiative collaborative approach.

KW - Automated theorem proving

KW - automated reasoning

KW - abstract argumentation

KW - argumentation

KW - collaborative intelligence

KW - dialogue games

KW - Lakatos

KW - mathematical argument

KW - structured argumentation

KW - social creativity

KW - philosophy of mathematical practice

U2 - 10.1016/j.artint.2017.02.006

DO - 10.1016/j.artint.2017.02.006

M3 - Article

VL - 246

SP - 181

EP - 219

JO - Artificial Intelligence

T2 - Artificial Intelligence

JF - Artificial Intelligence

SN - 0004-3702

ER -